Conference paper
A Concise Sequent Calculus for Teaching First-Order Logic
We have formalized soundness and completeness for a sequent calculus for classical firstorder logic in the proof assistant Isabelle/HOL. We first describe a technique for extending a completeness result for closed formulas to completeness for open formulas as well. This requires some tricky reasoning due to our use of de Bruijn indices.
We then describe a concise sequent calculus for first-order logic and introduce a useful way to write up the sequent calculus derivations in Isabelle/HOL. Our formalization has recently been used in a computer science course on automated reasoning.
Language: | English |
---|---|
Year: | 2020 |
Proceedings: | Isabelle Workshop 2020<br/> |
Types: | Conference paper |
ORCIDs: | From, Asta Halkjær and Villadsen, Jørgen |