DFG Heisenberg research project
# Computational Metaphysics

Freie Universität Berlin

Department of Mathematics and Computer Science

Institute for Computer Science

Department of Mathematics and Computer Science

Institute for Computer Science

Project funded by

German Research Foundation

German Research Foundation

**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:

- E. Badstübner, D. Kirchner, P. Schießl: The Theory of Abstract Objects
- M. Bentert, Y. Lewash, D. Streit, S. Stugk: Proving God's Existence by Automating Leibniz' Algebra of Concepts
- David Fuenmayor: Formalization and Assessment of Lowe's Modal Ontological Argument
- Lukas Grätz, Fabian Schütz: Computerized Verification of Formal Reconstructions of Anselm's Argument by Eder and Ramharter
- Daniel Dormagen, Irina Makarenko: Formalising Category Theory by Automating Free Logic in Higher-Order Logic
- Lukas Grätz: Leibniz’s ”Impossible Things”

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

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

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.

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

- Summer 2017
- Künstliche Intelligenz (
*Artifial intelligence*) - 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