Research Interests and Contributions: Christoph Benzmüller

I am a logician working on the boundary of different disciplines: mathematical logic, computer science, artificial intelligence, philosophy and computational linguistics.

My research is founded on an expressive mathematical logic: Church's type theory, also known as classical higher-order logic (HOL), which Church proposed as a foundation for mathematics. In my PhD work and afterwards I have worked on the semantics and the proof theory of (modern variants of) this logic. Moreover, I have significantly contributed to its mechanization and automation using computers.

From early on the architecture and implementation of my higher-order automated theorem provers LEO-I, LEO-II and Leo-III, integrated artificial intelligence techniques and ideas. LEO-II and Leo-III are also employing state of the art implementation techniques and data structures from computer science. The provers have found international acclaim; for example, LEO-II was the TPTP world champion in higher-order automated theorem proving in 2010.

Most importantly, however, the development of the LEO-II prover paralleled and strongly influenced the joint development of the international TPTP THF infrastructure. The THF syntax format has been adopted by several other provers and it very successfully serves as an exchange format between interactive proof assistants (such as Isabelle/HOL) and the HOL automated theorem provers.

I have applied HOL theorem provers in various domains, including computer science, maths, artificial intelligence and most recently philosophy (metaphysics). In recent experiments in computational metaphysics my theorem LEO-II has contributed some very relevant but previously unknown results about the ontological argument (in Kurt Gödel's version) for the existence of God.

To make this possible, I had previously shown how classical HOL can be utilized as a meta-logic to elegantly and effectively embed various quantified non-classical logics, including higher-order modal logic as employed in Gödel's proof.

This work in metaphysics, which has some obvious relation to Leibniz' vision known as Calculemus! and which provides a promising link between maths, computer science and philosophy, had a media repercussion on a global scale.

In addition to these core research contributions, I have also headed research projects on the edge to computational linguistics (natural language dialog), tutoring, human-computer interaction and (proof) planning. A significant time in my early career went into the OMEGA project (mathematical proof assistant) and the Calculemus research training network (integration of symbolic computation and symbolic reasoning).

Below I list the most relevant publications (personal choice) wrt to different research topics (these papers are available here).

An older description of my research can be found here.

C. Benzmüller (Last modified: Thu Jul 21 22:04:13 CEST 2016 )