Asta Halkjær From

I strengthen the foundations of epistemic logic by formalizing the family of normal modal logics in the proof assistant Isabelle/HOL. I define an abstract canonical model over any set of axioms and formalize completeness-via-canonicity: when the canonical model for the chosen axioms belongs to a certain class of frames, strong completeness over that class follows immediately. I instantiate the result with logics based on various epistemic principles to obtain completeness results for systems from K to S5. I then move to a family of public announcement logics (PAL) and prove abstract results for strong soundness and completeness. I lift the completeness results from epistemic logic to the setting with public announcements in a modular way. This work formulates the completeness-via-canonicity technique as a proper theorem and demonstrates its applicability. Additionally, it succinctly formalizes the requirements for lifting completeness from bare epistemic logic to the addition of public announcements.

@article{From24,
abstract = {{I strengthen the foundations of epistemic logic by formalizing the family of normal modal logics in the proof assistant Isabelle/HOL. I define an abstract canonical model over any set of axioms and formalize completeness-via-canonicity: when the canonical model for the chosen axioms belongs to a certain class of frames, strong completeness over that class follows immediately. I instantiate the result with logics based on various epistemic principles to obtain completeness results for systems from K to S5. I then move to a family of public announcement logics (PAL) and prove abstract results for strong soundness and completeness. I lift the completeness results from epistemic logic to the setting with public announcements in a modular way. This work formulates the completeness-via-canonicity technique as a proper theorem and demonstrates its applicability. Additionally, it succinctly formalizes the requirements for lifting completeness from bare epistemic logic to the addition of public announcements.}},
author = {From, Asta Halkjær},
doi = {10.1093/logcom/exae054},
issn = {0955-792X},
journal = {Journal of Logic and Computation},
month = {09},
title = {{Formalized soundness and completeness of epistemic and public announcement logic}},
year = {2024},
}

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.

@article{FromJ24,
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.},
author = {Asta Halkj{æ}r From and Frederik Krogsdal Jacobsen},
doi = {10.1007/s10817-024-09697-3},
journal = {Journal of Automated Reasoning},
number = {15},
publisher = {Springer},
title = {Verifying a Sequent Calculus Prover for First-Order Logic with Functions in {Isabelle/HOL}},
volume = {68},
year = {2024},
}

The analytic technique for proving completeness gives a very operational perspective: build a countermodel to the unproved formula from a failed proof attempt in your calculus. We have to be careful, however, that the proof attempt did not fail because our strategy in finding it was flawed. Overcoming this concern requires designing a prover. We design and formalize in Isabelle/HOL a sequent calculus prover for first-order logic with functions. We formalize soundness and completeness theorems using an existing framework and extract executable code to Haskell. The crucial idea is to move complexity from the prover itself to a stream of instructions that it follows. The result serves as a minimal example of the analytic technique, a naive prover for first-order logic, and a case study in formal verification.

@inproceedings{FromV23,
abstract = {The analytic technique for proving completeness gives a very operational perspective: build a countermodel to the unproved formula from a failed proof attempt in your calculus. We have to be careful, however, that the proof attempt did not fail because our strategy in finding it was flawed. Overcoming this concern requires designing a prover. We design and formalize in Isabelle/HOL a sequent calculus prover for first-order logic with functions. We formalize soundness and completeness theorems using an existing framework and extract executable code to Haskell. The crucial idea is to move complexity from the prover itself to a stream of instructions that it follows. The result serves as a minimal example of the analytic technique, a naive prover for first-order logic, and a case study in formal verification.},
author = {Asta Halkj{æ}r From and J{ø}rgen Villadsen},
booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods - 32nd International Conference, {TABLEAUX} 2023, Prague, Czech Republic, September 18-21, 2023, Proceedings},
doi = {10.1007/978-3-031-43513-3_25},
editor = {Revantha Ramanayake and Josef Urban},
pages = {468--480},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {A Naive Prover for First-Order Logic: {A} Minimal Example of Analytic Completeness},
volume = {14278},
year = {2023},
}

We formalize in Isabelle/HOL soundness and completeness of a one-sided sequent calculus for first-order logic. The completeness is shown via a translation from a semantic tableau calculus, whose completeness proof we base on the theory entry ‘First-Order Logic According to Fitting’ by Berghofer in the Archive of Formal Proofs. The calculi and proof techniques are taken from Ben-Ari’s textbook Mathematical Logic for Computer Science (Springer, 2012). We thereby demonstrate that Berghofer’s approach works not only for natural deduction but also constitutes a framework for mechanically checked completeness proofs for a range of proof systems.

@article{FromSV23,
abstract = {We formalize in Isabelle/HOL soundness and completeness of a one-sided sequent calculus for first-order logic. The completeness is shown via a translation from a semantic tableau calculus, whose completeness proof we base on the theory entry ‘First-Order Logic According to Fitting’ by Berghofer in the Archive of Formal Proofs. The calculi and proof techniques are taken from Ben-Ari’s textbook Mathematical Logic for Computer Science (Springer, 2012). We thereby demonstrate that Berghofer’s approach works not only for natural deduction but also constitutes a framework for mechanically checked completeness proofs for a range of proof systems.},
author = {Asta Halkj{æ}r From and Anders Schlichtkrull and J{ø}rgen Villadsen},
doi = {10.1093/logcom/exad013},
journal = {Journal of Logic and Computation},
number = {4},
pages = {818--836},
title = {A sequent calculus for first-order logic formalized in {Isabelle/HOL}},
volume = {33},
year = {2023},
}

We consider a plethora of well-known axiomatic systems, and some less well-known variants, for classical propositional logic all with soundness and completeness theorems formalized in the proof assistant Isabelle/HOL. We have previously only formalized systems based on either implication and falsity or on disjunction and negation. We have now formalized 12 additional systems based on implication and negation. Each of them has three or more axioms. We have also formalized single-axiom systems, by Lukasiewicz and Tarski as well as by Meredith, and we describe the formalization of the former in detail. A few systems with two axioms are described too.

@inbook{EschenFV23,
abstract = {We consider a plethora of well-known axiomatic systems, and some less well-known variants, for classical propositional logic all with soundness and completeness theorems formalized in the proof assistant Isabelle/HOL. We have previously only formalized systems based on either implication and falsity or on disjunction and negation. We have now formalized 12 additional systems based on implication and negation. Each of them has three or more axioms. We have also formalized single-axiom systems, by Lukasiewicz and Tarski as well as by Meredith, and we describe the formalization of the former in detail. A few systems with two axioms are described too.},
address = {Chisinau},
author = {Agnes Moesg{å}rd Eschen and Asta Halkj{æ}r From and J{ø}rgen Villadsen},
booktitle = {Logic and Artificial Intelligence},
editor = {Svetlana Cojocaru and Ioachim Drugus and Mykola Nikitchenco and Alexei Muravitsky},
isbn = {978-9975-68-484-2},
pages = {7--22},
publisher = {Vladimir Andrunachievici Institute of Mathematics and Computer Science},
title = {More Formalized Axiomatic Systems for Propositional Logic in {Isabelle/HOL}},
url = {https://slai2022.islai.org/proceedings/},
year = {2023},
}

We present Aesop, a proof search tactic for the Lean 4 interactive theorem prover. Aesop performs a tree-based search over a user-specified set of proof rules. It supports safe and unsafe rules and uses a best-first search strategy with customisable prioritisation. Aesop also allows users to register custom normalisation rules and integrates Lean's simplifier to support equational reasoning. Many details of Aesop's search procedure are designed to make it a white-box proof automation tactic, meaning that users should be able to easily predict how their rules will be applied, and thus how powerful and fast their Aesop invocations will be. Since we use a best-first search strategy, it is not obvious how to handle metavariables which appear in multiple goals. The most common strategy for dealing with metavariables relies on backtracking and is therefore not suitable for best-first search. We give an algorithm which addresses this issue. The algorithm works with any search strategy, is independent of the underlying logic and makes few assumptions about how rules interact with metavariables. We conjecture that with a fair search strategy, the algorithm is as complete as the given set of rules allows.

@inproceedings{LimpergF23,
abstract = {We present Aesop, a proof search tactic for the Lean 4 interactive theorem prover. Aesop performs a tree-based search over a user-specified set of proof rules. It supports safe and unsafe rules and uses a best-first search strategy with customisable prioritisation. Aesop also allows users to register custom normalisation rules and integrates Lean's simplifier to support equational reasoning. Many details of Aesop's search procedure are designed to make it a white-box proof automation tactic, meaning that users should be able to easily predict how their rules will be applied, and thus how powerful and fast their Aesop invocations will be. Since we use a best-first search strategy, it is not obvious how to handle metavariables which appear in multiple goals. The most common strategy for dealing with metavariables relies on backtracking and is therefore not suitable for best-first search. We give an algorithm which addresses this issue. The algorithm works with any search strategy, is independent of the underlying logic and makes few assumptions about how rules interact with metavariables. We conjecture that with a fair search strategy, the algorithm is as complete as the given set of rules allows.},
author = {Jannis Limperg and Asta Halkj{æ}r From},
booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, {CPP} 2023, Boston, MA, USA, January 16-17, 2023},
doi = {10.1145/3573105.3575671},
editor = {Robbert Krebbers and Dmitriy Traytel and Brigitte Pientka and Steve Zdancewic},
pages = {253--266},
publisher = {{ACM}},
title = {Aesop: White-Box Best-First Proof Search for Lean},
year = {2023},
}

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.

