2 Search Results for "Jacobsen, Frederik Krogsdal"

Document
DOI: 10.4230/LIPIcs.TYPES.2021.8
A Succinct Formalization of the Completeness of First-Order Logic

Authors: Asta Halkjær From

Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)

Abstract
I succinctly formalize the soundness and completeness of a small Hilbert system for first-order logic in the proof assistant Isabelle/HOL. The proof combines and details ideas from de Bruijn, Henkin, Herbrand, Hilbert, Hintikka, Lindenbaum, Smullyan and others in a novel way, and I use a declarative style, custom notation and proof automation to obtain a readable formalization. The formalized definitions of Hintikka sets and Herbrand structures allow open and closed formulas to be treated uniformly, making free variables a non-concern. This paper collects important techniques in mathematical logic in a way suited for both study and further work.
Cite as

Asta Halkjær From. A Succinct Formalization of the Completeness of First-Order Logic. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 8:1-8:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{from:LIPIcs.TYPES.2021.8,
  author =	{From, Asta Halkj{\ae}r},
  title =	{{A Succinct Formalization of the Completeness of First-Order Logic}},
  booktitle =	{27th International Conference on Types for Proofs and Programs (TYPES 2021)},
  pages =	{8:1--8:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-254-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{239},
  editor =	{Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.8},
  URN =		{urn:nbn:de:0030-drops-167771},
  doi =		{10.4230/LIPIcs.TYPES.2021.8},
  annote =	{Keywords: First-Order Logic, Completeness, Isabelle/HOL}
}
Document
DOI: 10.4230/LIPIcs.ITP.2022.13
Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL

Authors: Asta Halkjær From and Frederik Krogsdal Jacobsen

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

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.
Cite as

Asta Halkjær From and Frederik Krogsdal Jacobsen. Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 13:1-13:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.ITP.2022.13},
  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}
}
  • Refine by Author
  • 2 From, Asta Halkjær
  • 1 Jacobsen, Frederik Krogsdal

  • Refine by Classification
  • 1 Theory of computation → Automated reasoning
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Program verification
  • 1 Theory of computation → Proof theory

  • Refine by Keyword
  • 2 Completeness
  • 2 First-Order Logic
  • 2 Isabelle/HOL
  • 1 Prover
  • 1 SeCaV
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 2 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact