News

April 2017: Invited lecture on Calculemus!: Analyse von Kurt Gödel's Gottesbeweis mit dem Computer by Christoph Benzmüller at Urania Berlin on June 16th 2017.

March 2017: On March 27th, 4pm, Christoph Benzmüller gives an invited lecture on Computational Metaphysics: The Virtues of Formal Proofs Beyond Math in the scope of ILIAS Distinguished Lectures at University of Luxembourg (Maison du Savoir, Room 04-4.020, Campus Belval).

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

Based on successful previous work by Benzmüller and Woltzenlogel-Paleo on the formalisation and verification of Kurt Gödel's variant of the Ontological Argument (for the existence of God) on the computer, we have set-up a research team and associated lecture courses on Computational Metaphysics and its foundations at FU Berlin. Our project targets the formalisation and deep logical analysis of rational arguments from metaphysics (i.e. theoretical philosophy and other areas) on the computer. Computer-formalisation of rational arguments presupposes and incorporates their digitalisation. At the same time our project pioneers a novel research direction towards computational humanities: it demonstrates that the logical quality of (selected) rational arguments in theoretical philosophy can meanwhile be rigorously analysed and assessed by modern artificial intelligence systems, so called interactive and automated theorem provers. As we have demonstrated, computer systems may help to detect errors in published arguments in philosophy and they may even contribute novel philosophical knowledge. While the focus of our studies so far has been on rational arguments from metaphysics, our approach is by no means restricted to this domain and it generally links very well with the objectives of the new collaborative research center \emph{Robust Argumentation Machines (RATIO, SPP 1999)}; in this context it can be seen as a forerunner project. In fact, we have meanwhile exemplarily applied our technology also to a range of arguments, texts and proofs in mathematics, artificial intelligence, computer science and computational linguistics.

See also DFG Heisenberg programme

Resources and Further References

Formalizations

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

Leo-III

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

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.

Publications

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, http://arxiv.org/abs/1609.01493, 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.