November 2016: Student's poster presentation (small selection) on group topics of Computational Metaphysics Summer 2016 at Urania on December 16th, 1pm. Posters/Topics presented:

November 2016: Invited BMS Friday talk by Christoph Benzmüller on "Computational Metaphysics: The Virtues of Formal Proofs Beyond Maths", Decmber 16th, 2:15 pm, Urania.

May 2016: Our lecture concept on "Computational Metaphysics" won the Central Teaching Award of Freie Universität Berlin. More information on the course: lecture course proposal and website/schedule.

General Information

Introduction text

Info about the project here.

DFG Heisenberg programme more info


Selected list of relevant publications (reverse chronological order):

  • Computer-Assisted Analysis of the Anderson-Hájek Controversy (Christoph Benzmüller, Leon Weber, Bruno Woltzenlogel-Paleo), In Logica Universalis, 2017. To appear.
  • Analysis of an Ontological Proof Proposed by Leibniz (Matthias Bentert, Christoph Benzmüller, David Streit, Bruno Woltzenlogel-Paleo), Chapter in Death and Anti-Death, Volume 14: Four Decades after Michael Polanyi, Three Centuries after G. W. Leibniz (Charles Tandy, ed.), Ria University Press, 2017. To appear.
  • An Object-Logic Explanation for the Inconsistency in Gödel's Ontological Theory (Extended Abstract) (Christoph Benzmüller, Bruno Woltzenlogel Paleo), In KI 2016: Advances in Artificial Intelligence, Proceedings (Malte Helmert, Franz Wotawa, eds.), Springer, LNCS, 2016.
  • Einsatz von Theorembeweisern in der Lehre (Max Wisniewski, Alexander Steen, Christoph Benzmüller), In Hochschuldidaktik der Informatik: 7. Fachtagung des GI-Fachbereichs Informatik und Ausbildung/Didaktik der Informatik; 13.-14. September 2016 an der Universität Potsdam (Andreas Schwill, Ulrike Lucke, eds.), Universitätsverlag Potsdam, Commentarii informaticae didacticae (CID), 2016.
  • TPTP and Beyond: Representation of Quantified Non-Classical Logics (Max Wisniewski, Alexander Steen, Christoph Benzmüller), In ARQNL 2016. Automated Reasoning in Quantified Non-Classical Logics (Christoph Benzmüller, Jens Otten, eds.), 2016.
  • Axiomatizing Category Theory in Free Logic (Christoph Benzmüller, Dana S. Scott), arXiv,, 2016.
  • Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic (Alexander Steen, Christoph Benzmüller), In Logic and Logical Philosophy, 2016.
  • Computer-Assisted Analysis of the Anderson-Hájek Controversy (Christoph Benzmüller, Leon Weber, Bruno Woltzenlogel-Paleo), In Logica Universalis, 2016.
  • Cut-Elimination for Quantified Conditional Logic (Christoph Benzmüller), In Journal of Philosophical Logic, 2016.
  • Automating Free Logic in Isabelle/HOL (Christoph Benzmüller, Dana Scott), In Mathematical Software -- ICMS 2016, 5th International Congress, Proceedings (G.-M. Greuel, T. Koch, P. Paule, A. Sommese, eds.), Springer, LNCS, volume 9725, pp. 43-50, 2016.
  • The Inconsistency in Gödel's Ontological Argument: A Success Story for AI in Metaphysics (Christoph Benzmüller, Bruno Woltzenlogel Paleo), In IJCAI 2016 (Subbarao Kambhampati, ed.), AAAI Press, volume 1-3, pp. 936-942, 2016.
  • The Modal Collapse as a Collapse of the Modal Square of Opposition (Christoph Benzmüller, Bruno Woltzenlogel-Paleo), Chapter in The Square of Opposition: A Cornerstone of Thought (Collection of papers related to the World Congress on the Square of Opposition IV, Vatican, 2014) (Jean-Yves Béziau, Gianfranco Basti, eds.), Springer International Publishing Switzerland 2016, Studies in Universal Logic, 2016.
  • Quantified Multimodal Logics in Simple Type Theory (Christoph Benzmüller, Lawrence Paulson), In Logica Universalis (Special Issue on Multimodal Logics), volume 7, number 1, pp. 7-20, 2013.

Associated Teaching

Summer 2017
Computational Metaphysics (planned)
Winter 2016/2017
Seminar on Higher-Order Theorem Proving
Summer 2016
Computational Metaphysics
Künstliche Intelligenz
Summer 2015
Proseminar Logik
Künstliche Intelligenz
Winter 2014/2015
Expressive Logiken - Theorie, Mechanisierung, Andnwendungen

Further References and Resources


Formalization sources, papers and various other related material are freely accessible via our GitHub repository.


In the Leo-III project, we turn LEO-II into a state-of-the-art theorem prover based on ordered paramodulation/ superposition. In constrast to LEO-II, we replace the internal term representation (the commonly used simply typed lambda calculus) by a more expressive system supporting type polymorphism. In the course of the project, we plan to further enhance the type system with type classes and type constructors similar to System Fω . In order to achieve a substantial performance speed-up, the architecture of Leo-III will be based on massive parallelism (e.g. And/Or-Parallelism, Multisearch).

More information can be found on the Leo-III project web site.


LEO-II is a standalone, resolution-based higher-order theorem prover designed for fruitful cooperation with specialist provers for natural fragments of higher-order logic. At present LEO-II can cooperate with TPTP compliant first-order automated theorem provers such as E, SPASS, Gandalf and Vampire. LEO-II was the winner of the THF division (automation of higher-order logic) at CASC-J5. LEO-II was the first theorem prover to support THF, FOF and CNF syntax.

More information can be found on the LEO-II project web site.