News / Events

Recent news

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.
June 2022: To celebrate World Logic Day 2023, we are hosting a commemorative lecture on the life and work of Gerhard Gentzen on June 20, 2023. The guest speaker will be Prof. Reinhard Kahle (Tübingen).
April 2023: Forthcoming special issue of the journal KI – Künstliche Intelligenz on Non-Classical Reasoning for Contemporary AI Applications, feel free to submit!

Recommended upcoming events (partially with personal involvement)

July 1-6, 2024: International Joint Conference on Automated Reasoning (IJCAR 2024) in Nancy, France. (PC member)
July 1, 2024: TPTP Tea Party (Workshop), co-located with IJCAR 2024 in Nancy, France. (Co-organizer)
July 2, 2024: Workshop on Practical Aspects of Automated Reasoning (PAAR 2024), co-located with IJCAR 2024 in Nancy, France. (PC co-chair)
July 2, 2024: Workshop on Automated Theorem Proving in Quantified Non-Classical Logics (ARQNL), co-located with IJCAR 2024 in Nancy, France.
October 19/20, 2024: International Workshop on AI Value Engineering and AI Compliance Meechanisms (VECOMP 2024), co-located with ECAI 2024 in Santiago de Compostela, Spain. (PC member AICOM track)

About

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

Education

2018
Doctorate (Dr. rer. nat., summa cum laude) in Computer Science, Freie Universität Berlin, Germany
Dissertation: Extensional Paramodulation for Higher-Order Logic and its Effective Implementation Leo-III
Supervisor: Christoph Benzmüller (Freie Universität Berlin), Second examiner: Geoff Sutcliffe (University of Miami)
2014
Master of Science in Computer Science, Freie Universität Berlin, Germany
2014
Bachelor of Science in Mathematics, Freie Universität Berlin, Germany
2013
Bachelor of Science in Computer Science, Freie Universität Berlin, Germany
2009
Abitur (A-Levels), Lichtenberg-Gymnasium, Cuxhaven, Germany

Professional Affiliations

2022 -
Assistant professor (Juniorprofessor) for Computer Science, University of Greifswald, Germany.
2018 - 2021
Post-doctoral research associate at the Faculty of Science, Technology and Medicine (FSTM) of the University of Luxembourg
Member of the Individual and Collective Reasoning (ICR) group and the Interdisciplinary Lab for Intelligent and Adaptive Systems (ILIAS)
2018
Independent scientific consulting, project "Towards a Verifiable Smart Contract Language", BILLON SP. Z O.O., Warsaw/London.
2014 - 2018
Research assistant (wiss. Mitarbeiter) at the Dahlem Center for Machine Learning and Robotics at the Institute of Computer Science, Freie Universität Berlin.
2014
Student research assistant (stud. Hilfskraft) at the project Leo-III, Freie Universität Berlin
2011
Freelance programmer (Java, JavaScript, GWT) at Farfromhomepage
2010 - 2014
Tutor (stud. Hilfskraft) at Freie Universität Berlin, Germany

Prizes, Honors etc.

2024
Nomination for the Teaching Award of the University of Greifswald
2023
Best Paper Award of CLAR 2023
2022
Fellow of the Academy of Sciences and Humanities in Hamburg
Top 10 Papers of the IRIS 2022 conference
2021
Participation in Dagstuhl seminar 21371: Integrated Deduction (September 12-17)
2020
LexisNexis Best Paper Award of the Int. Legal Informatics Symposium (IRIS 2020)
2019
1st place at CASC-27 (LTB division) with Leo-III
Runner-up at CASC-27 (THF division) with Leo-III
Finalist for the Ernst-Reuter-Prize of Freie Universität Berlin
Nominated as AI Newcomer (BMBF, GI)
2018
Junior-Fellowship of the German Gesellschaft für Informatik (GI)
DFG mentor for 30th European Union Contest for Young Scientists (EUCYS) in Dublin
Woody Bledsoe Travel Award of the CADE
2017
Participation in Dagstuhl seminar 14741: Deduction Beyond First-Order Logic (September 10-15)
2nd place at CASC-26 (THF division) with Leo-III
2016
Woody Bledsoe Travel Award of the CADE
Zentraler Lehrpreis 2015/2016 (Teaching award) of the Freie Universität Berlin for the concept of a lecture on Computational Metaphysics (Press release: german, english)
2015
GI FB-KI Travel Grant (Gesellschaft für Informatik, Fachbereich Künstliche Intelligenz)
2012 - 2014
Scholarship of the German Academic Foundation (Studienstiftung des deutschen Volkes)

Projects / Software development

AuReLeE – Automated Reasoning with Legal Entities

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 – Effective Automation for Higher-Order Logic

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
  • Leo-III @ GitHub: Code of and instructions for Leo-III are available at github.com/leoprover/Leo-III.
  • Leo-III example input and outputs: Case studies for the application of Leo-III to higher-order logic problems, modal logic reasoning, choice reasoning and polymorphic HOL reasoning are available as supplemental material to my PhD thesis.
  • Dissertation abstract about Leo-III: A 4-page overview of the Leo-III project and its theoretical and practical details is freely avaiable at Springer Link.

 

