Asta (formerly Andreas) Halkjær
From
I am a PhD student at DTU Compute since February 2020 working on Formally Correct Deduction Methods for Computational Logic, especially using the proof assistant Isabelle/HOL. My supervisor is Jørgen Villadsen and my co-supervisor is Nina Gierasimczuk.
I was a MSc student on the Honours Programme in Computer Science and Engineering at DTU from 2018 to 2020. My MSc thesis on Hybrid Logic was supervised by Jørgen Villadsen, Alexander Birch Jensen and Patrick Blackburn.
Academic Activities
- Co-chair of the Logic and Computation track for the Student Session @ 32nd European Summer School in Logic, Language and Information (ESSLLI 2021).
Awards
- Travel scholarship awarded by DTU (February 2022).
Articles
-
SeCaV: A Sequent Calculus Verifier in Isabelle/HOL in
Proceedings 16th Logical and
Semantic Frameworks with Applications (LSFA 2021)
Asta Halkjær From, Frederik Krogsdal Jacobsen, Jørgen Villadsen.
DOI: 10.4204/EPTCS.357.4
-
Teaching Intuitionistic and Classical Propositional Logic Using Isabelle in
ThEdu'21 post-proceedings
Jørgen Villadsen, Asta Halkjær From, Patrick Blackburn.
DOI: 10.4204/EPTCS.354.6
-
Interactive Theorem Proving for Logic and Information in
Natural Language Processing
in Artificial Intelligence — NLPinAI 2021
Jørgen Villadsen, Asta Halkjær From, Alexander Birch Jensen, Anders Schlichtkrull.
DOI: 10.1007/978-3-030-90138-7_2
Formalizations: Epistemic Logic, Public Announcement Logic -
Formalized Soundness and Completeness of Epistemic Logic at
WoLLIC 2021
Asta Halkjær From.
DOI: 10.1007/978-3-030-88853-4_1
Formalization: Epistemic Logic -
A Sequent Calculus for First-Order Logic Formalized in Isabelle/HOL at
CILC 2021
Asta Halkjær From, Anders Schlichtkrull, Jørgen Villadsen.
CEUR-WS: PDF
Formalization: Sequent Calculus - A Case Study in Computer-Assisted Meta-reasoning at DCAI 2021, Special Session on Computational Linguistics, Information, Reasoning, and AI (CompLingInfoReasAI'21) Asta Halkjær From, Simon Tobias Lund, Jørgen Villadsen.
- Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL at Conference on Intelligent Computer Mathematics (CICM 2021) Asta Halkjær From, Agnes Moesgård Eschen, Jørgen Villadsen.
- Teaching Automated Reasoning and Formally Verified Functional Programming in Agda and Isabelle/HOL at 10th International Workshop on Trends in Functional Programming in Education (TFPIE 2021) Asta Halkjær From, Jørgen Villadsen.
-
Synthetic Completeness for a Terminating Seligman-Style Tableau System in
TYPES 2020 post-proceedings
Asta Halkjær From.
DOI: 10.4230/LIPIcs.TYPES.2020.5
Formalization: Hybrid Logic -
Isabelle/HOL as a Meta-Language for Teaching Logic in
ThEdu'20 post-proceedings
Asta Halkjær From, Jørgen Villadsen, Patrick Blackburn.
DOI: 10.4204/EPTCS.328.2
-
Hybrid Logic in the Isabelle Proof Assistant: Benefits, Challenges and the Road Ahead
(short paper) at AiML 2020
Asta Halkjær From
Booklet: PDF
Formalization: Hybrid Logic -
Formalizing Henkin-Style Completeness of an Axiomatic System for Propositional
Logic
at WeSSLLII + ESSLLI Virtual Student Session 2020 Asta Halkjær FromProceedings: PDF
-
A Concise Sequent Calculus for Teaching First-Order Logic at
Isabelle Workshop 2020
Asta Halkjær From, Jørgen Villadsen.
Paper: PDF
-
Formalizing a Seligman-Style Tableau System for Hybrid Logic (short paper) at
IJCAR 2020
Asta Halkjær From, Patrick Blackburn, Jørgen Villadsen.
DOI: 10.1007/978-3-030-51074-9_27
Formalization: Hybrid Logic -
Teaching a Formalized Logical Calculus in
ThEdu'19 post-proceedings
Asta Halkjær From, Alexander Birch Jensen, Anders Schlichtkrull, Jørgen Villadsen.
DOI: 10.4204/EPTCS.313.5
- Multi-Agent Programming Contest 2018 - The Jason-DTU Team Jørgen Villadsen, Mads Okholm Bjørn, Andreas Halkjær From, Thomas Søren Henney, John Bruntse Larsen.
-
A Verified Simple Prover for First-Order Logic at
PAAR 2018
Jørgen Villadsen, Anders Schlichtkrull, Andreas Halkjær From.
Paper: PDF
-
Students' Proof Assistant (SPA) in
ThEdu'18 post-proceedings
Anders Schlichtkrull, Jørgen Villadsen, Andreas Halkjær From.
DOI: 10.4204/EPTCS.290.1
-
Natural Deduction Assistant (NaDeA) in
ThEdu'18 post-proceedings
Jørgen Villadsen, Andreas Halkjær From, Anders Schlichtkrull.
DOI: 10.4204/EPTCS.290.2
-
Substitutionless First-Order Logic: A Formal Soundness Proof at
Isabelle Workshop 2018
Andreas Halkjær From, John Bruntse Larsen, Anders Schlichtkrull, Jørgen Villadsen.
Paper: PDF
-
Drawing Trees at
Isabelle Workshop 2018
Andreas Halkjær From, Anders Schlichtkrull, Jørgen Villadsen.
Paper: PDF, Formalization: Isabelle theory
-
Natural Deduction and the Isabelle Proof Assistant in
ThEdu'17 post-proceedings
Jørgen Villadsen, Andreas Halkjær From, Anders Schlichtkrull.
DOI: 10.4204/EPTCS.267.9
- Multi-Agent Programming Contest 2016 - The Python-DTU Team in IJAOSE 2018 Jørgen Villadsen, Andreas Halkjær From, Salvador Jacobi, Nikolaj Nøkkentved Larsen.
-
Code Generation for a Simple First-Order Prover at
Isabelle Workshop 2016
Jørgen Villadsen, Anders Schlichtkrull, Andreas Halkjær From.
Paper: PDF
Start of PhD
Published formalizations
-
A Naive Prover for First-Order Logic in
Archive of Formal Proofs (March 2022)
Asta Halkjær From
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.
-
A Sequent Calculus Prover for First-Order Logic with Functions in
Archive of Formal Proofs (February 2022)
Asta Halkjær From, Frederik Krogsdal Jacobsen
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.
-
Soundness and Completeness of an Axiomatic System for First-Order Logic in
Archive of Formal Proofs (October 2021)
Asta Halkjær From
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.
-
Public Announcement Logic in
Archive of Formal Proofs (June 2021)
Asta Halkjær From
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.
-
Epistemic Logic: Completeness of Modal Logics in
Archive of Formal Proofs (October 2018, updated April
2021)
Asta Halkjær From
This work is a formalization of epistemic logic with countably many agents. 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).
-
Hybrid Logic in
Archive of Formal Proofs (December 2019, updated June
2020)
Asta Halkjær From
The formalization accompanying my MSc thesis and TYPES 2020 paper.
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.
-
A Sequent Calculus for First-Order Logic in
Archive of Formal Proofs (July 2019)
Asta Halkjær From
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.
-
IsaFoL: Isabelle Formalization of Logic
I have contributed to a number of formalizations in the IsaFoL project:
Abstracts
- On the Use of Isabelle/HOL for Formalizing New Concise Axiomatic Systems for Classical Propositional Logic at TYPES 2021 Asta Halkjær From and Jørgen Villadsen
- Formalized Soundness and Completeness of Epistemic Logic at LAMAS & SR 2021 Asta Halkjær From, Alexander Birch Jensen and Jørgen Villadsen
- Formalized soundness and completeness of natural deduction for first-order logic at SLS 2018 Andreas Halkjær From.
- Teaching first-order logic with the natural deduction assistant (NaDeA) at SLS 2018 Andreas Halkjær From, Helge Hatteland, Jørgen Villadsen.
Theses
-
MSc: Hybrid Logic (January 2020)
My MSc thesis on formalizing the soundness and completeness of a Seligman-style tableau system for hybrid logic in Isabelle/HOL.
-
BSc: Formalized First-Order Logic (July 2017)
My BSc thesis on formalizing the soundness and completeness of NaDeA in Isabelle/HOL.
Talks
-
A Naive Prover for First-Order Logic - LSD Seminar (May 2022)
Invited talk at the Languages, Systems, and Data Seminar (Spring 2022).
-
A Naive Prover for First-Order Logic - 02256 (April 2022)
Guest talk in the course 02256 Automated Reasoning at the Technical University of Denmark.
-
Formalized Soundness and Completeness of Epistemic Logic (October 2021)
Given at WoLLIC 2021.
-
Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL (July 2021)
Given at CICM 2021.
-
Formalized Soundness and Completeness of Epistemic Logic (May 2021)
Given at LAMAS & SR 2021.
-
Hybrid Logic (January 2021)
Given at 3rd World Logic Day - 14 January 2021 - A Zoom on Logic.
-
Belief Revision and Isabelle/HOL (November 2020)
Given at a DTU seminar course.
-
Hybrid Logic in the Isabelle Proof Assistant: Benefits, Challenges and the Road Ahead
Given at AiML 2020.
-
Formally Correct Deduction Methods for Computational Logic (July 2020)
Given at CICM 2020 doctoral session.
-
Formalizing Henkin-Style Completeness of an Axiomatic System for Propositional Logic (July 2020)
-
Formalizing a Seligman-Style Tableau System for Hybrid Logic (July 2020)
Overview of our paper. Recording: YouTube. Given at IJCAR 2020.
-
A Concise Sequent Calculus for Teaching First-Order Logic (June 2020)
Overview of our paper. Recording: YouTube. Given at the Isabelle Workshop 2020.
-
The Isabelle Proof Assistant and Hybrid Logic: Formalizing Seligman-Style Tableaux (October 2019)
Update on my MSc thesis work. Given at an AlgoLoG seminar at DTU.
-
Using the Isabelle Proof Assistant: Seligman-Style Tableau for Hybrid Logic (September 2019)
The Isabelle proof assistant can be used to mechanically develop and check results in logic, mathematics, computer science etc. In this talk I motivate this process and explain how it looks in practice for a basic hybrid logic. The running example will be preliminary work on the completeness and termination for a Seligman-style tableau system by Blackburn, Bolander, Braüner and Jørgensen. Given at The LogicS of Prior Past, Present, and Future at Roskilde University.
-
Magnolia – Implementing System F with Anonymous Sums and Products (March 2018)
Overview of the Complete and Easy Bidirectional Type Checking for Higher-Rank Polymorphism paper as well as my own additions. Also briefly describes Abstract Binding Trees. Given at DTU.
-
FIT – From's Isabelle Tutorial – Verification of Quicksort (October 2017)
A fast-paced, hands-on introduction to Isabelle/HOL I gave at PART DTU.
Work Experience
Teaching Assistant
I have been a TA in the following courses:- 02101 Introductory Programming, fall 2015
- 02105 Algorithms and Data Structures 1, spring 2016
- 02101 Introductory Programming, fall 2016
- 02110 Algorithms and Data Structures 2, fall 2016
- 02105 Algorithms and Data Structures 1, spring 2017
- 02180 Introduction to Artificial Intelligence, spring 2018
- 02156 Logical Systems and Logic Programming, fall 2018
- 02156 Logical Systems and Logic Programming, fall 2019
- 02102 Introductory Programming, spring 2020
- 02256 Automated Reasoning, spring 2020
- 02287 Logical Theories for Uncertainty and Learning, fall 2020