September 2024: I'm on parental leave until March 2025!
August 2024: The AI section (FBKI) of the German Informatics Society (Gesellschaft für Informatik) has published a new statement paper on generativ AI and the AI act. See the press release (German).
July 2024: The CEUR-WS.org proceedings of the PAAR 2024 workshop are available online.
May 2024: I'm proud to present the publication announcement of the science comic book Was wissen wir schon (what do we know), published by the Jaja-Verlag, in September 2024! The book contains 21 science comics of the Fellows of the Academy of Science and Humanities in Hamburg (Akademie der Wissenschaften in Hamburg), including a science comic panel about my search on automated reasoning, with an additional foreword by Susanne Schwertfeger. See here for details.
April 2024: I will be joining the online plenary discussion on consequences of the AI act (Die Konsequenzen des EU-AI-Act – Blicke aus der Informatik), on May 15. Feel free to join! See GI WebTalk series on the EU vote 2024
March 2024: I'm pleased to host the fellow lecture of Daniel Misselbeck-Wessel at the Alfried Krupp Institute for Advanced Study in Greifswald. Feel free to join!
January 2024: The next Workshop on Practical Aspects of Automated Reasoning (PAAR-2024) will take place on July 2, 2024, at IJCAR 2024 in Nancy, France.
PAAR-2024 is co-chaired by
Cláudia Nalon (University of Brasilia, BR),
Martin Suda (Czech Technical University in Prague, CZ)
and myself.
December 2023: I was elected, together with Ralf Möller (U Lübeck), as new co-head (Speaker) of the Section for Artificial Intelligence (Fachbereich Künstliche Intelligenz, FBKI) of the German Informatics Society (Gesellschaft für Informatik, GI). The term starts in January 2024. See press release (in German).
November 2023: I was invited as panelist and speaker at the panel of the Alfried Krupp Institute for Advanced Study
on Artificial Intelligence and fairness (Künstliche Intelligenz: unsicher – unfair – ungerecht?).
November 2023: The Science Comic Posters project (a collection of 21 posters from many different scientific fields) will be presented as an exhibition
at the Alfried Krupp Institute for Advanced Study in Greifswald, Germany. The project is supported by the
Academy of Sciences and Humanities in Hamburg (Akademie der Wissenschaften in Hamburg).
October 2023: My essay on Truth and Logic (Wahrheit und Logik) has been
published by the Academy of Sciences and Humanities in Hamburg as part of the essay series on
truth (in german).
October 2023: A science comic about my research for the general public is presented along with many others at the Hamburg Comic Festival. This science communication initiative is funded by the Academy of Sciences and Humanities in Hamburg. A short press release in available (in German).
September 2023: The conference proceedings of KI 2023 has been published. It is available as part of Springer's LNCS series (volume 14236) at Springer Link.
September 2023: Our paper Solving Modal Logic Problems by Translation to Higher-Order Logic (A. Steen, G. Sutcliffe, T. Scholl, C. Benzmüller), presented at the 5th International Conference on Logic and Argumentation (CLAR 2023), won the Best Paper Award of the conference!
September 2023: My essay on fairness/equity in AI (Gerechte Künstliche Intelligenz) has been published, together with eleven further essays, as part of the
book
Mojib Latif (Hrsg.), Gerechtigkeit im 21. Jahrhundert (Mojib Latif (Ed.), Equity in the 21st century), Herder Verlag in collaboration with the Hamburg Academy of Sciences and Humanities.
This is the personal homepage of Alexander Steen. I am a Juniorprofessor (this is roughly equivalent to an assistant professor position) at the Institute of Mathematics and Computer Science of the University of Greifswald. I'm working on computational logic, automated reasoning and theoretical computer science. I'm the lead developer of 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) as well as further smaller software artifacts. 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, proposer and PI (until end of 2022): 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.
Leo-III won the LTB division of CASC-27! Also, Leo-III ranked second place in the CASC-27's THF division. See also the news article (Luxemburger Wort) and the UL press release.
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 informationI completed an advanced training certificate for unversity teaching (Hochschuldidaktisches Lehrzertifikat) of Freie Universität Berlin (Support für die Lehre) and a teaching certificate at the University of Greifswald following the standards of the Deutsche Gesellschaft für Hochschuldidaktik.
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.