MET – Modal Embedding Tool for Reasoning in Quantified Modal Logics

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
  • MET @ GitHub: Code of and instructions for MET are available at github.com/leoprover/embed_modal.
  • Ongoing standardization project as TPTP standard: The input format is currently considered as a logic specification format standard at the TPTP infrastructure, see the proposal document.

 

NAI – Normative Reasoning/Legal Analysis

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
  • NAI @ GitHub: Code of and instructions for the frontend and backend of NAI are available at github.com/normativeai.
  • NAI web tool: An instance of NAI is hosted at nai.uni.lu, free for own experimentation and tests.
  • Tutorial material: Tutorial material that was used in lectures on normative reasoning at the ICAIL 2019 conference in Montreal, Canada, is available at tutorial.normativeai.com.
  • Youtube video tutorial for NAI: A visual guide by Tomer Libal for the usage of NAI can be found at Youtube. It was presented by Tomer at ReMeP 2019.

Professional Activities

Organizations

Program Committees/Conference Organization

2024
2023
2022
2021
2020
2019
2018
2015
CADE-25 (local co-organizer)

Administrative Academic Services

2024 -
2023 -
Member of the working group on AI in unversity teaching (AG KI in der Lehre) at the University of Greifswald
2022 -
Appointed examiner for state examinations in Mathematics (Prüfer für das erste Staatsexamen Mathematik Lehramt) at University of Greifswald
2021 -
Management committee (MC) of COST action European Research Network on Formal Proofs (CA20111), vice leader of WG2 on automated theorem proving. Since November 2022: Leader of WG2
2019 -
Mentoring programme of the German Informatics Society (GI)
2019 - 2024
Spokesperson of the SIG on deduction systems (Fachgruppe Deduktionssysteme) (re-elected January 2022)
2020 - 2021
Editor of the ZLAIRE newsletter
2017 - 2018
2016 - 2018
Member of the faculty council (Fachbereichsrat)
2015 - 2016
2015 - 2017
Head of the tutor selection committee for Computer Science studies (Tutorenauswahlkommission Informatik)
2015 - 2016
Deputy Member of the faculty council (Fachbereichsrat)
2013 - 2015
Student member of the tutor selection committee for Computer Science (Tutorenauswahlkommission Informatik), Department of Mathematics and Computer Science, Freie Universität Berlin
2013 - 2014
Head of the teaching committee (Ausbildungskommission), Department of Mathematics and Computer Science, Freie Universität Berlin
2013 - 2014
Student member of the institute administrative council (Institutsleitung), Institute for Computer Science, Freie Universität Berlin
2012 - 2013
Mentoring for new enrollees, Institute of Computer Science, Freie Universität Berlin
2012
Student representative for the computer science graduate program at the inFU-visit days for high-school students

Publications

[google scholar] [dblp] [orbi.lu]

Books

  1. Alexander Steen, Extensional Paramodulation for Higher-Order Logic and its Effective Implementation Leo-III. Part of series Dissertations in Artificial Intelligence (DISKI), volume 345, EAN/ISBN 978-3-89838-739-2, AKA-Verlag, 2018. Book version of dissertation, Freie Universität Berlin.

Edited volumes

  1. Chris Brown, Daniela Kaufmann, Cláudia Nalon, Alexander Steen, Martin Suda (Eds.), Joint Proceedings of the 9th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 9th Satisfiability Checking and Symbolic Computation Workshop (SC-Square). CEUR Workshop Proceedings, Vol. 3717, CEUR-WS.org, urn:nbn:de:0074-3717-7, 2024.
  2. Dietmar Seipel, Alexander Steen (Eds.), KI 2023: Advances in Artificial Intelligence. 46th German Conference on AI, Berlin, Germany, September 26–29, 2023, Proceedings. LNCS, Vol. 14236, Springer, 2023.
  3. Boris Konev, Claudia Schon, Alexander Steen (Eds.), Proceedings of the Workshop on Practical Aspects of Automated Reasoning (PAAR 2022). CEUR Workshop Proceedings, Vol. 3201, CEUR-WS.org, urn:nbn:de:0074-3201-6, 2022.
  4. Dörthe Arndt, Ahmet Soylu, Jan Vanthienen, Evgeny Kharlamov, Alexander Steen (Eds.), Proceedings of the 16th International Rule Challenge and 6th Doctoral Consortium @ RuleML+RR 2022 (RuleML+RR DC 2022). CEUR Workshop Proceedings, Vol. 3229, CEUR-WS.org, urn:nbn:de:0074-3229-5, 2022.
  5. Ahmet Soylu, Sotiris Moschoyiannis, Guido Governatori, Mantas Simkus, Petros Stefaneas Alexander Steen, Adrian Giurca (Eds.), Proceedings of the 13th RuleML+RR 2019 Doctoral Consortium and Rule Challenge. CEUR Workshop Proceedings, Vol. 2438, CEUR-WS.org, urn:nbn:de:0074-2438-5, 2019.
  6. Christoph Benzmüller, Xavier Parent and Alexander Steen (Eds.), Selected Student Contributions and Workshop Papers of LuxLogAI 2018. Kalpa Publications in Computing, volume 10, ISSN 2515-1762, EasyChair, 2019.
  7. Daniel Lee and Alexander Steen and Toby Walsh (Eds.), GCAI-2018. 4th Global Conference on Artificial Intelligence. EPiC Series in Computing, volume 55, ISSN 2398-7340, EasyChair, 2018.

