A Concise Sequent Calculus for Teaching First-Order Logic

Asta Halkjær From, Jørgen Villadsen

Research output: Contribution to conferencePaperResearchpeer-review

170 Downloads (Pure)


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 languageEnglish
Publication date2020
Number of pages16
Publication statusPublished - 2020
EventIsabelle Workshop 2020
- Virtual event
Duration: 30 Jun 202030 Jun 2020


WorkshopIsabelle Workshop 2020
LocationVirtual event
Internet address


  • First-Order Logic
  • Sequent Calculus
  • Isabelle/HOL


Dive into the research topics of 'A Concise Sequent Calculus for Teaching First-Order Logic'. Together they form a unique fingerprint.

Cite this