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.
Info about the project here.
DFG Heisenberg programme more info
Selected list of relevant publications (reverse chronological order):
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.