Alexander Steen

Recent news

May 2018: The Modal Embedding Tool (MET) Version 1.0 has been released! Also see the LPAR-21 paper.
May 2018: Our system description of Leo-III got accepted at IJCAR 2018 in Oxford. Also see the extended version of the paper at arXiv:1802.02732.
December 2017: Version 1.2 of Leo-III has been released! See the release notes for details.
August 2017: 2nd place for Leo-III in CASC-26 THF division, see CASC results page.

Recommended events (personal involvement)

June 25-27, 2018: First European Workshop on Higher-Order Automated Reasoning, Amsterdam, The Netherlands (attendee, speaker)
July 14-17, 2018: 9th International Joint Conference on Automated Reasoning, Oxford, UK (attendee, speaker)
September 17-19, 2018: 4th Global Conference on Artificial Intelligence (GCAI 2018), Luxembourg (pc member)
September 18-21, 2018: 2nd International Joint Conference on Rules and Reasoning (RuleML+RR 2018), Luxembourg (poster session chair)
September 21, 2018: Jahrestreffen der Fachgruppe Deduktionssysteme der Gesellschaft der Informatik (Deduktionstreffen 2018), Luxembourg (program co-chair)

This is the personal homepage of Alexander Steen. I am a researcher and doctoral student at the Artificial Intelligence group of the Institute of Computer Science at the FU Berlin. I'm currently working on the Leo-III system, an massively parallel automated theorem prover (ATP) for expressive higher-order logics.

My current research investigates efficient data structures for higher-order theorem proving 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

Since 2015

PhD student, Computer Science, working title: An Extensional Ordered Paramodulation Calculus for HOL, advisor: Christoph Benzmüller

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/Matura), Lichtenberg-Gymnasium, Cuxhaven, Germany

Professional Affiliations

2018 -

Researcher (wiss. Mitarbeiter) at the Dahlem Center for Machine Learning and Robotics for the project CRAP: Consistent Rational Argumentation in Politics, Freie Universität Berlin

2014 - 2018

Researcher (wiss. Mitarbeiter) at the Dahlem Center for Machine Learning and Robotics for the DFG project Leo-III, 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

Current Administrative Academic Services

Since 2017

• Deputy member of the Teaching Committee (Kommission für Lehrangelegenheiten) of Freie Universität Berlin
• Deputy member of the tutor selection committee for Computer Science studies (Tutorenauswahlkommission Informatik)

Since 2016

Member of the faculty council (Fachbereichsrat)

Since 2015

• Member of the examination board for the Bachelor degree in Computer Science (Prüfungsausschuss Informatik Bachelor und Lehramt)
• Member of the examination board for the Master and Diploma degree in Computer Science (Prüfungsausschuss Informatik Master/Diplom)
• Member of the institute administrative council (Institutsleitung)

Past Services

2017 - 2018

Deputy Member of the Extended Academic Senate of Freie Universität Berlin (Erweiterter Akademischer Senat)

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

Prizes, Honors etc.

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)

