November 2021: A guest column about automation of non-classical logics,
authored by Claudia Nalon (Univ. of Brasilia) and myself, has been published in the
most recent edition of the AAR newsletter (Association for Automated Reasoning).
You can find the article in the
Newsletter No. 136.
November 2021: Our proposal for the next Workshop on Practical Aspects of Automated Reasoning (PAAR-2022) was accepted to take place at FLoC 2022 in Haifa, Isreal. PAAR-2022 will be co-chaired by Boris Konev (Liverpool University, UK), Claudia Schon (University of Koblenz-Landau, DE) and myself. PAAR-2022 is planned to take place on August 11 - 12, 2022. Details will follow soon.
November 2021: The AI Chapter of the German Informatics Society (GI), at which I'm a member of the board, published a statement against the usage of autonomous (lethal) weapons in Germany. See the context and statement at their website.
October 2021: Together with Max Rapp I will be serving as guest lecturer in Prof. Axel Adrian's seminar "Artificial Intelligence and legal argumentation" at the Department of Law at FAU University Erlangen-Nuremberg in November, focusing on the use of formal argumentation and automated reasoning in normative and legal contexts.
October 2021: I will be serving as vice leader of the working group on Automated Theorem Proving (WG2) of the COST action EuroProofNet. If you are interested to contribute to the goals of EuroProofNet, please register via e-COST.
August 2021: I was invited to join the upcoming Dagstuhl seminar on "Integrated Deduction" (Seminar 21371). Looking forward to it!
June 2021: I was invited to co-host, together with Prof. Cláudia Nalon (Univ. of Brasilia), a virtual discussion about automation aspects of non-classical logics at the reception of CADE-28. If you're interested, you are cordially invited to join on Monday, July 12, 3.30pm (EDT).
June 2021: I am happy to announce the launch of the new COST action EuroProofNet (CA20111). A COST action supports research exchanges and visits. Anyone willing to contribute to the goals of the action is eligible to join. If you are interested, please register via e-COST.
May 2021: I'm organizing a kick-off event of my recently started AuReLeE project, including invited talks by Prof. Adam Wyner (Swansea Univ.) and Prof. Leon van der Torre (Univ. of Luxembourg). Everybody is welcome to join, see aurelee.net/kickoff for more information.
May 2021: The Luxembourg National Research Fund (FNR) published a short feature on my research: Spotlight on Young Researchers: AI for ethical and legal debates. Thanks a lot for the interest!
April 2021: I'm happy to announce that the project proposal Höhere Ordnungen - performative Recherche zu Künstlicher Intelligenz of Benedikt Grubel and myself was accepted for funding by the Fond Darstellende Künste (federal Performing Arts Fund in Germany) within the #TakeCare programme. In this project, we will explore processes and notions of perception, knowledge representation and language that are common in Theater and AI.
March 2021: My article on extensional paramodulation in Leo-III (jww Christoph Benzmüller) was published in the Journal of Automated Reasoning. You can access the article on Springer Link.
February 2021: I was appointed an expert jury member for the selection of German AI talents (KI-Newcomer*innen 2021), an award hosted by the KI Camp project of the German BMBF and the Gesellschaft für Informatik. Looking forward to it!
November 10-12, 2021:
33th Benelux Conference on Artificial Intelligence and the 30th Belgian Dutch Conference on Machine Learning, Esch/Alzette, Luxembourg.
December 9, 2021: 11th TPTP Tea Party (TPTPTP), online. (participant)
July 23-29, 2022: 31th International Joint Conference on Artificial Intelligence and the 23rd European Conference on Artificial Intelligence (IJCAI-ECAI 2022), Vienna, Austria. (PC member)
July 31 - August 12, 2022: Federated Logic Conference (FLoC 2021), including IJCAR, LICS, ... etc, in Haifa, Isreal.
August 11-12, 2022: Workshop on Practical Aspects of Automated Reasoning (PAAR-2022), co-located at FLoC 2022, Haifa, Isreal. (PC co-chair)
September 19 - 23: 45th German Conference on Artificial Intelligence (KI 2022), Trier, Germany.
This is the personal homepage of Alexander Steen. I am a post-doctoral researcher at the Faculty of Science, Technology and Medicine (FSTM) of the University of Luxembourg. I'm working on the automated theorem prover Leo-III, a reasoning system for classical higher-order logic (HOL) and further expressive, non-classical logics (including higher-order modal logics and deontic logics). My ORCID ID is 0000-0001-8781-9462.
My current research interests include theory and practice of higher-order reasoning, including efficient data structures for higher-order theorem provers, and related implementation techniques. Furthermore, I'm interested in practical aspects and applications of logics and formal methods in computer science, mathematics and philosophy. Also, I like functional programming (e.g. in Haskell). A research profile (self-portrayal) about my recent work was published by the it - Information Technology journal: See doi:10.1515/itit-2019-0001.
In my freetime, I'm a bass singer in a choir for classical music of various periods and singer in a Schola Cantorum (Vokalschola), see "Links" section.
AuReLeE is funded by Luxembourg National Research Fund (FNR) under grant CORE C20/IS/14616644, PI: A. Steen
The goal of the project Automated Reasoning with Legal Entities (AuReLeE) is to provide effective and general means for the automation of normative reasoning processes based on legal knowledge bases. To this end, the project will design and implement a dedicated system that combines efficient decision procedures with a flexible approach to import and re-use existing knowledge bases for their employment as underlying contexts for the normative reasoning tasks. The results of AuReLeE hence allow to full utilization of the existing legal knowledge bases’ potential for compliance checking.
AuReLeE is conducted at the Faculty of Science, Technology and Medicine of the University of Luxembourg. It is hosted by the Individual and Collective Reasoning (ICR) research group at the Depart of Computer Science.Further information
Leo-III was funded by DFG under grant BE 2501/11-1 (Leo-III), PI: C. Benzmüller
Leo-III is an effective ATP system for HOL with Henkin semantics and choice. It is implemented in Scala; its source code, and that of related projects, is publicly available under BSD-3 license on GitHub. The system accepts all common TPTP input syntax formats, including untyped clause normal form (CNF), untyped and typed first-order logic (FOF and TFF, respectively) and, as primary input format, monomorphic higher-order logic (THF). Additionally, as one of the first higher-order ATP systems, Leo-III upports reasoning in rank-1 polymorphic variants of the above logics (TF1 and TH1 syntax). The prover returns results according to the standardized TPTP SZS ontology and produces a verifiable TPTP-compatible proof certificate, if a proof is found.
Leo-III was identified as one of the most effective (in terms of number of solved problems) and most versatile (in terms of supported logical formalisms) theorem prover to date by the GRUNGE evaluation, see arXiv:1903.02539.
Conducted at Dahlem Center of Machine Learning and Robotics of Freie Universität Berlin, joint work with T. Gleißner
MET is a tool for embedding modal logic logic problems into classical higher-order logic represented in TPTP THF format. The input language allows the user to specify the semantics of the desired quantified modal logic and automatically computes the correspondig embedding.Further information
Conducted at the Individual and Collective Reasoning group of University of Luxembourg, joint work with T. Libal
NAI (for Normative AI) is a framework for normative reasoning. NAI features an annotation-based editor which abstracts over the underlining logical language. It also contains an easily accessible functionality for quality assurance and a transparent analysis of the created formalized document. NAI also supports an approach for assessing the correctness of formalizations via execution of behavioral tests using so-called queries. Lastly, it provides an interface for the creation of such queries and for checking their validity. The architecture of NAI is modular, which allows using different logics and reasoning engines. It also provides an web-based interface, which can be used by other tools in order to reason over the formalized legislation.
NAI is open-source, its source code is freely available at GitHub 3 under GPL-3.0 license. It was awarded with the LexisNexis Best Paper Award of Internationales Rechtsinformatik Symposium (IRIS 2020), in Salzburg, Austria, 2020.Further information
I completed the advanced training certificate for unversity teaching (Hochschuldidaktisches Lehrzertifikat) of Freie Universität Berlin (Support für die Lehre).
Only showing the latest six teaching activities. » show complete list
Interested in writing a bachelors or masters thesis in the context of automated theorem proving or related areas? Feel free to contact me via e-mail.