Abstract
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.
| Original language | English |
|---|---|
| Publication date | 2020 |
| Number of pages | 16 |
| Publication status | Published - 2020 |
| Event | Isabelle Workshop 2020 - Virtual event Duration: 30 Jun 2020 → 30 Jun 2020 https://sketis.net/isabelle/isabelle-workshop-2020 |
Workshop
| Workshop | Isabelle Workshop 2020 |
|---|---|
| Location | Virtual event |
| Period | 30/06/2020 → 30/06/2020 |
| Internet address |
Keywords
- First-Order Logic
- Sequent Calculus
- Isabelle/HOL