package coq-propcalc

  1. Overview
  2. No Docs
Propositional Calculus

Install

Dune Dependency

github.com Edit opam file Versions (6)

Authors

  1. F
    Floris van Doorn <fpvdoorn@gmail.com> [http://www.contrib.andrew.cmu.edu/~fpv/]

Maintainers

  1. H
    Hugo.Herbelin@inria.fr

Sources

v8.7.0.tar.gz
md5=201c4c6bb4453482fae1c75e3a3a9d6b

Description

http://arxiv.org/abs/1503.08744

Formalization of basic theorems about classical propositional logic. The main theorems are (1) the soundness and completeness of natural deduction calculus, (2) the equivalence between natural deduction calculus, Hilbert systems and sequent calculus and (3) cut elimination for sequent calculus.

Tags

keyword: propositional calculus keyword: classical logic keyword: completeness keyword: natural deduction keyword: sequent calculus keyword: cut elimination category: Mathematics/Logic/Foundations

Published: 11 Jan 2019

Dependencies (2)

  1. coq >= "8.7" & < "8.8~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None