Journal articles

  1. Alexander Steen, Geoff Sutcliffe, Christoph Benzmüller, Solving Quantified Modal Logic Problems by Translation to Classical Logics. Journal of Logic and Computation, 2024. (submitted)
  2. Alexander Steen, Ableitungen als wesentliche Fähigkeit von KI-Systemen nach KI-VO. (to appear)
  3. Alexander Steen, Christoph Benzmüller, Non-Classical Reasoning for Contemporary AI Applications. KI – Künstliche Intelligenz, 2024.
  4. Alexander Steen, Christoph Benzmüller, Challenges for Non-Classical Reasoning in Contemporary AI Applications. KI – Künstliche Intelligenz, 2024.
  5. Axel Adrian, Michael Keuchen, Max Rapp, Alexander Steen, Auslegung des KI-VO-E zur Evaluation von Symbolischen Deduktionsverfahren der Künstlichen Intelligenz für Juristische Anwendungen. Jusletter IT, 15. Februar 2024.
  6. Alexander Steen, Christoph Benzmüller, On Reductions of Hintikka Sets for Higher-Order Logic. Journal of Applied Logics, 2024. (accepted for publication)
  7. Antoine Martina, Alexander Steen, An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic. Journal of Logic and Computation, 2024.
  8. Alexander Steen, Christoph Benzmüller, What are Non-Classical Logics and why do we need them? An extended interview with Dov Gabbay and Leon van der Torre. KI – Künstliche Intelligenz, 2024.
  9. Axel Adrian, Max Rapp, Alexander Steen, Juristische Methodenlehre 3.0: Auf dem Weg zu einer maschinengestützten Methodenwissenschaft. Jusletter IT, 23. Februar 2023.
  10. Christoph Benzmüller, David Fuenmayor, Alexander Steen, Geoff Sutcliffe, Who Finds the Short Proof? An Exploration of Variants of Boolos' Curious Inference using Higher-order Automated Theorem Provers. Logic Journal of the IGPL, 2023.
  11. Alexander Steen, David Fuenmayor, A Formalisation of Abstract Argumentation in Higher-Order Logic. Journal of Logic and Computation, 2023.
  12. Axel Adrian, Max Rapp and Alexander Steen, Von Objekt- und Meta-Ebenen: Analyse der Softwareanforderungen Computergestützter Juristischer Entscheidungen Jusletter IT 30. Juni 2022
  13. Alexander Steen, Christoph Benzmüller, Extensional Higher-Order Paramodulation in Leo-III. Journal of Automated Reasoning 65, pp. 775-807, 2021.
  14. Christoph Benzmüller, Ali Farjami, David Fuenmayor, Paul Meder, Xavier Parent, Alexander Steen, Leendert van der Torre, Valeria Zahoransky, LogiKEy Workbench: Deontic Logics, Logic Combinations and Expressive Ethical and Legal Reasoning (Isabelle/HOL Dataset). In Data in Brief, Volume 33, December 2020, 106409, Elsevier, 2020.
  15. Alexander Steen, Extensional Paramodulation for Higher-Order Logic and its Effective Implementation Leo-III (Dissertation Abstract). In Künstliche Intelligenz, Volume 34, pp. 105 - 108, 2020.
  16. Tomer Libal, Alexander Steen, NAI: Towards Transparent and Usable Semi-Automated Legal Analysis. In Verantwortungsbewusste Digitalisierung, Proceedings of 23rd Internationales Rechtsinformatik Symposion (IRIS 2020), E. Schweighofer, W. Hötzendorfer, F. Kummer, A. Saarenpää (Eds.), pp. 265-272, ISBN 978-3-96698-589-5, Editions Weblaw, 2020; and Jusletter IT, Volume of 27. Mai 2020, 2020.
  17. Alexander Steen, Higher-Order Theorem Proving and its Applications (GI Junior-Fellow self-portrayal). it - Information Technology, Volume 61, Issue 4, Pages 187–191, ISSN (Online) 2196-7032, ISSN (Print) 1611-2776, 2019.
  18. Alexander Steen, Christoph Benzmüller The Higher-Order Prover Leo-III (extended abstract). In Künstliche Intelligenz 2019, Proceedings, LNCS, Vol. 11793, Springer, 2019.
  19. Alexander Steen, Christoph Benzmüller, Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic. In Logic and Logical Philosophy, Volume 25, No 4, Nicolaus Copernicus University, 2016.