1. 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. (To appear)
2. 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, 2018. (To appear)
3. Alexander Steen, Leo-III: A Theorem Prover for Classical and Non-Classical Logics, Automated Reasoning Workshop 2018, Cambridge, UK (mildly reviewed).
4. Alexander Steen, Christoph Benzmüller, The Higher-Order Theorem Prover Leo-III, arXiv:1802.02732, CoRR, 2017. https://arxiv.org/abs/1802.02732.
5. 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.
6. 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.
7. 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.
8. 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.
9. 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.
10. 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.
11. 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.
12. 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.
13. 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 (ARNQL 2016), Coimbra, Portugal, July 2016, Proceedings, CEUR Workshop Proceedings, Volume 1770, CEUR-WS.org, 2016.
14. 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.
15. 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.
16. 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.
17. 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)
18. 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.
19. 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.
20. Alexander Steen, Efficient Data Structures for Higher-Order Reasoners (Poster). Deduktionstreffen 2015, Berlin, Germany, 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.
22. 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.
23. Alexander Steen, Efficient Data Structures for Automated Theorem Proving in Expressive Higher-Order Logics. Master Thesis, Freie Universität Berlin, 2014.
24. 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.
25. 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.
26. Alexander Steen, Generation and State-Space Reduction of Program Graphs for Non-deterministic Programs. Bachelor Thesis, Freie Universität Berlin, 2012.

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 17: WYSIWYG-Editor for Higher Order Logic, 10 ECTS, Co-instructor
2. Winter 16/17: Seminar on Higher-Order Theorem Proving, 5 ECTS, Instructor
3. Winter 16/17: Planung, Durchführung und Analyse eines Tutoriums (Conception and conduction of a tutorial), 5 ECTS, Instructor
4. Summer 16: Künstliche Intelligenz (artificial intelligence), 5 ECTS, Tutorial sessions
5. Summer 16: Computational Metaphysics, 5 ECTS, Instructor
6. Summer 16: Planung, Durchführung und Analyse eines Tutoriums (Conception and conduction of a tutorial), 5 ECTS, Instructor
7. Winter 15/16: Programmieren (Programming Basics), 5 ECTS, Stand-in Lecturer
8. Summer 15: Proseminar Logik (Seminar on logic), 5 ECTS, Instructor
9. Summer 15: ALP IV: Nichtsequentielle Programmierung (Concurrent programming), 5 ECTS, Lecturer (mit Lehrauftrag)
10. Winter 14/15: Entwicklung eines netzbasierten Editors zur Generierung von PDF-Dokumenten (Software project), 10 ECTS, Instructor
11. Winter 14/15: ALP V: Netzprogrammierung (Network programming), 5 ECTS, Tutorial session (mit Lehrauftrag)
12. Winter 14/15: Expressive Logiken -- Theorie, Mechanisierung, Anwendungen (Theory, Automatization and Applications of Expressive Logics), 5 ECTS, Tutorial session
13. Winter 13/14: ALP V: Netzprogrammierung (Network programming), Tutorial session
14. Summer 13: Realworld Haskell (advanced functional programming), Lecturer & Tutorial session
15. Summer 13: Hacken mit Haskell (introduction to functional programming for senior high school students), Lecturer
16. Summer 13: ALP IV: Nichtsequentielle Programmierung (Concurrent programming), Tutorial session
17. Winter 12/13: ALP V: Netzprogrammierung (Network programming), Tutorial session
18. July/August 12: ProInformatik II - Funktionale Programmierung (Functional programming), Tutorial session (mit Lehrauftrag)
19. Summer 12: ALP IV: Nichtsequentielle Programmierung (Concurrent programming), Tutorial session
20. Winter 11/12: ALP I: Funktionale Programmierung (Functional programming), Tutorial session
21. Summer 11: ALP IV: Nichtsequentielle Programmierung (Concurrent programming), Tutorial session
22. Winter 10/11: ALP I: Funktionale Programmierung (Functional programming), Tutorial session

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

Supervision of theses

Ongoing theses

n/a

Completed theses

• Samuel Gfrörer: Effizientes Parsen von Problemen der Prädikatenlogik höherer Stufe in THF-Syntax für den Theorembeweiser Leo-III, 2016 (Bachelors, co-supervisor)
• Tobias Gleißner: Converting Higher-Order Model Logic Problems into Classical Higher-Order Logic, 2016 (Bachelors, co-supervisor)
• Marco Ziener: Mixing automated theorem proving and machine learning, 2018 (Masters, 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.

Links

• Collegium Academicum Berlin e.V., at which I am serving at the steering committee.
• GitHub project for the visualization of three- and four-dimensional point groups that correspond to convex polytopes, created for a project course at FU Berlin, 2013/2014
• Vokalschola "ave florum flos"
• St. Paulus Chor Moabit
• Simple manual on how to create infinitely many ice cubes in practice (German): "...und einfach beliebig viele Eiswürfel entnehmen"

Further Documents

1. Nullstellen von Polynomen und Erweiterungskörper, Seminar paper on Finite Fields, 2014
2. Embedding of Quantified Modal Logic in Higher Order Logic, Seminar paper on Expressive Logics and their Automation, 2014
3. The Drinking Philosophers Problem: Resource Allocation in Distributed Systems, Seminar paper on Distributed Programming, 2014.