@inproceedings{FromJ22,
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.},
author = {Asta Halkj{æ}r From and Frederik Krogsdal Jacobsen},
booktitle = {13th International Conference on Interactive Theorem Proving, {ITP} 2022, August 7-10, 2022, Haifa, Israel},
doi = {10.4230/LIPIcs.ITP.2022.13},
editor = {June Andronick and Leonardo de Moura},
pages = {13:1--13:22},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{ü}r Informatik},
series = {LIPIcs},
title = {Verifying a Sequent Calculus Prover for First-Order Logic with Functions in {Isabelle/HOL}},
volume = {237},
year = {2022},
}

We discuss human and mechanized reasoning with regards to the use of proof assistants, in particular Isabelle/HOL. We use the development of novel NAND- and NOR-based micro provers as a case study. Current, widely available automated reasoning technology is suitable for assisting humans with certain types of reasoning, like finding proofs for well-defined theorems. Other types of reasoning, like the discovery of new theorems, are notoriously difficult for mechanized reasoning. Our case study indicates that proof assistants are well suited as development tools for assuredly correct programs in languages like Haskell.

@inproceedings{FromLV22,
abstract = {We discuss human and mechanized reasoning with regards to the use of proof assistants, in particular Isabelle/HOL. We use the development of novel NAND- and NOR-based micro provers as a case study. Current, widely available automated reasoning technology is suitable for assisting humans with certain types of reasoning, like finding proofs for well-defined theorems. Other types of reasoning, like the discovery of new theorems, are notoriously difficult for mechanized reasoning. Our case study indicates that proof assistants are well suited as development tools for assuredly correct programs in languages like Haskell.},
address = {Cham},
author = {From, Asta Halkj{æ}r and Lund, Simon Tobias and Villadsen, J{ø}rgen},
booktitle = {Distributed Computing and Artificial Intelligence, Volume 2: Special Sessions 18th International Conference},
doi = {10.1007/978-3-030-86887-1_5},
editor = {Gonz{á}lez, Sara Rodr{í}guez and Machado, Jos{é} Manuel and Gonz{á}lez-Briones, Alfonso and Wikarek, Jaroslaw and Loukanova, Roussanka and Katranas, George and Casado-Vara, Roberto},
isbn = {978-3-030-86887-1},
pages = {53--63},
publisher = {Springer International Publishing},
series = {Lecture Notes in Networks and Systems},
title = {A Case Study in Computer-Assisted Meta-reasoning},
volume = {332},
year = {2022},
}

Automated reasoning is the study of computer programs that can build proofs of theorems in a logic. Such programs can be either automatic theorem provers or interactive theorem provers. The latter are also called proof assistants because the user constructs the proofs with the help of the system. We focus on the Isabelle proof assistant. The system ensures that the proofs are correct, in contrast to pen-and-paper proofs which must be checked manually. We present applications to logical systems and models of information, in particular selected modal logics extending classical propositional logic. Epistemic logic allows intelligent systems to reason about the knowledge of agents. Public announcements can change the knowledge of the system and its agents. In order to account for this, epistemic logic can be extended to public announcement logic. An axiomatic system consists of axioms and rules of inference for deriving statements in a logic. Sound systems can only derive valid statements and complete systems can derive all valid statements. We describe formalizations of sound and complete axiomatic systems for epistemic logic and public announcement logic, thereby strengthening the foundations of automated reasoning for logic and information.

@inbook{VilladsenFJS22,
abstract = {Automated reasoning is the study of computer programs that can build proofs of theorems in a logic. Such programs can be either automatic theorem provers or interactive theorem provers. The latter are also called proof assistants because the user constructs the proofs with the help of the system. We focus on the Isabelle proof assistant. The system ensures that the proofs are correct, in contrast to pen-and-paper proofs which must be checked manually. We present applications to logical systems and models of information, in particular selected modal logics extending classical propositional logic. Epistemic logic allows intelligent systems to reason about the knowledge of agents. Public announcements can change the knowledge of the system and its agents. In order to account for this, epistemic logic can be extended to public announcement logic. An axiomatic system consists of axioms and rules of inference for deriving statements in a logic. Sound systems can only derive valid statements and complete systems can derive all valid statements. We describe formalizations of sound and complete axiomatic systems for epistemic logic and public announcement logic, thereby strengthening the foundations of automated reasoning for logic and information.},
address = {Cham},
author = {Villadsen, J{ø}rgen and From, Asta Halkj{æ}r and Jensen, Alexander Birch and Schlichtkrull, Anders},
booktitle = {Natural Language Processing in Artificial Intelligence --- NLPinAI 2021},
doi = {10.1007/978-3-030-90138-7_2},
editor = {Loukanova, Roussanka},
isbn = {978-3-030-90138-7},
pages = {25--48},
publisher = {Springer International Publishing},
series = {Studies in Computational Intelligence},
title = {Interactive Theorem Proving for Logic and Information},
volume = {999},
year = {2022},
}

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.

@inproceedings{From21-TYPES,
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.},
author = {Asta Halkj{æ}r From},
booktitle = {27th International Conference on Types for Proofs and Programs, {TYPES} 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference)},
doi = {10.4230/LIPIcs.TYPES.2021.8},
editor = {Henning Basold and Jesper Cockx and Silvia Ghilezan},
pages = {8:1--8:24},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{ü}r Informatik},
series = {LIPIcs},
title = {A Succinct Formalization of the Completeness of First-Order Logic},
volume = {239},
year = {2021},
}

We strengthen the foundations of epistemic logic by formalizing the family of normal modal logics in the proof assistant Isabelle/HOL. We define an abstract canonical model and prove a truth lemma for any logic in the family. We then instantiate it with logics based on various epistemic principles to obtain completeness results for systems from K to S5. Our work gives a disciplined treatment of completeness-via-canonicity arguments and demonstrates their compositionality.

@inproceedings{From21-WoLLIC,
abstract = {We strengthen the foundations of epistemic logic by formalizing the family of normal modal logics in the proof assistant Isabelle/HOL. We define an abstract canonical model and prove a truth lemma for any logic in the family. We then instantiate it with logics based on various epistemic principles to obtain completeness results for systems from K to S5. Our work gives a disciplined treatment of completeness-via-canonicity arguments and demonstrates their compositionality.},
author = {Asta Halkj{æ}r From},
booktitle = {Logic, Language, Information, and Computation - 27th International Workshop, WoLLIC 2021, Virtual Event, October 5-8, 2021, Proceedings},
doi = {10.1007/978-3-030-88853-4_1},
editor = {Alexandra Silva and Renata Wassermann and Ruy J. G. B. de Queiroz},
pages = {1--15},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Formalized Soundness and Completeness of Epistemic Logic},
volume = {13038},
year = {2021},
}