Papers in conference proceedings (peer-reviewed)

  1. Melanie Taprogge, Alexander Steen, Flexible Automation of Quantified Multi-Modal Logics with Interaction. In KI 2023: Advances in Artificial Intelligence. 46th German Conference on AI, Berlin, Germany, September 26–29, 2023, Proceedings, LNCS, Vol. 14236, Springer, 2023.
  2. Alexander Steen, Geoff Sutcliffe, Tobias Gleißner and Christoph Benzmüller, Solving QMLTP Problems by Translation to Higher-order Logic. In Proceedings of the 5th International Conference on Logic and Argumentation (CLAR 2023), LNCS, Vol. 14156, Springer, 2023.
  3. Alexander Steen, Geoff Sutcliffe, Pascal Fontaine and Jack McKeown, Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic. In 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-24), Proceedings, Ruzica Piskac, Andrei Voronkov (Eds.), EPiC Series in Computing, Vol. 94, pp. 369-385, EasyChair, 2023.
  4. Axel Adrian, Max Rapp, Alexander Steen, Juristische Methodenlehre 3.0: Auf dem weg zu einer maschinengestützten Methodenwissenschaft. In Erich Schweighofer, Jakob Zanol, Stefan Eder (Eds.), Rechtsinformatik als Methodenwissenschaft des Rechts. Tagungsband des 26. Internationalen Rechtsinformatik Symposions IRIS 2023, Editions Weblaw 2023, ISBN 978-3-98595-714-9, pp. 81-90, Weblaw, 2023.
  5. Alexander Steen, David Fuenmayor, Bridging between LegalRuleML and TPTP for Automated Normative Reasoning. In 6th International Joint Conference on Rules and Reasoning (RuleML+RR 2022), Proceedings, Anni-Yasmin Turhan, Guido Governatori (Eds.), LNCS, Vol. 13752, pp. 244--260, Springer, 2022.
  6. Axel Adrian, Max Rapp, Alexander Steen, Von Objekt- und Meta-Ebenen: Analyse der Softwareanforderungen computergestützter juristischer Entscheidung. In In Recht DIGITAL -- 25 Jahre IRIS, Tagungsband des 25. Internationalen Rechtsinformatik Symposiums IRIS 2022, Proceedings of 25th Internationales Rechtsinformatik Symposion (IRIS 2022), Erich Schweighofer, Ahti Saarenpää, Stefan Eder, Jakob Zanol, Felix Schmautzer, Franz Kummer, Philip Hanke (Eds.), pp. 307ff, Editions Weblaw, Bern, 2022.
  7. Alexander Steen, Goal-Directed Decision Procedures for Input/Output Logics. In 15th International Conference on Deontic Logic and Normative Systems (DEON 2020/2021, Munich), Fenrong Liu, Alessandra Marra, Paul Portner, and Frederik Van De Putte (Eds.), College Publications, London, 2021.
  8. Alexander Steen, Christoph Benzmüller, The Higher-Order Prover Leo-III. In 24th European Conference on Artificial Intelligence (ECAI 2020), Proceedings, De Giacomo, G., Catala, A., Dilkina, B., Milano, M., Barro, S., Bugarín, A., Lang, J. (Eds.), Frontiers in Artificial Intelligence and Applications, Vol. 325, pp. 2937 - 2938, IOS Press, 2020.
  9. Tomer Libal, Alexander Steen, Towards an Executable Methodology for the Formalization of Legal Texts. In 3rd International Conference on Logic and Argumentation (CLAR 2020), Proceedings, Lecture Notes in Computer Science (LNCS), Volume 12061, pp. 151-165, Springer, 2020.
  10. Tomer Libal, Alexander Steen, NAI: The Normative Reasoner. In 17. International Conference on Artificial Intelligence and Law (ICAIL 2019), pp. 262-263, ACM, 2019.
  11. Tomer Libal, Alexander Steen, The NAI Suite - Drafting and Reasoning over Legal Texts. In 32nd International Conference on Legal Knowledge and Information Systems (JURIX 2019), Frontiers in Artificial Intelligence and Applications, Volume 322, pp. 243--246, IOS Press, 2019.
  12. Tobias Gleißner, Alexander Steen, The MET: The Art of Flexible Reasoning with Modalities. In Christoph Benzmüller, Francesco Ricca (Eds.), 2nd International Joint Conference on Rules and Reasoning (RuleML+RR 2018), Proceedings, Springer, LNCS, 2018.
  13. Alexander Steen, Christoph Benzmüller, The Higher-Order Prover Leo-III. In Didier Galmiche, Stephan Schulz, Roberto Sebastiani (Eds.), Automated Reasoning --- 9th International Joint Conference, IJCAR 2018, Oxford, UK, July 14-17, 2018, Proceedings , Springer, LNCS, Volume 10900, pp. 108-116, 2018.
  14. Tobias Gleißner, Alexander Steen, Christoph Benzmüller, Theorem Provers for Every Normal Modal Logic, In Thomas Eiter, David Sands (Eds.), LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EasyChair, EPiC Series in Computing, Volume 46, pp. 14-30, 2017.
  15. Alexander Steen, Max Wisniewski, Christoph Benzmüller, Tutorial on Reasoning in Expressive Non-Classical Logics with Isabelle/HOL. In Christoph Benzüller, Raul Rojas, Geoff Sutcliffe (Eds.), Second Global Conference on Artificial Intelligence (GCAI), Proceedings, EasyChair, EPiC Series in Computing, Volume 41, pp. 1-10, 2016.
  16. Alexander Steen, Max Wisniewski, Christoph Benzmüller, Einsatz von Theorembeweisern in der Lehre. In Andreas Schwill, Ulrike Lucke (Eds.), Hochschuldidaktik der Informatik, HDI2016 – 7. Fachtagung des GI-Fachbereichs Informatik und Ausbildung / Didaktik der Informatik ; 13.-14. September 2016 an der Universität Potsdam, Commentarii Informaticae Didacticae, Volume 10, pages 81 - 92, Universitätsverlag Potsdam, 2016.
  17. Alexander Steen, Max Wisniewski, Christoph Benzmüller, Agent-Based HOL Reasoning. In 5th International Congress on Mathematical Software, ICMS 2016, Berlin, Germany, July 2016, Proceedings, Springer, LNCS, volume 9725, 2016.
  18. Max Wisniewski, Alexander Steen, Kim Kern, Christoph Benzmüller, Effective Normalization Techniques for HOL. In Nicola Olivetti, Ashish Tiwari (Eds.), 8th International Joint Conference on Automated Reasoning, IJCAR 2016, Coimbra, Portugal, 27 June - 2 July, 2016, Proceedings. Springer, LNAI, volume 9706, 2016.
  19. Alexander Steen, Christoph Benzmüller, There Is No Best Beta-Normalization Strategy for Higher-Order Reasoners. In Martin Davis, Ansgar Fehnker, Annabelle CcIver, Andrei Voronkov (Eds.), 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Suva, Fiji, November 2015, Proceedings, Springer, LNCS/ARCoSS, volume 9450, 2015.
  20. Alexander Steen, Christoph Benzmüller, Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic (Extended Abstract). Non-Classical Logic. Theory and Applications, Torun, Poland, September 24-26, 2015.
  21. Max Wisniewski, Alexader Steen, Christoph Benzmüller, LeoPARD - A Generic Platform for the Implementation of Higher-Order Reasoners (Project Paper). In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, Volker Sorge (Eds.), Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings , Springer, LNCS, volume 9150, pp. 325--330, 2015.

