Search Results

Documents authored by From, Asta Halkjær

Artifact
Software
DOI: 10.4230/artifacts.23798
Analytic Completeness

Authors: Asta Halkjær From and Anders Schlichtkrull

Abstract
Cite as

Asta Halkjær From, Anders Schlichtkrull. Analytic Completeness (Software, Mechanization). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-23798,
   title = {{Analytic Completeness}}, 
   author = {From, Asta Halkj{\ae}r and Schlichtkrull, Anders},
   note = {Software, version 1.0., swhId: \href{https://archive.softwareheritage.org/swh:1:dir:1bea24a089edbdbc233081a23b0dc45963bf6c8f;origin=https://github.com/astahfrom/Analytic_Completeness;visit=swh:1:snp:1c9ea048be7f3b4c9f6ed573e2d87ba0b8480717;anchor=swh:1:rev:cd6a06dd8478287763c6e820e51581322faa7f2c}{\texttt{swh:1:dir:1bea24a089edbdbc233081a23b0dc45963bf6c8f}} (visited on 2025-09-22)},
   url = {https://github.com/astahfrom/Analytic_Completeness},
   doi = {10.4230/artifacts.23798},
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.8
Abstract, Compositional Consistency: Isabelle/HOL Locales for Completeness à la Fitting

Authors: Asta Halkjær From and Anders Schlichtkrull

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Smullyan and Fitting have used abstract consistency properties to great effect in unifying meta-theoretical results in logic. In this paper, we generalize these developments with the help of Isabelle/HOL. We use locales to decompose abstract consistency into general parts, and provide the textbook variants as special cases. Users can assemble their own consistency property for a given logic. The compositionality alleviates the absence of dependent types in Isabelle/HOL. We use our development to mechanize completeness of calculi for three logics: (1) first-order logic where we only instantiate universal quantifiers with already occurring terms, (2) second-order logic over general models, and (3) a recently developed strong hybrid logic with propositional quantification.
Cite as

Asta Halkjær From and Anders Schlichtkrull. Abstract, Compositional Consistency: Isabelle/HOL Locales for Completeness à la Fitting. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{from_et_al:LIPIcs.ITP.2025.8,
  author =	{From, Asta Halkj{\ae}r and Schlichtkrull, Anders},
  title =	{{Abstract, Compositional Consistency: Isabelle/HOL Locales for Completeness \`{a} la Fitting}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{8:1--8:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.8},
  URN =		{urn:nbn:de:0030-drops-246406},
  doi =		{10.4230/LIPIcs.ITP.2025.8},
  annote =	{Keywords: Logic, completeness, abstract consistency property, Isabelle/HOL, locales}
}
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}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2020.5
Synthetic Completeness for a Terminating Seligman-Style Tableau System

Authors: Asta Halkjær From

Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)

Abstract
Hybrid logic extends modal logic with nominals that name worlds. Seligman-style tableau systems for hybrid logic divide branches into blocks named by nominals to achieve a local proof style. We present a Seligman-style tableau system with a formalization in the proof assistant Isabelle/HOL. Our system refines an existing system to simplify formalization and we claim termination from this relationship. Existing completeness proofs that account for termination are either analytic or based on translation, but synthetic proofs have been shown to generalize to richer logics and languages. Our main result is the first synthetic completeness proof for a terminating hybrid logic tableau system. It is also the first formalized completeness proof for any hybrid logic proof system.
Cite as

Asta Halkjær From. Synthetic Completeness for a Terminating Seligman-Style Tableau System. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{from:LIPIcs.TYPES.2020.5,
  author =	{From, Asta Halkj{\ae}r},
  title =	{{Synthetic Completeness for a Terminating Seligman-Style Tableau System}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{5:1--5:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-182-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{188},
  editor =	{de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.5},
  URN =		{urn:nbn:de:0030-drops-138847},
  doi =		{10.4230/LIPIcs.TYPES.2020.5},
  annote =	{Keywords: Hybrid logic, Seligman-style tableau, synthetic completeness, Isabelle/HOL}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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