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.
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):