Propositional Calculus in Coq
classification
🧮 math.LO
cs.LO
keywords
calculusdeductionnaturalpropositionalsequenttheoremsassistantclassical
read the original abstract
I formalize important theorems about classical propositional logic in the proof assistant Coq. The main theorems I prove 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.