Propositional Calculus in Coq
Floris van Doorn
TL;DR
This paper formalizes key theorems in classical propositional logic within Coq, including soundness, completeness, equivalence of proof systems, and cut elimination, enhancing formal verification of logical systems.
Contribution
It provides a formal proof of fundamental theorems in propositional logic using Coq, establishing equivalences and properties of various proof calculi.
Findings
Soundness and completeness of natural deduction proven in Coq
Equivalence between natural deduction, Hilbert, and sequent calculus established
Cut elimination for sequent calculus demonstrated
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Logic, Reasoning, and Knowledge