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

Articles

Published formalizations

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

    Website, Outline (PDF), Theory

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

    Website, Outline (PDF), 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).

    Website, Outline (PDF), Theory

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

    Website, Outline (PDF), 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), Theory

  • 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

    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

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
I have also helped teach kids aged 9-12 years old game programming in MIT Scratch at Hello World.

Research Assistant

I worked as a research assistant at DTU Compute from August 2017 to December 2017, working with Isabelle and NaDeA, especially translating students' proofs in NaDeA to their encodings in Isabelle.