Asta (formerly Andreas) Halkjær From

Articles

• 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

• 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

• Formalizing Henkin-Style Completeness of an Axiomatic System for Propositional Logic
  at WeSSLLII + ESSLLI Virtual Student Session 2020
  Asta Halkjær From

  Proceedings: PDF

• A Concise Sequent Calculus for Teaching First-Order Logic at Isabelle Workshop 2020
  Asta Halkjær From, Jørgen Villadsen.

  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
  Talk: YouTube

• 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.

  Lecture Notes in Computer Science, vol 11957, pp. 41-71. Springer.
  Editors: Tobias Ahlbrecht, Jürgen Dix and Niklas Fiekas.

  DOI: 10.1007/978-3-030-37959-9_3

• A Verified Simple Prover for First-Order Logic at PAAR 2018
  Jørgen Villadsen, Anders Schlichtkrull, Andreas Halkjær From.

  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.

  PDF

• Drawing Trees at Isabelle Workshop 2018
  Andreas Halkjær From, Anders Schlichtkrull, Jørgen Villadsen.

  PDF, Isabelle theory

• Natural Deduction and the Isabelle Proof Assistant in ThEdu'17 post-proceedings
  Jørgen Villadsen, Andreas Halkjær From, Anders Schlichtkrull.

  Includes my work on translating online NaDeA proofs to the Isabelle encoding of the proof system.

  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.

  I did the initial work on the code used by the Python-DTU team for the Multi-Agent Programming Contest 2016.

  DOI: 10.1504/IJAOSE.2018.10010604

• Code Generation for a Simple First-Order Prover at Isabelle Workshop 2016
  Jørgen Villadsen, Anders Schlichtkrull, Andreas Halkjær From.

  PDF

Published formalizations

• Epistemic Logic: Completeness of Modal Logics in Archive of Formal Proofs (October 2018, updated April 2020)
  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).

  Website Outline (PDF) Theory

• Hybrid Logic in Archive of Formal Proofs (December 2019)
  Asta Halkjær From

  The formalization accompanying my MSc thesis.
  The development version contains the latest results.

  Website Outline (PDF) Main theory

• 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.

  Website Outline (PDF) Main theory

• IsaFoL: Isabelle Formalization of Logic

  I have contributed to a number of formalizations in the IsaFoL project:

  • First-Order Logic According to Berghofer
  • First-Order Logic According to Harrison
  • First-Order Logic According to Monk
  • Hybrid Logic
  • Simple Prover

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

  Abstract, Slides, Presentation, Zoom session

• Formalized Soundness and Completeness of Epistemic Logic at LAMAS & SR 2021
  Asta Halkjær From, Alexander Birch Jensen and Jørgen Villadsen

  Abstract, Slides

• Formalized soundness and completeness of natural deduction for first-order logic at SLS 2018
  Andreas Halkjær From.

  Abstract, Slides

• 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.

  Thesis, Slides

• BSc: Formalized First-Order Logic (July 2017)

  My BSc thesis on formalizing the soundness and completeness of NaDeA in Isabelle/HOL.

  Report, Slides (Danish)

Talks

• 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)

  Given at WeSSLLI + ESSLLI Virtual Student Session 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

• 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

Research Assistant