Workshop papers (peer-reviewed)

  1. Alexander Steen, Geoff Sutcliffe, TPTP World Infrastructure for Non-classical Logics. Ninth Workshop on Practical Aspects of Automated Reasoning (PAAR 2024). accepted for publication
  2. Geoff Sutcliffe, Jack McKeown, Alexander Steen, A Chat with Bard. 14th International Workshop on the Implementation of Logics (IWIL 2023), EasyChair Preprint no. 10329, 2023.
  3. Alexander Steen, David Fuenmayor, Tobias Gleißner, Geoff Sutcliffe and Christoph Benzmüller, Automated Reasoning in Non-classical Logics in the TPTP World. In Boris Konev, Claudia Schon, Alexander Steen (Eds.), 8th Workshop on Practical Aspects of Automated Reasoning (PAAR 2022), CEUR Workshop Proceedings, Vol. 3201, CEUR-WG.org, 2022.
  4. Alexander Steen, An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning. In Boris Konev, Claudia Schon, Alexander Steen (Eds.), 8th Workshop on Practical Aspects of Automated Reasoning (PAAR 2022), CEUR Workshop Proceedings, Vol. 3201, CEUR-WG.org, 2022.
  5. David Fuenmayor, Alexander Steen, A Flexible Approach to Argumentation Framework Analysis using Theorem Proving . In Logics for New-Generation AI 2021, Beishui Liao, Jieting Luo and Leendert van der Torre (Eds.), College Publications, London, 2021. ISBN 978-1-84890-373-9.
  6. Alexander Steen, Christoph Benzmüller, System Demonstration: The Higher-Order Prover Leo-III. In Christoph Benzmüller, Jens Otten (Eds.), ARQNL 2018. Automated Reasoning in Quantified Non-Classical Logics, Proceedings, CEUR Workshop Proceedings, http://ceur-ws.org, volume 2095, 2018.
  7. Alexander Steen, Max Wisniewski, Christoph Benzmüller Going Polymorphic - TH1 Reasoning for Leo-III, In Thomas Eiter, David Sands, Geoff Sutcliffe and Andrei Voronkov (Eds.), IWIL Workshop and LPAR Short Presentations, EasyChair, Kalpa Publications in Computing, Volume 1, pp. 100-112, 2017.
  8. Alexander Steen, Max Wisniewski, Hans-Jörg Schurr, Christoph Benzmüller Capability Discovery for Automated Reasoning Systems, In Thomas Eiter, David Sands, Geoff Sutcliffe and Andrei Voronkov (Eds.), IWIL Workshop and LPAR Short Presentations, EasyChair, Kalpa Publications in Computing, Volume 1, pp. 113-118, 2017.
  9. Christoph Benzmüller, Alexander Steen, Max Wisniewski Leo-III Version 1.1 (System description), In Thomas Eiter, David Sands, Geoff Sutcliffe and Andrei Voronkov (Eds.), IWIL Workshop and LPAR Short Presentations, EasyChair, Kalpa Publications in Computing, Volume 1, pp. 11-26, 2017.
  10. David Fuenmayor, Christoph Benzmüller, Alexander Steen, Max Wisniewski, Computer-assisted Assessment of Lowe's Modal Ontological Argument, In Stanislaw Krajewski, Piotr Balcerowicz (Eds.), Handbook of the 2nd World Congress on Logic and Religion, Warsaw, Poland, 2017.
  11. Tomer Libal, Alexander Steen, Towards a Substitution Tree Based Index for Higher-order Resolution Theorem Provers. In 5th Workshop on Practical Aspects of Automated Reasoning (PAAR 2016), Coimbra, Portugal, July 2016, Proceedings. CEUR Workshop Proceedings, Volume 1653, CEUR-WS.org, 2016.
  12. Max Wisniewski, Alexander Steen, Christoph Benzmüller, TPTP and Beyond: Representation of Quantified Non-Classical Logics. In C. Benzmüller, J. Otten (Eds.), 2nd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2016), Coimbra, Portugal, July 2016, Proceedings, CEUR Workshop Proceedings, Volume 1770, CEUR-WS.org, 2016.
  13. Alexander Steen, Max Wisniewski, Embedding of First-Order Nominal Logic into HOL. In Jean-Yves Beziau, Safak Ural, Arthur Buchsbaum, Iskender Tasdelen, Vedat Kamer (Eds.), 5th World Congress and School on Universal Logic (UNILOG'15), Handbook of abstracts, Istanbul, Turkey, pp. 337--339, 2015.
  14. Max Wisniewski, Alexander Steen, Christoph Benzmüller, The Leo-III Project. In Alexander Bolotov, Manfred Kerber (Eds.), Joint Automated Reasoning Workshop and Deduktionstreffen, Vienna, Austria, pp. 38, 2014.
  15. Max Wisniewski, Alexander Steen, Embedding of Quantified Higher-Order Nominal Modal Logic into Classical Higher-Order Logic. In Christoph Benzmüller, Jens Otten (Eds.), 1st International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2014), Vienna, Austria, Proceedings, EasyChair, EasyChair Proceedings in Computing, volume 33, pp. 59--64, 2014.

