package coq-propcalc

  1. Overview
  2. No Docs
Propositional Calculus

Install

Dune Dependency

arxiv.org 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.10.0.tar.gz
md5=e1ab2584b2a3713b92c06f543803de34

Description

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: 07 Dec 2019

Dependencies (2)

  1. coq >= "8.10" & < "8.11~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None