A Concise Sequent Calculus for Teaching First-Order Logic

Research output: Contribution to conferencePaperResearchpeer-review

76 Downloads (Pure)

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 languageEnglish
Publication date2020
Number of pages16
Publication statusPublished - 2020
EventIsabelle Workshop 2020
- Virtual event
Duration: 30 Jun 202030 Jun 2020
https://sketis.net/isabelle/isabelle-workshop-2020

Workshop

WorkshopIsabelle Workshop 2020
LocationVirtual event
Period30/06/202030/06/2020
Internet address

Keywords

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

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

Cite this