Other contributions

  1. Alexander Steen, Matteo Farinella, Automatisches Schlussfolgern (Automated Reasoning). Science Comic Poster, presented at the Hamburg Comic Festival, 2024.
  2. Alexander Steen, Wahrheit und Logik (Truth and Logic). In Essayreihe: Wahrheit (Essays on truth), Academy of Sciences and Humanities in Hamburg essay series, 2023.
  3. Alexander Steen, Gerechte Künstliche Intelligenz (Essay on equity/fairness in AI). In Majoib Latif (Ed.), Gerechtigkeit im 21. Jahrhundert (Equity in the 21st century), Academy of Sciences and Humanities in Hamburg book series, ISBN 978-3-451-39584-0, Herder Verlag, 2023.
  4. Zsofia Kräussl, Myriam Lapierre, Alexander Steen, Defining Governance for Public-Private Networks: A Computational Logic-based Approach. Research paper pre-print. Available at SSRN.
  5. Claudia Nalon, Alexander Steen, Guest Column: It is dark before dawn. Association for Automated Reasoning, Newsletter No. 136, November 2021.
  6. Claudia Schon, Alexander Steen (Eds.), Deduktionstreffen 2019, Proceedings. Informal workshop proceedings.
  7. Alexander Steen, Guest Column: Challenges in Higher-Order Theorem Proving. Association for Automated Reasoning, Newsletter No. 128, July 2019.
  8. Alexander Steen, Leo-III: A Theorem Prover for Classical and Non-Classical Logics, Automated Reasoning Workshop 2018, Cambridge, UK (mildly reviewed).
  9. Christoph Benzmüller, Alexander Steen, Max Wisniewski, News --- 25th International Conference on Automated Deduction (CADE-25), In Künstliche Intelligenz, volume 29, issue 4, pp. 451-452, 2015. (Non-reviewed conference report)
  10. Alexander Steen, Efficient Data Structures for Higher-Order Reasoners (Poster). Deduktionstreffen 2015, Berlin, Germany, 2015.
  11. Alexander Steen, Efficient Data Structures for Automated Theorem Proving in Expressive Higher-Order Logics. Master Thesis, Freie Universität Berlin, 2014.
  12. Alexander Steen, Generation and State-Space Reduction of Program Graphs for Non-deterministic Programs. Bachelor Thesis, Freie Universität Berlin, 2012.

Teaching

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

