License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2022.13
URN: urn:nbn:de:0030-drops-167221
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16722/
Go to the corresponding LIPIcs Volume Portal

From, Asta Halkjær ; Jacobsen, Frederik Krogsdal

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

pdf-format:
LIPIcs-ITP-2022-13.pdf (0.7 MB)

Abstract

We describe the design, implementation and verification of an automated theorem prover for first-order 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.

BibTeX - Entry

@InProceedings{from_et_al:LIPIcs.ITP.2022.13,
  author =	{From, Asta Halkj{\ae}r and Jacobsen, Frederik Krogsdal},
  title =	{{Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{13:1--13:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16722},
  URN =		{urn:nbn:de:0030-drops-167221},
  doi =		{10.4230/LIPIcs.ITP.2022.13},
  annote =	{Keywords: Isabelle/HOL, SeCaV, First-Order Logic, Prover, Soundness, Completeness}
}

Keywords: Isabelle/HOL, SeCaV, First-Order Logic, Prover, Soundness, Completeness
Collection: 13th International Conference on Interactive Theorem Proving (ITP 2022)
Issue Date: 2022
Date of publication: 03.08.2022
Supplementary Material: Software (Isabelle/HOL formalization in the Archive of Formal Proofs): https://www.isa-afp.org/entries/FOL_Seq_Calc2.html

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI