News / Events

Recent news

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.
December 2018: Together with Claudia Schon (U Koblenz), I was appointed Speaker (Sprecher) of the special interest group on deduction systems (Fachgruppe Deduktionssysteme) of the German Informatics Society (Gesellschaft für Informatik (GI)). Thanks for the trust!
September 2018: I was awarded a Junior-Fellowship of the German Gesellschaft für Informatik (GI) at this year's #INFORMATIK2018 (September 26, 2018, in Berlin). See also the official press release (german).

Recommended upcoming events (partially with personal involvement)

Feburary 27-29, 2020: Internationales Rechtsinformatik Symposion (IRIS 2020), Salzburg, Austria. (participant)
March 22-27, 2020: 5th Conference on Artificial Intelligence and Theorem Proving (AITP 2020), Aussois, France.
April 6-9 2020: Zhejiang Conferences on Logics in Artificial Intelligence (ZJULogAI 2020), Hangzhou, China. (Co-organizer)
April 6-9 2020: 6th Global Conference on Artificial Intelligence GCAI 2020, Hangzhou, China.
April 27-29, 2020: PhDs in Logic XII, Berlin, Germany. (Invited Speaker)
May 9-13, 2020: International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2020), Auckland, New Zealand. (PC member)
June 8-12, 2020: 24th European Conference on Artificial Intelligence (ECAI 2020), Santiago de Compostela, Spain. (participant)
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: 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: 15th International Conference on Deontic Logic and Normative Systems (DEON 2020), Munich, Germany.

About

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

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

2018 –
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)
2014 - 2018
Research assistant (wiss. Mitarbeiter) at the Dahlem Center for Machine Learning and Robotics, DFG project Leo-III and project CRAP: Consistent Rational Argumentation in Politics funded by Volkswagen Foundation, 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.

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)

Professional Activities

Organizations

Program Committees/Conference Organization

2020
2019
2018
2015
CADE-25 (local co-organizer)

Past Administrative Academic Services

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

See also: [google scholar] [dblp] [orbi.lu]
  1. Alexander Steen, Christoph Benzmpller, The Higher-Order Prover Leo-III. In 24th European Conference on Artificial Intelligence (ECAI 2020), Proceedings, 2020. (to appear).
  2. Alexander Steen, Extensional Paramodulation for Higher-Order Logic and its Effective Implementation Leo-III (Dissertation Abstract). In Künstliche Intelligenz, 2019. (to appear).
  3. Claudia Schon, Alexander Steen (Eds.), Deduktionstreffen 2019, Proceedings. Informal workshop proceedings.
  4. 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.
  5. Alexander Steen, Christoph Benzmüller, Extensional Higher-Order Paramodulation in Leo-III. Submitted article, preprint available at arXiv:1907.11501.
  6. Alexander Steen, Guest Column: Challenges in Higher-Order Theorem Proving. Association for Automated Reasoning, Newsletter No. 128, July 2019.
  7. Alexander Steen, Christoph Benzmüller The Higher-Order Prover Leo-III (extended abstract). In Künstliche Intelligenz 2019, Proceedings, LNCS, Vol. 11793, Springer, 2019.
  8. 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.
  9. 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.
  10. Alexander Steen, Extensional Paramodulation for Higher-Order Logic and its Effective Implementation Leo-III. Dissertation, Freie Universität Berlin. Published in Dissertations in Artificial Intelligence (DISKI), volume 345, EAN/ISBN 978-3-89838-739-2, AKA-Verlag, 2018.
  11. 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.
  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, 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.
  14. 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.
  15. Alexander Steen, Leo-III: A Theorem Prover for Classical and Non-Classical Logics, Automated Reasoning Workshop 2018, Cambridge, UK (mildly reviewed).
  16. Alexander Steen, Christoph Benzmüller, The Higher-Order Theorem Prover Leo-III, arXiv:1802.02732, CoRR, 2017. https://arxiv.org/abs/1802.02732.
  17. 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.
  18. 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.
  19. 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.
  20. 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.
  21. 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.
  22. 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.
  23. 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.
  24. 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.
  25. 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.
  26. 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.
  27. 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.
  28. 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.
  29. 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)
  30. 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.
  31. 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.
  32. Alexander Steen, Efficient Data Structures for Higher-Order Reasoners (Poster). Deduktionstreffen 2015, Berlin, Germany, 2015.
  33. 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.
  34. 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.
  35. Alexander Steen, Efficient Data Structures for Automated Theorem Proving in Expressive Higher-Order Logics. Master Thesis, Freie Universität Berlin, 2014.
  36. 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.
  37. 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.
  38. Alexander Steen, Generation and State-Space Reduction of Program Graphs for Non-deterministic Programs. Bachelor Thesis, Freie Universität Berlin, 2012.

