Alexander Birch Jensen [dblp]
In August 2016 I obtained the MSc in Computer Science and Engineering degree on the Honours Programme at DTU (Technical University of Denmark).
I was a research assistant at DTU Compute from September 2016 to January 2017 and then I was a software developer at PDC A/S.
From February 2019 to February 2022 I am a PhD student at DTU Compute.
PhD Project: Logical Foundations of AI Algorithms
This project takes up the challenge of developing new AI algorithms with provable properties of functional correctness including safety, security, soundness, completeness and termination. Building upon recent advancements, the project strives to combine functional programming languages like SML, Haskell, OCaml and Scala with type systems and programming in the Isabelle proof assistant to achieve robust and efficient algorithms based on logical foundations.
Main supervisor: Jørgen Villadsen, DTU Compute - Algorithms, Logic and Graphs Section
Co-supervisor: Sebastian Mödersheim, DTU Compute - Formal Methods Section
Machine-Checked Verification of Cognitive Agents.
Alexander Birch Jensen.
In Proceedings of the 14th International Conference on Agents and Artificial Intelligence - Volume 1: ICAART (2022), SciTePress, p. 245-256.
Interactive Theorem Proving for Logic and Information.
Jørgen Villadsen, Asta Halkjær From, Alexander Birch Jensen & Anders Schlichtkrull.
Natural Language Processing in Artificial Intelligence - NLPinAI 2021, Springer SCI 999:25-48 (2021).
A Theorem Proving Approach to Formal Verification of a Cognitive Agent.
Alexander Birch Jensen.
DCAI 2021: Distributed Computing and Artificial Intelligence, Volume 1: 18th International Conference.
The 15th Edition of the Multi-Agent Programming Contest - The GOAL-DTU Team
Alexander Birch Jensen, Jørgen Villadsen, Jonas Weile & Erik Kristian Gylling.
The Multi-Agent Programming Contest 2021, Springer LNCS 12947:46-81 (2021).
Formal Verification of a Cognitive Agent Using Theorem Proving.
Alexander Birch Jensen.
9th International Workshop on Engineering Multi-Agent Systems (EMAS 2021), Springer, p. 1-11.
Formalized Soundness and Completeness of Epistemic Logic.
Asta Halkjær From, Alexander Birch Jensen & Jørgen Villadsen.
International Workshop on Logical Aspects in Multi-Agent Systems and Strategic Reasoning (LAMAS & SR 2021).
On Using Theorem Proving for Cognitive Agent-Oriented Programming.
Alexander Birch Jensen, Koen V. Hindriks & Jørgen Villadsen.
In Proceedings of the 13th International Conference on Agents and Artificial Intelligence - Volume 1: ICAART (2021), SciTePress, p. 337-344.
Towards Verifying GOAL Agents in Isabelle/HOL.
Alexander Birch Jensen.
In Proceedings of the 13th International Conference on Agents and Artificial Intelligence - Volume 1: ICAART (2021), SciTePress, p. 345-352.
Towards Verifying a Blocks World for Teams GOAL Agent.
Alexander Birch Jensen.
In Proceedings of the 13th International Conference on Agents and Artificial Intelligence - Volume 1: ICAART (2021), SciTePress, p. 446-453.
A Verification Framework for GOAL Agents.
Alexander Birch Jensen.
8th International Workshop on Engineering Multi-Agent Systems (EMAS 2020), 8-9 May 2020, Auckland, New Zealand.
GOAL-DTU: Development of Distributed Intelligence for the Multi-Agent Programming Contest.
Alexander Birch Jensen & Jørgen Villadsen.
The Multi-Agent Programming Contest 2019, Springer LNCS 12381:79-105 (2020).
Teaching a Formalized Logical Calculus.
Asta Halkjær From, Alexander Birch Jensen, Anders Schlichtkrull & Jørgen Villadsen.
8th International Workshop on Theorem Proving Components for Educational Software.
Electronic Proceedings in Theoretical Computer Science, vol: 313, 73-92 (2020).
Programming and Verifying a Declarative First-Order Prover in Isabelle/HOL.
Alexander Birch Jensen, John Bruntse Larsen, Anders Schlichtkrull & Jørgen Villadsen.
AI Communications 31:281-299 (2018).
First-Order Logic According to Harrison.
Alexander Birch Jensen, Anders Schlichtkrull & Jørgen Villadsen.
Archive of Formal Proofs - Isabelle Document 1-66 (2017).
NaDeA: A Natural Deduction Assistant with a Formalization in Isabelle.
Jørgen Villadsen, Alexander Birch Jensen & Anders Schlichtkrull.
IFCoLog Journal of Logics and their Applications 4:55-82 (2017).
Development and Verification of a Proof Assistant.
Alexander Birch Jensen.
Master's Thesis, Technical University of Denmark (2016).
Verification of an LCF-Style First-Order Prover with Equality.
Alexander Birch Jensen, Anders Schlichtkrull & Jørgen Villadsen.
Isabelle Workshop (2016).
The Multi-Agent Programming Contest 2020/2021.
March (2021) (postponed).
GOAL-DTU Team: Jørgen Villadsen, Alexander Birch Jensen, Jonas Weile, Benjamin Simon Stenbjerg Jepsen & Erik Kristian Gylling.
The Multi-Agent Programming Contest 2019.
October (2019).
GOAL-DTU Team: Jørgen Villadsen, Alexander Birch Jensen & Asta Halkjær From.
31st European Summer School in Logic, Language and Information (ESSLLI 2019).
University of Latvia.
August 5-16 (2019).
External Research Stay at VU Amsterdam.
Visited Jasmin Blanchette & Koen V. Hindriks.
June-July (2019).
Øresund Security Day 2019.
Technical University of Denmark.
May 22 (2019).
Engineering Reliable Multiagent Systems.
Dagstuhl Seminar 19112.
March 10–15 (2019).
Organizers: Jürgen Dix (TU Clausthal), Brian Logan (University of Nottingham), Michael Winikoff (University of Otago).
ICAART 2022
Machine-Checked Verification of Cognitive Agents
- Gvf_Logic.thy - Syntax and semantics of propositional logic.
- Gvf_Mental_States.thy - Mental states of agents: beliefs and goals.
- Gvf_Actions.thy - Agent actions and transitions between states.
- Gvf_Hoare_Logic.thy - Hoare logic for agent actions.
- Gvf_Agent_Specification.thy - Specification of agent programs.
- Gvf_Temporal_Logic.thy - Temporal logic for proving properties of agents.
- Gvf_Example_BW4T.thy - Correctness proof of an example agent.
DCAI 2021
A Theorem Proving Approach to Formal Verification of a Cognitive Agent *
- Gvf_Logic.thy - Formalization of classical logic framework.
- Gvf_PL.thy - Formalization of propositional logic instance.
- Gvf_Mental_States.thy - Formalization of cognitive aspects of agents.
- Gvf_Actions.thy - Formalization of actions for agents.
- Gvf_Hoare_Logic.thy - Formalization of Hoare logic for actions.
- Gvf_Agent_Specification.thy - Formalization of agent specification.
- Gvf_Example_BW4T.thy - Small specification example (experimental).
* This paper is a substantially extended and revised version of our short paper, in the student session with no proceedings, at EMAS 2021 (9th International Workshop on Engineering Multi-Agent Systems): Formal Verification of a Cognitive Agent Using Theorem Proving.
EMAS 2021
Formal Verification of a Cognitive Agent Using Theorem Proving
This short paper appears in the student session with no proceedings.
Our DCAI 2021 paper above: A Theorem Proving Approach to Formal Verification of a Cognitive Agent is a substantially extended and revised version of this short paper.
ICAART 2021
Towards Verifying a Blocks World for Teams GOAL Agent
- appendix.pdf - Appendix PDF.
- bw4t.mas2g - MAS configuration file.
- robotMain.mod2g - Main module.
- robotInit.mod2g - Initialization module.
- robotEvent.mod2g - Event module (perceive environment).
- robotActions.act2g - Action specification.
- robot.pl - Prolog knowledge base.
- TestMap - Test map configuration.
Towards Verifying GOAL Agents in Isabelle/HOL
- Gvf_PL.thy - Formalization of propositional logic.
- Gvf_GOAL.thy - Formalization of GOAL.