Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL

Asta Halkjær*, Frederik Krogsdal Jacobsen

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

52 Downloads (Pure)

Abstract

We describe the design, implementation and verification of an automated theorem prover for firstorder logic with functions. The proof search procedure is based on sequent calculus and we formally verify its soundness and completeness in Isabelle/HOL using an existing abstract framework for coinductive proof trees. Our analytic completeness proof covers both open and closed formulas. Since our deterministic prover considers only the subset of terms relevant to proving a given sequent, we do so as well when building a countermodel from a failed proof. Finally, we formally connect our prover with the proof system and semantics of the existing SeCaV system. In particular, the prover can generate human-readable SeCaV proofs which are also machine-verifiable proof certificates.

Original languageEnglish
Title of host publicationProceedings of 13th International Conference on Interactive Theorem Proving
EditorsJune Andronick, Leonardo de Moura
PublisherSchloß Dagstuhl
Publication date1 Aug 2022
Pages13:1--13:22
Article number13
ISBN (Electronic)9783959772525
Publication statusPublished - 1 Aug 2022
Event13th International Conference on Interactive Theorem Proving - Haifa, Israel
Duration: 7 Aug 202210 Aug 2022

Conference

Conference13th International Conference on Interactive Theorem Proving
Country/TerritoryIsrael
CityHaifa
Period07/08/202210/08/2022
SeriesLeibniz International Proceedings in Informatics, LIPIcs
Volume237
ISSN1868-8969

Keywords

  • Completeness
  • First-Order Logic
  • Isabelle/HOL
  • Prover
  • SeCaV
  • Soundness

Fingerprint

Dive into the research topics of 'Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL'. Together they form a unique fingerprint.

Cite this