Current and past teaching activities

  1. Summer 24: Theoretische Informatik (theoretical computer science), lecture and tutorial, University of Greifswald
  2. Winter 23/24: Comicseminar Logik und Grundlagen der Mathematik (comic seminar on logic and foundations of mathematics), seminar, University of Greifswald.
  3. Winter 23/24: Einführung in mathematische Logik (introduction to mathematical logic), lecture, University of Greifswald.
  4. Summer 23: Projektseminar Logik und Künstliche Intelligenz (project seminar on logic and AI), seminar, University of Greifswald.
  5. Summer 23: Pro-/Seminar: Juristische Argumentation und „Künstliche Intelligenz“ (seminar on legal argumentation and AI), guest lecturer at University of Erlangen-Nuremberg, course by Prof. Dr. Axel Adrian
  6. Winter 22: Expressive Logiken (expressive logics), lecture and tutorial, University of Greifswald.
  7. Summer 22: International Seminar on Theorem Proving, seminar, University of Greifswald.
  8. Summer 22: Theorie und Praxis automatischer Theorembeweisersysteme (Theory and practice of automated thorem proving systems), Lecture and tutorial, University of Greifswald.
  9. Summer 22: Logik und Künstliche Intelligenz für Legal Tech (Logic and AI for Legal Tech), seminar, University of Greifswald.
  10. Summer 22: Gastdozent im Juristen-Proseminar zu Subsumtion und Logik in Rechtsanwendung und Legal-Tech (guest lecturer, legal students seminar on subsumption and logic in the application of law and legal tech), seminar by Prof. Dr. Axel Adrian, FAU University of Erlangen-Nuremberg.
  11. Winter 21: Proseminar/Seminar 'Künstliche Intelligenz' und juristische Argumentation (Seminar on Artificial Intelligence and legal argumentation), course by Prof. Dr. Axel Adrian, FAU University Erlangen-Nuremberg, guest lecturer (two lectures in November 2021).
  12. Winter 21: Data, Information and Technology (Lectures on Introduction to computational logic and knowledge representation), Master in Finance and Economics, University of Luxembourg.
  13. Summer 21: PhD graduate course on Logic, Argumentation and AI, Doctoral School in Science and Engineering (DSSE), University of Luxembourg
  14. Summer 21: Intelligent Agents 1 (introduction to agent-based knowledge representation and argumentation), University of Luxembourg, Lecturer
  15. March 21: Webinar on Knowledge Representation and Reasoning, lecturer, as part of the Elements of AI MOOC.
  16. Winter 20: Selected Topics in AI (Seminar): Knowledge Evolution - From belief revision and machine learning to theory dynamics, Co-Instructor together with Emil Weydert, University of Luxembourg
  17. Winter 20: Intelligent Systems: Agents and Reasoning, University of Luxembourg, Lecturer
  18. Winter 20: PhD graduate course on Logic in AI, Doctoral School in Science and Engineering (DSSE), University of Luxembourg
  19. Summer 20: ProInformatik III (introduction to imperative programming), Freie Universität Berlin (via Erasmus+), Lecturer, together with Victor Brekenfeld (cancelled)
  20. Summer 20: Intelligent Agents 1, University of Luxembourg, Lecturer, together with Leon van der Torre
  21. Summer 20: Bachelor Semester Project, University of Luxembourg
  22. Winter 19: Intelligent Systems: Agents and Reasoning, University of Luxembourg, Lecturer
  23. Winter 19: Automated Deduction with legal texts, Tutorial at ICAIL 2019, Montreal, Canada
  24. Summer 19: Bachelor Semester Project, University of Luxembourg
  25. Winter 18: Intelligent Agents II, University of Luxembourg, Co-lecturer
  26. Summer 17: WYSIWYG-Editor for Higher Order Logic, 10 ECTS, Co-instructor
  27. Winter 16/17: Seminar on Higher-Order Theorem Proving, 5 ECTS, Instructor
  28. Winter 16/17: Planung, Durchführung und Analyse eines Tutoriums (Conception and conduction of a tutorial), 5 ECTS, Instructor
  29. Summer 16: Künstliche Intelligenz (artificial intelligence), 5 ECTS, Tutorial sessions
  30. Summer 16: Computational Metaphysics, 5 ECTS, Instructor
  31. Summer 16: Planung, Durchführung und Analyse eines Tutoriums (Conception and conduction of a tutorial), 5 ECTS, Instructor
  32. Winter 15/16: Programmieren (Programming Basics), 5 ECTS, Stand-in Lecturer
  33. Summer 15: Proseminar Logik (Seminar on logic), 5 ECTS, Instructor
  34. Summer 15: ALP IV: Nichtsequentielle Programmierung (Concurrent programming), 5 ECTS, Lecturer (mit Lehrauftrag)
  35. Winter 14/15: Entwicklung eines netzbasierten Editors zur Generierung von PDF-Dokumenten (Software project), 10 ECTS, Instructor
  36. Winter 14/15: ALP V: Netzprogrammierung (Network programming), 5 ECTS, Tutorial session (mit Lehrauftrag)
  37. Winter 14/15: Expressive Logiken -- Theorie, Mechanisierung, Anwendungen (Theory, Automatization and Applications of Expressive Logics), 5 ECTS, Tutorial session
  38. Winter 13/14: ALP V: Netzprogrammierung (Network programming), Tutorial session
  39. Summer 13: Realworld Haskell (advanced functional programming), Lecturer & Tutorial session
  40. Summer 13: Hacken mit Haskell (introduction to functional programming for senior high school students), Lecturer
  41. Summer 13: ALP IV: Nichtsequentielle Programmierung (Concurrent programming), Tutorial session
  42. Winter 12/13: ALP V: Netzprogrammierung (Network programming), Tutorial session
  43. July/August 12: ProInformatik II - Funktionale Programmierung (Functional programming), Tutorial session (mit Lehrauftrag)
  44. Summer 12: ALP IV: Nichtsequentielle Programmierung (Concurrent programming), Tutorial session
  45. Winter 11/12: ALP I: Funktionale Programmierung (Functional programming), Tutorial session
  46. Summer 11: ALP IV: Nichtsequentielle Programmierung (Concurrent programming), Tutorial session
  47. Winter 10/11: ALP I: Funktionale Programmierung (Functional programming), Tutorial session