I formalize a Henkin-style completeness proof for an axiomatic system for propositional logic in the proof assistant Isabelle/HOL. The formalization precisely details the structure of this proof method.

@inproceedings{From21-ESSLLI,
abstract = {I formalize a Henkin-style completeness proof for an axiomatic system for propositional logic in the proof assistant Isabelle/HOL. The formalization precisely details the structure of this proof method.},
author = {Asta Halkj{æ}r From},
booktitle = {Selected Reflections in Language, Logic, and Information - {ESSLLI} 2019, {ESSLLI} 2020 and {ESSLLI} 2021 Student Sessions, Selected Papers},
doi = {10.1007/978-3-031-50628-4_5},
editor = {Alexandra Pavlova and Mina Young Pedersen and Raffaella Bernardi},
pages = {80--92},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Formalizing Henkin-Style Completeness of an Axiomatic System for Propositional Logic},
volume = {14354},
year = {2021},
}

We formalize soundness and completeness proofs for a number of axiomatic systems for propositional logic in the proof assistant Isabelle/HOL.

@inproceedings{FromEV21,
abstract = {We formalize soundness and completeness proofs for a number of axiomatic systems for propositional logic in the proof assistant Isabelle/HOL.},
author = {Asta Halkj{æ}r From and Agnes Moesg{å}rd Eschen and J{ø}rgen Villadsen},
booktitle = {Intelligent Computer Mathematics - 14th International Conference, {CICM} 2021, Timisoara, Romania, July 26-31, 2021, Proceedings},
doi = {10.1007/978-3-030-81097-9_3},
editor = {Fairouz Kamareddine and Claudio Sacerdoti Coen},
pages = {32--46},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Formalizing Axiomatic Systems for Propositional Logic in {Isabelle/HOL}},
volume = {12833},
year = {2021},
}

We describe SeCaV, a sequent calculus verifier for first-order logic in Isabelle/HOL, and the SeCaV Unshortener, an online tool that expands succinct derivations into the full SeCaV syntax. We leverage the power of Isabelle/HOL as a proof checker for our SeCaV derivations. The interactive features of Isabelle/HOL make our system transparent. For instance, the user can simply click on a side condition to see its exact definition. Our formalized soundness and completeness proofs pertain exactly to the calculus as exposed to the user and not just to some model of our tool. Users can also write their derivations in the SeCaV Unshortener, which provides a lighter syntax, and expand them for later verification. We have used both tools in our teaching.

@inproceedings{FromJV21,
abstract = {We describe SeCaV, a sequent calculus verifier for first-order logic in Isabelle/HOL, and the SeCaV Unshortener, an online tool that expands succinct derivations into the full SeCaV syntax. We leverage the power of Isabelle/HOL as a proof checker for our SeCaV derivations. The interactive features of Isabelle/HOL make our system transparent. For instance, the user can simply click on a side condition to see its exact definition. Our formalized soundness and completeness proofs pertain exactly to the calculus as exposed to the user and not just to some model of our tool. Users can also write their derivations in the SeCaV Unshortener, which provides a lighter syntax, and expand them for later verification. We have used both tools in our teaching.},
author = {Asta Halkj{æ}r From and Frederik Krogsdal Jacobsen and J{ø}rgen Villadsen},
booktitle = {Proceedings 16th Logical and Semantic Frameworks with Applications, {LSFA} 2021, Buenos Aires, Argentina (Online), 23rd - 24th July, 2021},
doi = {10.4204/EPTCS.357.4},
editor = {Mauricio Ayala{-}Rinc{ó}n and Eduardo Bonelli},
pages = {38--55},
publisher = {Open Publishing Association},
series = {{EPTCS}},
title = {{SeCaV}: {A} Sequent Calculus Verifier in {Isabelle/HOL}},
volume = {357},
year = {2021},
}

We formalize in Isabelle/HOL soundness and completeness of a one-sided sequent calculus for first-order logic. The completeness is shown via a translation from a semantic tableau calculus, whose completeness proof we base on the theory entry “First-Order Logic According to Fitting” by Berghofer in the Archive of Formal Proofs (AFP). The calculi and proof techniques are taken from Ben-Ari’s textbook Mathematical Logic for Computer Science (Springer 2012). We thereby demonstrate that Berghofer’s approach works not only for natural deduction but constitutes a framework for mechanically-checked completeness proofs for a range of proof systems.

