Hompage of

Max Wisniewski

Computer Science Department
Freie Universität Berlin

Max Wisniewski
Arnimallee 7 Room 113
14195 Berlin

Contact Information
Mail : m.wisniewski[ät]fu-berlin.de
Tel : +49 (0)30 838-75101
Office hours: whenever I'm there


I am a research assistant and doctoral student at Freie Universität Berlin in the artificial intelligence group.

Currently I am working mainly on the Leo-III project. Our goal is to develop a new Higher-Order Theorem Prover based on heavily use of parallelism. I investigate and evaluate whether an agent-based approach can be beneficial to theorem proving on various levels of the proof process.

In my free time I lend my voice to the bass of the Schola Vocalis Ave Florum Flos.


Ongoing projects:


  1. 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. Accepted for publication, to appear in 2016.
  2. 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, LNCS, 2016. To Appear in 2016.
  3. Max Wisniewski, Christoph Benzmüller, Is it Reasonable to Employ Agents in Theorem Proving? In Proc. of the 8th International Conference on Agents and Artificial Intelligence (ICAART), SciTePress Digital Library, 2016.
  4. Max Wisniewski, Agents and Organization in a Higher-Order Theorem Prover(Poster), Deduktionstreffen 2015, 2015 Berlin, Germany, 2015.
  5. Max Wisniewski, Alexander Steen, Christoph Benzmüller, LeoPARD - A Generic Platform for the Implementation of Higher-Order Reasoners, In Mafred Kerber, Jacque Carette, Cezary Kaliszyk, Florian Rabe, Volker Sorge (Eds.), Intelligent Computer Mathematics - International Conference. CICM 2015, Washington DC., USA, Juliy 13-17. 2015, Proceedings Springer, LNCS, volume 9150, pp. 325--330, 2015
  6. 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.), Handbook of the 5th World Congress and School on Universal Logic (UNILOG'15), Istanbul, Turkey, pp. 337--339, 2015.
  7. Max Wisniewski, Multiagent Blackboard Architexture for Automated Theorem Proving in Expressive Higher Order Logic. Master Thesis, Freie Universität Berlin, 2014.
  8. Max Wisniewski, Alexander Steen, Christoph Benmüller, The Leo-III Project. In Alexander Bolotov, Manfred Kerber (Eds.), Joint Automated Reasoning Workshop and Deduktionstreffen 2014.
  9. Max Wisniewski, Alexander Steen, Embedding of Quantified Higher-Order Nominal Modal Logic into Classical Higher-Order Logic. In Christoph Benzmüller, Jens Otten (Eds.), Automated Reasoning in Quantified Non-Classical Logics, Proceedings of the 1st international Workshop, Vienna, Austria, 2014.
  10. Max Wisniewski, Expression Evaluation in a Concurrent Programming Language Using a SMT-Solver , Bachelor Thesis, Freie Universität Berlin, 2012.


Zentraler Lehrpreis (Teaching award) of the Freie Universität Berlin for the concept of a lecture on Computational Metaphysics (Press release: german, english)


  1. Summer 16: Computational Metaphysics Instructor
  2. Winter 15/16: Programmieren (Programming), Lecturer
  3. Summer 15: Proseminar Logik, Instructor
  4. Winter 14/15: Programmieren in Java (Java programming course), Lecturer
  5. Winter 14/15: Entwicklung eines netzbasierten Editors zur Generierung von PDF-Dokumenten (Software project), Instructor
  6. Winter 14/15: Expressive Logiken -- Theorie, Mechanisierung, Anwendung (Theory, Automatization and Application of Expressive Logics), Tutorial session.
  7. Winter 13/14: ALP I: Funktionale Programmierung (funktional programming), Tutorial session
  8. Summer 13: ALP IV: Nichtsequentielle Programmierung (concurrent programming), Tutorial session.
  9. Winter 12/13: ALP III: Datenstrukturen und Abstraktion (datastructures and abstraction) Tutorial session
  10. Summer 12: ALP IV: Nichtsequentielle Programmierung (concurrent programming), Tutorial session.
  11. Winter 11/12: ALP III: Datenstrukturen und Abstraktion (datastructures and abstraction) Tutorial session
  12. Summer 11: ALP IV: Nichtsequentielle Programmierung (concurrent programming), Tutorial session.
  13. Winter 10/11: ALP III: Datenstrukturen und Abstraktion (datastructures and abstraction) Tutorial session
  14. Summer 10: ALP II: Object orientierte Programmierung (object based programming), Tutorial session.
    1. ⇓Full list⇓

Further Links