Teaching

I completed the advanced training certificate for unversity teaching (Hochschuldidaktisches Lehrzertifikat) of Freie Universität Berlin (Support für die Lehre).

Current and past teaching activities

  1. Summer 20: Intelligent Agents 1: Knowledge Representation, University of Luxembourg, Lecturer, together with Leon van der Torre
  2. Winter 19: Intelligent Systems: Agents and Reasoning, University of Luxembourg, Lecturer
  3. Winter 19: Automated Deduction with legal texts, Tutorial at ICAIL 2019, Montreal, Canada
  4. Winter 18: Intelligent Agents II, University of Luxembourg, Co-lecturer
  5. Summer 17: WYSIWYG-Editor for Higher Order Logic, 10 ECTS, Co-instructor
  6. Winter 16/17: Seminar on Higher-Order Theorem Proving, 5 ECTS, Instructor
  7. Winter 16/17: Planung, Durchführung und Analyse eines Tutoriums (Conception and conduction of a tutorial), 5 ECTS, Instructor
  8. Summer 16: Künstliche Intelligenz (artificial intelligence), 5 ECTS, Tutorial sessions
  9. Summer 16: Computational Metaphysics, 5 ECTS, Instructor
  10. Summer 16: Planung, Durchführung und Analyse eines Tutoriums (Conception and conduction of a tutorial), 5 ECTS, Instructor
  11. Winter 15/16: Programmieren (Programming Basics), 5 ECTS, Stand-in Lecturer
  12. Summer 15: Proseminar Logik (Seminar on logic), 5 ECTS, Instructor
  13. Summer 15: ALP IV: Nichtsequentielle Programmierung (Concurrent programming), 5 ECTS, Lecturer (mit Lehrauftrag)
  14. Winter 14/15: Entwicklung eines netzbasierten Editors zur Generierung von PDF-Dokumenten (Software project), 10 ECTS, Instructor
  15. Winter 14/15: ALP V: Netzprogrammierung (Network programming), 5 ECTS, Tutorial session (mit Lehrauftrag)
  16. Winter 14/15: Expressive Logiken -- Theorie, Mechanisierung, Anwendungen (Theory, Automatization and Applications of Expressive Logics), 5 ECTS, Tutorial session
  17. Winter 13/14: ALP V: Netzprogrammierung (Network programming), Tutorial session
  18. Summer 13: Realworld Haskell (advanced functional programming), Lecturer & Tutorial session
  19. Summer 13: Hacken mit Haskell (introduction to functional programming for senior high school students), Lecturer
  20. Summer 13: ALP IV: Nichtsequentielle Programmierung (Concurrent programming), Tutorial session
  21. Winter 12/13: ALP V: Netzprogrammierung (Network programming), Tutorial session
  22. July/August 12: ProInformatik II - Funktionale Programmierung (Functional programming), Tutorial session (mit Lehrauftrag)
  23. Summer 12: ALP IV: Nichtsequentielle Programmierung (Concurrent programming), Tutorial session
  24. Winter 11/12: ALP I: Funktionale Programmierung (Functional programming), Tutorial session
  25. Summer 11: ALP IV: Nichtsequentielle Programmierung (Concurrent programming), Tutorial session
  26. 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. Federico G. (University of Bologna): AI-mediated commercial practices and the duty to trade fairly. (PhD, committee member (CET))
  2. Paul P. (Freie Universität Berlin): Verifiable Smart contracts (working title). (Masters, co-supervisor)
Past/completed
  1. Tobias G. (Freie Universität Berlin): A Framework for Higher-Order Modal Logic Theorem Proving, 2019. (Masters, supervisor)
  2. Gavin G. (American University of Paris): Summer internship on programming and legal tech, 2019.
  3. Marco Z. (Freie Universität Berlin): Mixing automated theorem proving and machine learning, 2018. (Masters, co-supervisor)
  4. 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)
  5. 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? 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.