February 2020: The paper NAI: Towards Transparent and Usable Semi-Automated
Legal Analysis of Tomer and me, presented at the
23rd Internationales Rechtsinformatik Symposion (IRIS 2020), was awarded the
LexisNexis Best Paper Award. Thanks a lot to the jury for chosing our contribution!
See also this press release.
January 2020: A summary paper ("highlight paper") about the Leo-III prover was accepted for presentation at ECAI 2020 in Santiago de Compostela, Spain.
September 2019: I was invited to join the "AI and Science" track at the KI-Camp (December 2019) and as an invited speaker at PhDs in Logic XII (April 2020), both in Berlin.
August 2019: Leo-III won the LTB division of this year's CASC! Also, Leo-III ranked second place in the CASC's THF division. See also the news article (Luxemburger Wort) and the UL press release.
July 2019: Our new album, Adoramus Te, is now available at Spotify, Amazon, and iTunes. See also some of our tracks at YouTube.
March 2019: An independent, large evaluation study identifies Leo-III as the worlds leading higher-order automated theorem prover: See arXiv:1903.02539.
January 2019: A research profile (self-portrayal) about my recent work was published by the it - Information Technology journal: See doi:10.1515/itit-2019-0001.
April 6-9, 2020 (postponed):
Zhejiang Conferences on Logics in Artificial Intelligence (ZJULogAI 2020), Hangzhou, China. (Co-organizer)
April 27-29, 2020 (postponed):
PhDs in Logic XII, Berlin, Germany. (Invited Speaker)
June 29 - July 2, 2020: 10th International Joint Conference on Automated Reasoning (IJCAR 2020), Paris, France.
June 29, 2020: 7th Workshop on Practical Aspects of Automated Reasoning (PAAR 2020), Paris, France. (PC member)
July 11 - 17, 2020 (postponed):
29th International Joint Conference on Artificial Intelligence (IJCAI 2020), Yokohama, Japan. (PC member)
July 26 - 31, 2020: 13th Conference on Intelligent Computer Mathematics (CICM 2020), Bertinoro, Forli, Italy.
July 30 - August 2, 2020 (postponed):
15th International Conference on Deontic Logic and Normative Systems (DEON 2020), Munich, Germany.
August 29 - September 2, 2020: 24th European Conference on Artificial Intelligence (ECAI 2020), Santiago de Compostela, Spain. (participant)
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).
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.
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 GRUNDE evaluation. Also. Leo-III won the LTB division of the CASC-27 in 2019.Further information
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? Feel free to contact me via e-mail.