to be updated...
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).
Consistent, rational argumentation in politics (and other contexts)
seems on the retreat, while socially dangerous, inconsistent and
irrational propaganda is on the rise. The question is whether
knowledge representation and reasoning techniques from artificial
intelligence can help to analyse and rigorously assess arguments in
politics (and beyond). The objective of CRAP is to exemplarily
formalise selected arguments on the computer using Benzmüller's
shallow semantical embedding technique, and to subsequently assess
their deep logical representations using latest automated reasoning
technology. CRAP wants to raise awareness of logical
consistency as an essential ingredient of rational argumentation.
In the past decades powerful proof assistants with trusted logical kernels have been
developed, and in own work (and that of others) they have been
successfully applied in frontier applications in mathematics and
metaphysics. However, the deep logical analysis of political arguments
is a challenge no one has attempted before. Political rhetoric is
often messy, contains noise, and plays with ambiguities and near
fallacies. It is here where a respective computer-supported methodology for formal
argument assessment could have a significant impact, when being
applied to some carefully selected arguments from recent political
debates. Their scientific dissection in combination with a careful
reflection and (public) discussion of the results could eventually
raise the awareness about the nature, the danger and the patterns of
irrationality that is rapidly spreading out in today's political culture.
See also Volkswagenstiftung project index
To be provided soon.
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):