Only showing the latest six teaching activities. » show complete list

Supervision of students

Ongoing
  1. William K. (University of Greifswald): Reconstruction of higher-order automated proofs with external first-order cooperation (working title, Masters, supervisor).
  2. Milene J. (University of Greifswald): Modal logic problems for the TPTP (Bachelors, supervisor).
  3. Jule W. (University of Greifswald): Implementation of Arithmetic in Leo-III (Bachelors, supervisor).
  4. A.K. Schütz (University of Greifswald), PhD, member of commission.
Past/completed
  1. Melanie T. (University of Greifswald): Computer-Assisted Proof Verification for Higher-Order Automated Reasoning within the Dedukti Framework, 2024. (Masters, supervisor)
  2. Skipp G. (University of Greifswald): Interaktive Visualisierung von prädikatenlogischen Kripke-Strukturen, 2024. (Bachelors, supervisor)
  3. Bennet B. (University of Greifswald): Frühe Rezeptionsgeschichte des Intuitionismus im deutschsprachigen Raum, 2024. (State examination, second examiner)
  4. Jakob H. (University of Greifswald): Automation of Term-Modal-Logics, 2023. (Masters, supervisor)
  5. Lukasz R. (University of Greifswald): Visualization of Kripke-Models for modal logic reasoning, 2023. (Bachelors, supervisor)
  6. Colin R. (Freie Universität Berlin): Automated theorem proving for dependent typed theories via a translation to higher-order logic. (Masters, co-supervisor)
  7. Nina P. (Freie Universität Berlin): Vertrauenswürdige autonome Fahrzeuge — Ethische Kontrolle in Unfallsituationen gemäß ALTAI und vorgeschlagenem AIA. (Bachelors, co-supervisor)
  8. Petar Vukmirović (Free University of Amsterdam): implementation of higher-order superposition. (PhD, member of commission)
  9. Antoine M. (University of Luxembourg): An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic. (Masters, daily supervisor and advisor)
  10. Marc N. (Freie Universität Berlin): CI/CD für einen Automatischen Theorembeweiser. (Bachelors, co-supervisor)
  11. Federico G. (University of Bologna): Algorithmic business and the EU law on fair trading. (PhD, committee member (CET))
  12. Alessio N. (University of Luxembourg): Visualization of Kripke-Models, 2020. (Bachelor semester project, supervisor)
  13. Irina M. (Freie Universität Berlin): Free Higher-Order Logic - Notion, Definition and Embedding. (Masters, co-supervisor)
  14. Tobias G. (Freie Universität Berlin): A Framework for Higher-Order Modal Logic Theorem Proving, 2019. (Masters, supervisor)
  15. Gavin G. (American University of Paris): Summer internship on programming and legal tech, 2019.
  16. Adriano V. M. (University of Luxembourg): A Guide to Understand and Write Mathematical Proofs, 2019. (Bachelor semester project, supervisor)
  17. Marco Z. (Freie Universität Berlin): Mixing automated theorem proving and machine learning, 2018. (Masters, co-supervisor)
  18. Samuel G. (Freie Universität Berlin): Effizientes Parsen von Problemen der Prädikatenlogik höherer Stufe in THF-Syntax für den Theorembeweiser Leo-III, 2016. (Bachelors, co-supervisor)
  19. Tobias G. (Freie Universität Berlin): Converting Higher-Order Model Logic Problems into Classical Higher-Order Logic, 2016. (Bachelors, co-supervisor)

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.

Miscellaneous

Links

Further Documents

  1. Nitpicking Lambda-Free Higher-Order Logic, Retracted manuscript, original version, 2019. See also the discussion on the Matryoshka mailing list.
  2. Nullstellen von Polynomen und Erweiterungskörper, Seminar paper on Finite Fields, 2014
  3. Embedding of Quantified Modal Logic in Higher Order Logic, Seminar paper on Expressive Logics and their Automation, 2014
  4. The Drinking Philosophers Problem: Resource Allocation in Distributed Systems, Seminar paper on Distributed Programming, 2014.