@inproceedings{FromSV21,
abstract = {We formalize in Isabelle/HOL soundness and completeness of a one-sided sequent calculus for first-order logic. The completeness is shown via a translation from a semantic tableau calculus, whose completeness proof we base on the theory entry “First-Order Logic According to Fitting” by Berghofer in the Archive of Formal Proofs (AFP). The calculi and proof techniques are taken from Ben-Ari’s textbook Mathematical Logic for Computer Science (Springer 2012). We thereby demonstrate that Berghofer’s approach works not only for natural deduction but constitutes a framework for mechanically-checked completeness proofs for a range of proof systems.},
author = {Asta Halkj{æ}r From and Anders Schlichtkrull and J{ø}rgen Villadsen},
booktitle = {Proceedings of the 36th Italian Conference on Computational Logic, Parma, Italy, September 7-9, 2021},
editor = {Stefania Monica and Federico Bergenti},
pages = {107--121},
publisher = {CEUR-WS.org},
series = {{CEUR} Workshop Proceedings},
title = {A Sequent Calculus for First-Order Logic Formalized in {Isabelle/HOL}},
url = {http://ceur-ws.org/Vol-3002/paper7.pdf},
volume = {3002},
year = {2021},
}

We describe a natural deduction formalization of intuitionistic and classical propositional logic in the Isabelle/Pure framework. In contrast to earlier work, where we explored the pedagogical benefits of using a deep embedding approach to logical modelling, here we employ a logical framework modelling. This gives rise to simple and natural teaching examples and we report on the role it played in teaching our Automated Reasoning course in 2020 and 2021.

@inproceedings{VilladsenFB21,
abstract = {We describe a natural deduction formalization of intuitionistic and classical propositional logic in the Isabelle/Pure framework. In contrast to earlier work, where we explored the pedagogical benefits of using a deep embedding approach to logical modelling, here we employ a logical framework modelling. This gives rise to simple and natural teaching examples and we report on the role it played in teaching our Automated Reasoning course in 2020 and 2021.},
author = {J{ø}rgen Villadsen and Asta Halkj{æ}r From and Patrick Blackburn},
booktitle = {Proceedings 10th International Workshop on Theorem Proving Components for Educational Software, ThEdu@CADE 2021, (Remote) Carnegie Mellon University, Pittsburgh, PA, United States, 11 July 2021},
doi = {10.4204/EPTCS.354.6},
editor = {Jo{ã}o Marcos and Walther Neuper and Pedro Quaresma},
pages = {71--85},
publisher = {Open Publishing Association},
series = {{EPTCS}},
title = {Teaching Intuitionistic and Classical Propositional Logic Using {Isabelle}},
volume = {354},
year = {2021},
}

We outline benefits of formalizing a proof system for hybrid logic in the proof assistant Isabelle/HOL, showcase how the process of formalization can shape our proofs, and describe our current work on formalizing completeness of a more restrictive system. Formalization: https://devel.isa-afp.org/entries/Hybrid_Logic.html

@inproceedings{From20-AiML,
abstract = {We outline benefits of formalizing a proof system for hybrid logic in the proof assistant Isabelle/HOL, showcase how the process of formalization can shape our proofs, and describe our current work on formalizing completeness of a more restrictive system. Formalization: https://devel.isa-afp.org/entries/Hybrid\_Logic.html},
author = {Asta Halkj{æ}r From},
booktitle = {Short Papers: Advances in Modal Logic (AiML)},
editor = {Nicola Olivetti and Rinke Verbrugge},
pages = {23--27},
title = {Hybrid logic in the Isabelle Proof Assistant: Benefits, Challenges and the Road Ahead},
url = {https://archive.org/details/aiml2020shortpapers.pdf},
year = {2020},
}

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.

@inproceedings{From20-TYPES,
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.},
author = {Asta Halkj{æ}r From},
booktitle = {26th International Conference on Types for Proofs and Programs, {TYPES} 2020, March 2-5, 2020, University of Turin, Italy},
doi = {10.4230/LIPIcs.TYPES.2020.5},
editor = {Ugo de'Liguoro and Stefano Berardi and Thorsten Altenkirch},
pages = {5:1--5:17},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{ü}r Informatik},
series = {LIPIcs},
title = {Synthetic Completeness for a Terminating {Seligman}-Style Tableau System},
volume = {188},
year = {2020},
}

Hybrid logic is modal logic enriched with names for worlds. We formalize soundness and completeness proofs for a Seligman-style tableau system for hybrid logic in the proof assistant Isabelle/HOL. The formalization shows how to lift certain rule restrictions, thereby simplifying the original un-formalized proof. Moreover, the completeness proof we formalize is synthetic which suggests we can extend this work to prove a wider range of results about hybrid logic.

@inproceedings{FromBV20,
abstract = {Hybrid logic is modal logic enriched with names for worlds. We formalize soundness and completeness proofs for a Seligman-style tableau system for hybrid logic in the proof assistant Isabelle/HOL. The formalization shows how to lift certain rule restrictions, thereby simplifying the original un-formalized proof. Moreover, the completeness proof we formalize is synthetic which suggests we can extend this work to prove a wider range of results about hybrid logic.},
author = {Asta Halkj{æ}r From and Patrick Blackburn and J{ø}rgen Villadsen},
booktitle = {Automated Reasoning - 10th International Joint Conference, {IJCAR} 2020, Paris, France, July 1-4, 2020, Proceedings, Part {I}},
doi = {10.1007/978-3-030-51074-9_27},
editor = {Nicolas Peltier and Viorica Sofronie{-}Stokkermans},
pages = {474--481},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Formalizing a {Seligman}-Style Tableau System for Hybrid Logic (Short Paper)},
volume = {12166},
year = {2020},
}

Proof assistants are important tools for teaching logic. We support this claim by discussing three formalizations in Isabelle/HOL used in a recent course on automated reasoning. The first is a formalization of System W (a system of classical propositional logic with only two primitive symbols), the second is the Natural Deduction Assistant (NaDeA), and the third is a one-sided sequent calculus that uses our Sequent Calculus Verifier (SeCaV). We describe each formalization in turn, concentrating on how we used them in our teaching, and commenting on features that are interesting or useful from a logic education perspective. In the conclusion, we reflect on the lessons learned and where they might lead us next.

@inproceedings{FromVB20,
abstract = {Proof assistants are important tools for teaching logic. We support this claim by discussing three formalizations in Isabelle/HOL used in a recent course on automated reasoning. The first is a formalization of System W (a system of classical propositional logic with only two primitive symbols), the second is the Natural Deduction Assistant (NaDeA), and the third is a one-sided sequent calculus that uses our Sequent Calculus Verifier (SeCaV). We describe each formalization in turn, concentrating on how we used them in our teaching, and commenting on features that are interesting or useful from a logic education perspective. In the conclusion, we reflect on the lessons learned and where they might lead us next.},
author = {Asta Halkj{æ}r From and J{ø}rgen Villadsen and Patrick Blackburn},
booktitle = {Proceedings 9th International Workshop on Theorem Proving Components for Educational Software, ThEdu@IJCAR 2020, Paris, France, 29th June 2020},
doi = {10.4204/EPTCS.328.2},
editor = {Pedro Quaresma and Walther Neuper and Jo{ã}o Marcos},
pages = {18--34},
publisher = {Open Publishing Association},
series = {{EPTCS}},
title = {{Isabelle/HOL} as a Meta-Language for Teaching Logic},
volume = {328},
year = {2020},
}

Classical first-order logic is in many ways central to work in mathematics, linguistics, computer science and artificial intelligence, so it is worthwhile to define it in full detail. We present soundness and completeness proofs of a sequent calculus for first-order logic, formalized in the interactive proof assistant Isabelle/HOL. Our formalization is based on work by Stefan Berghofer, which we have since updated to use Isabelle's declarative proof style Isar (Archive of Formal Proofs, Entry FOL-Fitting, August 2007 / July 2018). We represent variables with de Bruijn indices; this makes substitution under quantifiers less intuitive for a human reader. However, the nature of natural numbers yields an elegant solution when compared to implementations of substitution using variables represented by strings. The sequent calculus considered has the special property of an always empty antecedent and a list of formulas in the succedent. We obtain the proofs of soundness and completeness for the sequent calculus as a derived result of the inverse duality of its tableau counterpart. We strive to not only present the results of the proofs of soundness and completeness, but also to provide a deep dive into a programming-like approach to the formalization of first-order logic syntax, semantics and the sequent calculus. We use the formalization in a bachelor course on logic for computer science and discuss our experiences.

@inproceedings{FromJSV19,
abstract = {Classical first-order logic is in many ways central to work in mathematics, linguistics, computer science and artificial intelligence, so it is worthwhile to define it in full detail. We present soundness and completeness proofs of a sequent calculus for first-order logic, formalized in the interactive proof assistant Isabelle/HOL. Our formalization is based on work by Stefan Berghofer, which we have since updated to use Isabelle's declarative proof style Isar (Archive of Formal Proofs, Entry FOL-Fitting, August 2007 / July 2018). We represent variables with de Bruijn indices; this makes substitution under quantifiers less intuitive for a human reader. However, the nature of natural numbers yields an elegant solution when compared to implementations of substitution using variables represented by strings. The sequent calculus considered has the special property of an always empty antecedent and a list of formulas in the succedent. We obtain the proofs of soundness and completeness for the sequent calculus as a derived result of the inverse duality of its tableau counterpart. We strive to not only present the results of the proofs of soundness and completeness, but also to provide a deep dive into a programming-like approach to the formalization of first-order logic syntax, semantics and the sequent calculus. We use the formalization in a bachelor course on logic for computer science and discuss our experiences.},
author = {Asta Halkj{æ}r From and Alexander Birch Jensen and Anders Schlichtkrull and J{ø}rgen Villadsen},
booktitle = {Proceedings 8th International Workshop on Theorem Proving Components for Educational Software, ThEdu@CADE 2019, Natal, Brazil, 25th August 2019},
doi = {10.4204/EPTCS.313.5},
editor = {Pedro Quaresma and Walther Neuper and Jo{ã}o Marcos},
pages = {73--92},
publisher = {Open Publishing Association},
series = {{EPTCS}},
title = {Teaching a Formalized Logical Calculus},
volume = {313},
year = {2019},
}

The Students' Proof Assistant (SPA) aims to both teach how to use a proof assistant like Isabelle and also to teach how reliable proof assistants are built. Technically it is a miniature proof assistant inside the Isabelle proof assistant. In addition we conjecture that a good way to teach structured proving is with a concrete prover where the connection between semantics, proof system, and prover is clear. The proofs in Lamport's TLAPS proof assistant have a very similar structure to those in the declarative prover SPA. To illustrate this we compare a proof of Pelletier's problem 43 in TLAPS, Isabelle/Isar and SPA. We also consider Pelletier's problem 34, also known as Andrews's Challenge, where students are encouraged to develop their own justification function and thus obtain a lot of insight into the proof assistant. Although SPA is fully functional we have so far only used it in a few educational scenarios.

@inproceedings{SchlichtkrullVF18,
abstract = {The Students' Proof Assistant (SPA) aims to both teach how to use a proof assistant like Isabelle and also to teach how reliable proof assistants are built. Technically it is a miniature proof assistant inside the Isabelle proof assistant. In addition we conjecture that a good way to teach structured proving is with a concrete prover where the connection between semantics, proof system, and prover is clear. The proofs in Lamport's TLAPS proof assistant have a very similar structure to those in the declarative prover SPA. To illustrate this we compare a proof of Pelletier's problem 43 in TLAPS, Isabelle/Isar and SPA. We also consider Pelletier's problem 34, also known as Andrews's Challenge, where students are encouraged to develop their own justification function and thus obtain a lot of insight into the proof assistant. Although SPA is fully functional we have so far only used it in a few educational scenarios.},
author = {Anders Schlichtkrull and J{ø}rgen Villadsen and Asta Halkj{æ}r From},
booktitle = {Proceedings 7th International Workshop on Theorem proving components for Educational software, ThEdu@FLoC 2018, Oxford, United Kingdom, 18 july 2018},
doi = {10.4204/EPTCS.290.1},
editor = {Pedro Quaresma and Walther Neuper},
pages = {1--13},
publisher = {Open Publishing Association},
series = {{EPTCS}},
title = {Students' Proof Assistant {(SPA)}},
volume = {290},
year = {2018},
}

We present the Natural Deduction Assistant (NaDeA) and discuss its advantages and disadvantages as a tool for teaching logic. NaDeA is available online and is based on a formalization of natural deduction in the Isabelle proof assistant. We first provide concise formulations of the main formalization results. We then elaborate on the prerequisites for NaDeA, in particular we describe a formalization in Isabelle of "Hilbert's Axioms" that we use as a starting point in our bachelor course on mathematical logic. We discuss a recent evaluation of NaDeA and also give an overview of the exercises in NaDeA.

@inproceedings{VilladsenFS18,
abstract = {We present the Natural Deduction Assistant (NaDeA) and discuss its advantages and disadvantages as a tool for teaching logic. NaDeA is available online and is based on a formalization of natural deduction in the Isabelle proof assistant. We first provide concise formulations of the main formalization results. We then elaborate on the prerequisites for NaDeA, in particular we describe a formalization in Isabelle of "Hilbert's Axioms" that we use as a starting point in our bachelor course on mathematical logic. We discuss a recent evaluation of NaDeA and also give an overview of the exercises in NaDeA.},
author = {J{ø}rgen Villadsen and Asta Halkj{æ}r From and Anders Schlichtkrull},
booktitle = {Proceedings 7th International Workshop on Theorem proving components for Educational software, ThEdu@FLoC 2018, Oxford, United Kingdom, 18 july 2018},
doi = {10.4204/EPTCS.290.2},
editor = {Pedro Quaresma and Walther Neuper},
pages = {14--29},
publisher = {Open Publishing Association},
series = {{EPTCS}},
title = {{Natural Deduction Assistant (NaDeA)}},
volume = {290},
year = {2018},
}

We present a simple prover for first-order logic with certified soundness and completeness in Isabelle/HOL, taking formalizations by Tom Ridge and others as the starting point, but with the aim of using the approach for teaching logic and verification to computer science stu- dents at the bachelor level. The prover is simple in the following sense: It is purely functional and can be executed with rewriting rules or as code generation to a number of functional programming languages. The prover uses no higher-order functions, that is, no function takes a function as argument or returns a function as its result. This is advantageous when students perform rewriting steps by hand. The prover uses the logic of first-order logic on negation normal form with a term language consist- ing of only variables. This subset of the full syntax of first-order logic allows for a simple proof system without resorting to the much weaker propositional logic.

@inproceedings{VilladsenSF18,
abstract = {We present a simple prover for first-order logic with certified soundness and completeness in Isabelle/HOL, taking formalizations by Tom Ridge and others as the starting point, but with the aim of using the approach for teaching logic and verification to computer science stu- dents at the bachelor level. The prover is simple in the following sense: It is purely functional and can be executed with rewriting rules or as code generation to a number of functional programming languages. The prover uses no higher-order functions, that is, no function takes a function as argument or returns a function as its result. This is advantageous when students perform rewriting steps by hand. The prover uses the logic of first-order logic on negation normal form with a term language consist- ing of only variables. This subset of the full syntax of first-order logic allows for a simple proof system without resorting to the much weaker propositional logic.},
author = {J{ø}rgen Villadsen and Anders Schlichtkrull and Asta Halkj{æ}r From},
booktitle = {Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning co-located with Federated Logic Conference 2018 (FLoC 2018), Oxford, UK, July 19th, 2018},
editor = {Boris Konev and Josef Urban and Philipp R{ü}mmer},
pages = {88--104},
publisher = {CEUR-WS.org},
series = {{CEUR} Workshop Proceedings},
title = {A Verified Simple Prover for First-Order Logic},
url = {http://ceur-ws.org/Vol-2162/paper-08.pdf},
volume = {2162},
year = {2018},
}

We provide a detailed description of the Python-DTU system, including the overall system design and the tools used in the agent contest.

@article{VilladsenFJL18,
abstract = {We provide a detailed description of the Python-DTU system, including the overall system design and the tools used in the agent contest.},
author = {J{ø}rgen Villadsen and Asta Halkj{æ}r From and Salvador Jacobi and Nikolaj N{ø}kkentved Larsen},
doi = {10.1504/IJAOSE.2018.10010604},
journal = {International Journal of Agent-Oriented Software Engineering},
number = {1},
pages = {86--100},
title = {Multi-Agent Programming Contest 2016 --- The {Python-DTU} Team},
volume = {6},
year = {2018},
}

We provide a brief description of the Jason-DTU system, including the overall system design and the tools that we used in the Multi-Agent Programming Contest. We also provide a detailed evaluation of our system. The strengths of our system include dynamic assignment of agents to groups, enabling flexible use of agents according to the current situation. Our team performed overall very well and we won some matches by either a fairly big margin or closely.

@incollection{VilladsenBFHL18,
abstract = {We provide a brief description of the Jason-DTU system, including the overall system design and the tools that we used in the Multi-Agent Programming Contest. We also provide a detailed evaluation of our system. The strengths of our system include dynamic assignment of agents to groups, enabling flexible use of agents according to the current situation. Our team performed overall very well and we won some matches by either a fairly big margin or closely.},
author = {J{ø}rgen Villadsen and Mads Okholm Bj{ø}rn and Asta Halkj{æ}r From and Thomas S{ø}ren Henney and John Bruntse Larsen},
booktitle = {The Multi-Agent Programming Contest 2018 --- Agents Teaming Up in an Urban Environment},
doi = {10.1007/978-3-030-37959-9_3},
editor = {Tobias Ahlbrecht and J{ü}rgen Dix and Niklas Fiekas},
pages = {41--71},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Multi-Agent Programming Contest 2018 --- The {Jason-DTU} Team},
volume = {11957},
year = {2018},
}

We describe our Natural Deduction Assistant (NaDeA) and the interfaces between the Isabelle proof assistant and NaDeA. In particular, we explain how NaDeA, using a generated prover that has been verified in Isabelle, provides feedback to the student, and also how NaDeA, for each formula proved by the student, provides a generated theorem that can be verified in Isabelle.

@inproceedings{VilladsenFS17,
abstract = {We describe our Natural Deduction Assistant (NaDeA) and the interfaces between the Isabelle proof assistant and NaDeA. In particular, we explain how NaDeA, using a generated prover that has been verified in Isabelle, provides feedback to the student, and also how NaDeA, for each formula proved by the student, provides a generated theorem that can be verified in Isabelle.},
author = {J{ø}rgen Villadsen and Asta Halkj{æ}r From and Anders Schlichtkrull},
booktitle = {Proceedings 6th International Workshop on Theorem proving components for Educational software, ThEdu@CADE 2017, Gothenburg, Sweden, 6 Aug 2017},
doi = {10.4204/EPTCS.267.9},
editor = {Pedro Quaresma and Walther Neuper},
pages = {140--155},
publisher = {Open Publishing Association},
series = {{EPTCS}},
title = {Natural Deduction and the {Isabelle} Proof Assistant},
volume = {267},
year = {2017},
}

I sketch preliminary work on formalizing the termination of a tableau calculus for basic hybrid logic, whose soundness and completeness have already been formally verified. The formalization includes some crucial theorems, but omits others.

@unpublished{From22,
abstract = {I sketch preliminary work on formalizing the termination of a tableau calculus for basic hybrid logic, whose soundness and completeness have already been formally verified. The formalization includes some crucial theorems, but omits others.},
author = {Asta Halkjær From},
note = {Isabelle Workshop 2022},
title = {On Termination for Hybrid Tableaux},
url = {https://files.sketis.net/Isabelle_Workshop_2022/Isabelle_2022_paper_13.pdf},
year = {2022},
}

Epistemic logic allows reasoning about the knowledge of agents, and deductive proof systems enable this reasoning with a few axioms and inference rules. We strengthen the logical foundations of such a system by formalizing it in the proof assistant Isabelle/HOL. Our definitions are given in the precise language of higher-order logic and every step of our soundness and completeness proofs is mechanically checked.

@unpublished{FromJV21,
abstract = {Epistemic logic allows reasoning about the knowledge of agents, and deductive proof systems enable this reasoning with a few axioms and inference rules. We strengthen the logical foundations of such a system by formalizing it in the proof assistant Isabelle/HOL. Our definitions are given in the precise language of higher-order logic and every step of our soundness and completeness proofs is mechanically checked.},
author = {Asta Halkjær From and Alexander Birch Jensen and Jørgen Villadsen},
note = {LAMAS \& SR 2021, accepted abstract},
title = {Formalized Soundness and Completeness of Epistemic Logic},
url = {https://lamassr.github.io/editions/2021/papers/Formalized-Soundness.pdf},
year = {2021},
}

We describe novel axiomatic systems for classical propositional logic: one based on the K and S combinators and elimination rules and one on transitivity of implication, explosion and rules for disjunction. We show how Isabelle/HOL helps investigate such systems.

@unpublished{FromV21-TYPES,
abstract = {We describe novel axiomatic systems for classical propositional logic: one based on the K and S combinators and elimination rules and one on transitivity of implication, explosion and rules for disjunction. We show how Isabelle/HOL helps investigate such systems.},
author = {Asta Halkjær From and Jørgen Villadsen},
note = {TYPES 2021, accepted abstract},
title = {On the Use of Isabelle/HOL for Formalizing New Concise Axiomatic Systems for Classical Propositional Logic},
url = {https://types21.liacs.nl/download/on-the-use-of-isabelle-hol-for-formalizing-new-concise-axiomatic-systems-for-classical-propositional-logic/},
year = {2021},
}

We formalize two micro provers for propositional logic in Isabelle/HOL and Agda. The provers are used in an automated reasoning course at DTU where they concretize discussions of soundness and completeness. The students are familiar with functional programming beforehand but formalizing the provers, and other programs, introduces the students to formally verified functional programming in a proof assistant. Proofs that have been informal in previous courses, for instance of termination, can now be verified by the machine, and the provers provide practical examples. Similarly, the formal meta-languages provided by the formalizations clarify boundaries that can be muddled with pen and paper, for instance between syntactic and semantic arguments. We find that the automation available in Isabelle/HOL provides succinctness while the verification in Agda closer resembles functional programming.

@unpublished{FromV21-TFPIE,
abstract = {We formalize two micro provers for propositional logic in Isabelle/HOL and Agda. The provers are used in an automated reasoning course at DTU where they concretize discussions of soundness and completeness. The students are familiar with functional programming beforehand but formalizing the provers, and other programs, introduces the students to formally verified functional programming in a proof assistant. Proofs that have been informal in previous courses, for instance of termination, can now be verified by the machine, and the provers provide practical examples. Similarly, the formal meta-languages provided by the formalizations clarify boundaries that can be muddled with pen and paper, for instance between syntactic and semantic arguments. We find that the automation available in Isabelle/HOL provides succinctness while the verification in Agda closer resembles functional programming.},
author = {From, Asta Halkj{æ}r and Villadsen, J{ø}rgen},
note = {10th International Workshop on Trends in Functional Programming in Education (TFPIE 2021) --- Presentation Only/Online Papers},
title = {Teaching Automated Reasoning and Formally Verified Functional Programming in {Agda} and {Isabelle/HOL}},
url = {https://wiki.tfpie.science.ru.nl/images/a/a6/TFPIE_AHF_JV.pdf},
year = {2021},
}

We have formalized soundness and completeness for a sequent calculus for classical first- order 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.

@unpublished{FromV20,
abstract = {We have formalized soundness and completeness for a sequent calculus for classical first- order 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.},
author = {Asta Halkjær From and Jørgen Villadsen},
note = {Isabelle Workshop 2020},
title = {A Concise Sequent Calculus for Teaching First-Order Logic},
url = {https://files.sketis.net/Isabelle_Workshop_2020/Isabelle_2020_paper_6.pdf},
year = {2020},
}

@unpublished{From18,
author = {Asta Halkjær From},
note = {Scandinavian Logic Symposium 2018, accepted abstract},
title = {Formalized soundness and completeness of natural deduction for first-order logic},
url = {https://scandinavianlogic.org/assets/attachments/book_of_abstracts_sls2018.pdf#page=11},
year = {2018},
}

@unpublished{FromHV18,
author = {Asta Halkjær From and Helge Hatteland, and Jørgen Villadsen},
note = {Scandinavian Logic Symposium 2018, accepted abstract},
title = {Teaching first-order logic with the natural deduction assistant (NaDeA)},
url = {https://scandinavianlogic.org/assets/attachments/book_of_abstracts_sls2018.pdf#page=11},
year = {2018},
}

We formally prove in Isabelle/HOL two properties of an algorithm for laying out trees visually. The first property states that removing layout annotations recovers the original tree. The second property states that nodes are placed at least a unit of distance apart. We have yet to formalize three additional properties: That parents are centered above their children, that drawings are symmetrical with respect to reflection and that identical subtrees are rendered identically.

@unpublished{FromSV18,
abstract = {We formally prove in Isabelle/HOL two properties of an algorithm for laying out trees visually. The first property states that removing layout annotations recovers the original tree. The second property states that nodes are placed at least a unit of distance apart. We have yet to formalize three additional properties: That parents are centered above their children, that drawings are symmetrical with respect to reflection and that identical subtrees are rendered identically.},
author = {Asta Halkjær From and Anders Schlichtkrull and Jørgen Villadsen},
note = {Isabelle Workshop 2018},
title = {Drawing Trees},
url = {https://files.sketis.net/Isabelle_Workshop_2018/Isabelle_2018_paper_7.pdf},
year = {2018},
}

Substitution under quantifiers is non-trivial and may obscure a proof system for newcomers. Monk (Arch. Math. Log. Grundl. 1965) successfully eliminates substitution via identities and also uses a so-called normalization of formulas as a further simplification. We formalize the substitutionless proof system in Isabelle/HOL, spelling out its side conditions explicitly and verifying its soundness.

@unpublished{FromLSV18,
abstract = {Substitution under quantifiers is non-trivial and may obscure a proof system for newcomers. Monk (Arch. Math. Log. Grundl. 1965) successfully eliminates substitution via identities and also uses a so-called normalization of formulas as a further simplification. We formalize the substitutionless proof system in Isabelle/HOL, spelling out its side conditions explicitly and verifying its soundness.},
author = {Asta Halkjær From and John Bruntse Larsen and Anders Schlichtkrull and Jørgen Villadsen},
note = {Isabelle Workshop 2018.},
title = {Substitutionless First-Order Logic: A Formal Soundness Proof},
url = {https://files.sketis.net/Isabelle_Workshop_2018/Isabelle_2018_paper_3.pdf},
year = {2018},
}

We present Standard ML code generation in Isabelle/HOL of a sound and complete prover for first-order logic, taking formalizations by Tom Ridge and others as the starting point. We also define a set of so-called unfolding rules and show how to use these as a simple prover, with the aim of using the approach for teaching logic and verification to computer science students at the bachelor level.

@unpublished{VilladsenSF16,
abstract = {We present Standard ML code generation in Isabelle/HOL of a sound and complete prover for first-order logic, taking formalizations by Tom Ridge and others as the starting point. We also define a set of so-called unfolding rules and show how to use these as a simple prover, with the aim of using the approach for teaching logic and verification to computer science students at the bachelor level.},
author = {Jørgen Villadsen and Anders Schlichtkrull and Asta Halkjær From},
note = {Isabelle Workshop 2016},
title = {Code Generation for a Simple First-Order Prover},
url = {https://web.archive.org/web/20220121022845/https://www21.in.tum.de/~nipkow/Isabelle2016/Isabelle2016_12.pdf},
year = {2016},
}

In this work, I provide an abstract framework for proving the completeness of a logical calculus using the synthetic method. The synthetic method is based on maximal consistent saturated sets (MCSs). A set of formulas is consistent (with respect to the calculus) when we cannot derive a contradiction from it. It is maximally consistent when it contains every formula that is consistent with it. For logics where it is relevant, it is saturated when it contains a witness for every existential formula. To prove completeness using these maximal consistent saturated sets, we prove a truth lemma: every formula in an MCS has a satisfying model. Here, Hintikka sets provide a useful stepping stone. These can be seen as characterizations of the MCSs based on simple subformula conditions rather than via the calculus. We then prove that every Hintikka set gives rise to a satisfying model and that MCSs are Hintikka sets. Now, assume a valid formula cannot be derived. Then its negation must be consistent and therefore satisfiable. This contradicts validity and the original formula must be derivable. To start, I build maximal consistent saturated sets for any logic that satisfies a small set of assumptions. I do this using a transfinite version of Lindenbaum's lemma, which allows me to support languages of any cardinality. I then prove useful abstract results about derivations and refutations as they relate to MCSs. Finally, I show how Hintikka sets can be derived from the logic's semantics, outlining one way to prove the required truth lemma. To demonstrate the versatility of the framework, I instantiate it with five different examples. The formalization contains soundness and completeness results for: a propositional tableau calculus, a propositional sequent calculus, an axiomatic system for modal logic, a labelled natural deduction system for hybrid logic and a natural deduction system for first-order logic. The tableau example uses custom Hintikka sets based on the calculus, but the other four examples derive them from the semantics in the style of the framework. The hybrid and first-order logic examples rely on saturated MCSs. This places requirements on the cardinalities of their languages to ensure that there are enough witnesses available. In both cases, the type of witnesses must be infinite and have cardinality at least that of the type of propositional/predicate symbols.

@article{Synthetic_Completeness-AFP,
abstract = {In this work, I provide an abstract framework for proving the completeness of a logical calculus using the synthetic method. The synthetic method is based on maximal consistent saturated sets (MCSs). A set of formulas is consistent (with respect to the calculus) when we cannot derive a contradiction from it. It is maximally consistent when it contains every formula that is consistent with it. For logics where it is relevant, it is saturated when it contains a witness for every existential formula. To prove completeness using these maximal consistent saturated sets, we prove a truth lemma: every formula in an MCS has a satisfying model. Here, Hintikka sets provide a useful stepping stone. These can be seen as characterizations of the MCSs based on simple subformula conditions rather than via the calculus. We then prove that every Hintikka set gives rise to a satisfying model and that MCSs are Hintikka sets. Now, assume a valid formula cannot be derived. Then its negation must be consistent and therefore satisfiable. This contradicts validity and the original formula must be derivable. To start, I build maximal consistent saturated sets for any logic that satisfies a small set of assumptions. I do this using a transfinite version of Lindenbaum's lemma, which allows me to support languages of any cardinality. I then prove useful abstract results about derivations and refutations as they relate to MCSs. Finally, I show how Hintikka sets can be derived from the logic's semantics, outlining one way to prove the required truth lemma. To demonstrate the versatility of the framework, I instantiate it with five different examples. The formalization contains soundness and completeness results for: a propositional tableau calculus, a propositional sequent calculus, an axiomatic system for modal logic, a labelled natural deduction system for hybrid logic and a natural deduction system for first-order logic. The tableau example uses custom Hintikka sets based on the calculus, but the other four examples derive them from the semantics in the style of the framework. The hybrid and first-order logic examples rely on saturated MCSs. This places requirements on the cardinalities of their languages to ensure that there are enough witnesses available. In both cases, the type of witnesses must be infinite and have cardinality at least that of the type of propositional/predicate symbols.},
author = {Asta Halkjær From},
issn = {2150-914x},
journal = {Archive of Formal Proofs},
month = {January},
title = {Synthetic Completeness},
url = {https://isa-afp.org/entries/Synthetic_Completeness.html},
year = {2023},
}

This work is a formalization of soundness and completeness of the Bernays-Tarski axiom system for classical implicational logic. The completeness proof is constructive following the approach by László Kalmár, Elliott Mendelson and others. The result can be extended to full classical propositional logic by uncommenting a few lines for falsehood.

@article{Implicational_Logic-AFP,
abstract = {This work is a formalization of soundness and completeness of the Bernays-Tarski axiom system for classical implicational logic. The completeness proof is constructive following the approach by László Kalmár, Elliott Mendelson and others. The result can be extended to full classical propositional logic by uncommenting a few lines for falsehood.},
author = {Asta Halkjær From and Jørgen Villadsen},
issn = {2150-914x},
journal = {Archive of Formal Proofs},
month = {September},
title = {Soundness and Completeness of Implicational Logic},
url = {https://isa-afp.org/entries/Implicational_Logic.html},
year = {2022},
}

The AFP entry Abstract Completeness by Blanchette, Popescu and Traytel formalizes the core of Beth/Hintikka-style completeness proofs for first-order logic and can be used to formalize executable sequent calculus provers. In the Journal of Automated Reasoning, the authors instantiate the framework with a sequent calculus for first-order logic and prove its completeness. Their use of an infinite set of proof rules indexed by formulas yields very direct arguments. A fair stream of these rules controls the prover, making its definition remarkably simple. The AFP entry, however, only contains a toy example for propositional logic. The AFP entry A Sequent Calculus Prover for First-Order Logic with Functions by From and Jacobsen also uses the framework, but uses a finite set of generic rules resulting in a more sophisticated prover with more complicated proofs. This entry contains an executable sequent calculus prover for first-order logic with functions in the style presented by Blanchette et al. The prover can be exported to Haskell and this entry includes formalized proofs of its soundness and completeness. The proofs are simpler than those for the prover by From and Jacobsen but the performance of the prover is significantly worse. The included theory Fair-Stream first proves that the sequence of natural numbers 0, 0, 1, 0, 1, 2, etc. is fair. It then proves that mapping any surjective function across the sequence preserves fairness. This method of obtaining a fair stream of rules is similar to the one given by Blanchette et al. The concrete functions from natural numbers to terms, formulas and rules are defined using the Nat-Bijection theory in the HOL-Library.

@article{FOL_Seq_Calc3-AFP,
abstract = { The AFP entry Abstract Completeness by Blanchette, Popescu and Traytel formalizes the core of Beth/Hintikka-style completeness proofs for first-order logic and can be used to formalize executable sequent calculus provers. In the Journal of Automated Reasoning, the authors instantiate the framework with a sequent calculus for first-order logic and prove its completeness. Their use of an infinite set of proof rules indexed by formulas yields very direct arguments. A fair stream of these rules controls the prover, making its definition remarkably simple. The AFP entry, however, only contains a toy example for propositional logic. The AFP entry A Sequent Calculus Prover for First-Order Logic with Functions by From and Jacobsen also uses the framework, but uses a finite set of generic rules resulting in a more sophisticated prover with more complicated proofs. This entry contains an executable sequent calculus prover for first-order logic with functions in the style presented by Blanchette et al. The prover can be exported to Haskell and this entry includes formalized proofs of its soundness and completeness. The proofs are simpler than those for the prover by From and Jacobsen but the performance of the prover is significantly worse. The included theory Fair-Stream first proves that the sequence of natural numbers 0, 0, 1, 0, 1, 2, etc. is fair. It then proves that mapping any surjective function across the sequence preserves fairness. This method of obtaining a fair stream of rules is similar to the one given by Blanchette et al. The concrete functions from natural numbers to terms, formulas and rules are defined using the Nat-Bijection theory in the HOL-Library. },
author = {Asta Halkjær From},
issn = {2150-914x},
journal = {Archive of Formal Proofs},
month = {March},
title = {A Naive Prover for First-Order Logic},
url = {https://isa-afp.org/entries/FOL_Seq_Calc3.html},
year = {2022},
}

We formalize an automated theorem prover for first-order logic with functions. The proof search procedure is based on sequent calculus and we verify its soundness and completeness using the Abstract Soundness and Abstract Completeness theories. 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. We formally connect our prover with the proof system and semantics of the existing SeCaV system. In particular, the prover's output can be post-processed in Haskell to generate human-readable SeCaV proofs which are also machine-verifiable proof certificates. Paper: doi.org/10.4230/LIPIcs.ITP.2022.13.

@article{FOL_Seq_Calc2-AFP,
abstract = {We formalize an automated theorem prover for first-order logic with functions. The proof search procedure is based on sequent calculus and we verify its soundness and completeness using the Abstract Soundness and Abstract Completeness theories. 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. We formally connect our prover with the proof system and semantics of the existing SeCaV system. In particular, the prover's output can be post-processed in Haskell to generate human-readable SeCaV proofs which are also machine-verifiable proof certificates. Paper: doi.org/10.4230/LIPIcs.ITP.2022.13.},
author = {Asta Halkjær From and Frederik Krogsdal Jacobsen},
issn = {2150-914x},
journal = {Archive of Formal Proofs},
month = {January},
title = {A Sequent Calculus Prover for First-Order Logic with Functions},
url = {https://isa-afp.org/entries/FOL_Seq_Calc2.html},
year = {2022},
}

This work is a formalization of the soundness and completeness of an axiomatic system for first-order logic. The proof system is based on System Q1 by Smullyan and the completeness proof follows his textbook "First-Order Logic" (Springer-Verlag 1968). The completeness proof is in the Henkin style where a consistent set is extended to a maximal consistent set using Lindenbaum's construction and Henkin witnesses are added during the construction to ensure saturation as well. The resulting set is a Hintikka set which, by the model existence theorem, is satisfiable in the Herbrand universe. Paper: doi.org/10.4230/LIPIcs.TYPES.2021.8.

@article{FOL_Axiomatic-AFP,
abstract = {This work is a formalization of the soundness and completeness of an axiomatic system for first-order logic. The proof system is based on System Q1 by Smullyan and the completeness proof follows his textbook "First-Order Logic" (Springer-Verlag 1968). The completeness proof is in the Henkin style where a consistent set is extended to a maximal consistent set using Lindenbaum's construction and Henkin witnesses are added during the construction to ensure saturation as well. The resulting set is a Hintikka set which, by the model existence theorem, is satisfiable in the Herbrand universe. Paper: doi.org/10.4230/LIPIcs.TYPES.2021.8.},
author = {Asta Halkjær From},
issn = {2150-914x},
journal = {Archive of Formal Proofs},
month = {September},
title = {Soundness and Completeness of an Axiomatic System for First-Order Logic},
url = {https://isa-afp.org/entries/FOL_Axiomatic.html},
year = {2021},
}

This work is a formalization of public announcement logic with countably many agents. It includes proofs of soundness and completeness for a variant of the axiom system PA + DIST! + NEC!. The completeness proof builds on the Epistemic Logic theory. Paper: doi.org/10.1007/978-3-030-90138-7_2.

@article{Public_Announcement_Logic-AFP,
abstract = {This work is a formalization of public announcement logic with countably many agents. It includes proofs of soundness and completeness for a variant of the axiom system PA + DIST! + NEC!. The completeness proof builds on the Epistemic Logic theory. Paper: doi.org/10.1007/978-3-030-90138-7\_2.},
author = {Asta Halkjær From},
issn = {2150-914x},
journal = {Archive of Formal Proofs},
month = {June},
title = {Public Announcement Logic},
url = {https://isa-afp.org/entries/Public_Announcement_Logic.html},
year = {2021},
}

This work is a formalization of epistemic logic. It includes proofs of soundness and completeness for the axiom system K. The completeness proof is based on the textbook "Reasoning About Knowledge" by Fagin, Halpern, Moses and Vardi (MIT Press 1995). The extensions of system K (T, KB, K4, S4, S5) and their completeness proofs are based on the textbook "Modal Logic" by Blackburn, de Rijke and Venema (Cambridge University Press 2001). Papers: doi.org/10.1007/978-3-030-88853-4_1, doi.org/10.1007/978-3-030-90138-7_2.

@article{Epistemic_Logic-AFP,
abstract = {This work is a formalization of epistemic logic. It includes proofs of soundness and completeness for the axiom system K. The completeness proof is based on the textbook "Reasoning About Knowledge" by Fagin, Halpern, Moses and Vardi (MIT Press 1995). The extensions of system K (T, KB, K4, S4, S5) and their completeness proofs are based on the textbook "Modal Logic" by Blackburn, de Rijke and Venema (Cambridge University Press 2001). Papers: doi.org/10.1007/978-3-030-88853-4\_1, doi.org/10.1007/978-3-030-90138-7\_2.},
author = {Asta Halkjær From},
issn = {2150-914x},
journal = {Archive of Formal Proofs},
month = {October},
title = {Epistemic Logic: Completeness of Modal Logics},
url = {https://isa-afp.org/entries/Epistemic_Logic.html},
year = {2018},
}

This work is a formalization of soundness and completeness proofs for a Seligman-style tableau system for hybrid logic. The completeness result is obtained via a synthetic approach using maximally consistent sets of tableau blocks. The formalization differs from previous work in a few ways. First, to avoid the need to backtrack in the construction of a tableau, the formalized system has no unnamed initial segment, and therefore no Name rule. Second, I show that the full Bridge rule is admissible in the system. Third, I start from rules restricted to only extend the branch with new formulas, including only witnessing diamonds that are not already witnessed, and show that the unrestricted rules are admissible. Similarly, I start from simpler versions of the @-rules and show that these are sufficient. The GoTo rule is restricted using a notion of potential such that each application consumes potential and potential is earned through applications of the remaining rules. I show that if a branch can be closed then it can be closed starting from a single unit. Finally, Nom is restricted by a fixed set of allowed nominals. The resulting system should be terminating. Paper: doi.org/10.4230/LIPIcs.TYPES.2020.5.

@article{Hybrid_Logic-AFP,
abstract = {This work is a formalization of soundness and completeness proofs for a Seligman-style tableau system for hybrid logic. The completeness result is obtained via a synthetic approach using maximally consistent sets of tableau blocks. The formalization differs from previous work in a few ways. First, to avoid the need to backtrack in the construction of a tableau, the formalized system has no unnamed initial segment, and therefore no Name rule. Second, I show that the full Bridge rule is admissible in the system. Third, I start from rules restricted to only extend the branch with new formulas, including only witnessing diamonds that are not already witnessed, and show that the unrestricted rules are admissible. Similarly, I start from simpler versions of the @-rules and show that these are sufficient. The GoTo rule is restricted using a notion of potential such that each application consumes potential and potential is earned through applications of the remaining rules. I show that if a branch can be closed then it can be closed starting from a single unit. Finally, Nom is restricted by a fixed set of allowed nominals. The resulting system should be terminating. Paper: doi.org/10.4230/LIPIcs.TYPES.2020.5.},
author = {Asta Halkjær From},
issn = {2150-914x},
journal = {Archive of Formal Proofs},
month = {December},
title = {Formalizing a Seligman-Style Tableau System for Hybrid Logic},
url = {https://isa-afp.org/entries/Hybrid_Logic.html},
year = {2019},
}

This work formalizes soundness and completeness of a one-sided sequent calculus for first-order logic. The completeness is shown via a translation from a complete semantic tableau calculus, the proof of which is based on the First-Order Logic According to Fitting theory. The calculi and proof techniques are taken from Ben-Ari's Mathematical Logic for Computer Science. Paper: ceur-ws.org/Vol-3002/paper7.pdf.

@article{FOL_Seq_Calc1-AFP,
abstract = {This work formalizes soundness and completeness of a one-sided sequent calculus for first-order logic. The completeness is shown via a translation from a complete semantic tableau calculus, the proof of which is based on the First-Order Logic According to Fitting theory. The calculi and proof techniques are taken from Ben-Ari's Mathematical Logic for Computer Science. Paper: ceur-ws.org/Vol-3002/paper7.pdf.},
author = {Asta Halkjær From},
issn = {2150-914x},
journal = {Archive of Formal Proofs},
month = {July},
title = {A Sequent Calculus for First-Order Logic},
url = {https://isa-afp.org/entries/FOL_Seq_Calc1.html},
year = {2019},
}