Research Interests and Contributions:
I am a logician working on the boundary of
different disciplines: mathematical logic, computer science,
artificial intelligence, philosophy and computational
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
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
Below I list the most relevant publications (personal choice) wrt to
different research topics (these papers are available
- HOL: Semantics, Calculi, Proof Theory, Cut-Elimination
Automation of Higher-Order Logic, Handbook of the History of Logic, 2014.
- Cut-Simulation and Impredicativity, LMCS, 2009.
- Cut Elimination with Xi-Functionality, Festschrift Andrews, 2008.
- Higher-Order Semantics and Extensionality, JSL, 2004.
- Comparing Approaches to Resolution based Higher-Order Theorem
Proving, Synthese, 2002.
- Extensional Higher-Order Paramodulation and RUE-Resolution, CADE, 1999.
- Equality and Extensionality in Higher-Order Theorem Proving, PhD thesis, 1999.
Higher-Order Resolution, CADE, 1998.
- HOL: Automated Theorem Proving
- Effective Normalization Techniques for HOL, IJCAR, 2016.
- The Higher-Order Prover LEO-II, JAR, 2015.
- Higher-Order Automated Theorem Provers, All about Proofs, Proofs for All, 2015.
- Automated Reasoning in Higher-Order Logic using the TPTP THF
Infrastructure, J. Formalized Reasoning, 2010.
- Progress in the Development of Automated Theorem Proving for
Higher-order Logic, CADE, 2009.
- THF0 -- The Core of the TPTP Language for Classical Higher-Order Logic, IJCAR 2008.
- LEO-II -- A Cooperative Automatic Theorem Prover for Higher-Order Logic, IJCAR, 2008.
- A Structured Set of Higher-Order Problems, TPHOLs, 2005.
- Can a Higher-Order and a First-Order Theorem Prover Cooperate?, LPAR, 2004.
- LEO -- A Higher-Order Theorem Prover, CADE, 1998.
- Computational Metaphysics
Inconsistency in Gödels Ontological Argument: A Success
Story for AI in Metaphysics, IJCAI 2016.
Modal Collapse as a Collapse of the Modal Square of
Opposition, Studies in Universal Logic, 2016.
- Invited Talk: On a (Quite) Universal Theorem Proving Approach
and Its Application in Metaphysics, TABLEAUX, 2015.
- Computer-Assisted Analysis of the Anderson-Hajek Ontological
Controversy, 1st World Congress on Logic and Religion, 2015.
- Automating Gödel's Ontological Proof of God's Existence
with Higher-order Automated Theorem Provers, ECAI, 2014.
- Formalization, Mechanization and Automation of Gödel's
Proof of God's Existence, arXiv, 2013.
- Quantified Modal Logics
- Higher-Order Modal Logics: Automation and
Applications, Reasoning Web, 2015.
- Interacting with Modal Logics in the Coq Proof Assistant,
- Quantified Multimodal Logics in Simple Type Theory, Logica
- HOL based First-order Modal Logic Provers, LPAR, 2013.
- Implementing and Evaluating Provers for First-order Modal
Logics, ECAI, 2012.
- Exploring Properties of Normal Multimodal Logics in Simple
Type Theory with LEO-II, Festschrift Andrews, 2008.
- Other Quantified Non-Classical Logics
- Cut-Elimination for Quantified Conditional Logic, Journal of Philosophical Logic, 2016.
- Sweet SIXTEEN: Automation via Embedding into Classical
Higher-Order Logic, Logic and Logical Philosophy, 2016.
- Automating Quantified Conditional Logics in HOL, IJCAI, 2013.
- Embedding and Automating Conditional Logics in Classical
Higher-Order Logic, AMAI, 2012.
- Multimodal and Intuitionistic Logics in Simple Type Theory,
Logic J.IGPL, 2010.
- Automating Access Control Logic in Simple Type Theory with
LEO-II, SEC, 2009.
- Free Logic and Applications in Maths
- Meta-logical Reasoning and Logic Combinations
- Systematic Verification of the Modal Logic Cube in
Isabelle/HOL, EPTCS, 2015.
- A Top-down Approach to Combining Logics, ICAART, 2013.
- Combining and Automating Classical and Non-Classical Logics
in Classical Higher-Order Logic, AMAI, 2011.
- Simple Type Theory as Framework for Combining Logics, UNILOG, 2010.
- Verifying the Modal Logic Cube is an Easy Task, Festschrift Walther, 2010.
- Agent Based (Prover) Architectures and System Platforms
HOL Reasoning, ICMS, 2016.
- LeoPARD - A Generic Platform for the Implementation of
Higher-Order Reasoners, CICM, 2015.
- There Is No Best Beta-Normalization Strategy for Higher-Order
Reasoners, LPAR, 2015.
- Combined Reasoning by Automated Cooperation, J. Appl.Logic, 2008.
- OANTS -- Combining Interactive and Automated Theorem Proving,
Symb. Comp. and Autom. Reas., 2001.
- Experiments with an Agent-oriented Reasoning System, KI,
- An Agent Based Approach to Reasoning, AISB Convention, 2001.
- Critical Agents Supporting Interactive Theorem Proving, EPIA, 1999.
- A Blackboard Architecture for Guiding Interactive Proofs, AIMSA, 1998.
- Mathematical Proof Assistants and Proof Planning
and Reconstructions, FroCoS, 2015.
- OMEGA: Resource-Adaptive Processes in an Automated Reasoning Systems, Cognitive Technologies, 2010.
- The curious inference of Boolos in MIZAR and OMEGA,
Festschrift Trybulec, 2007.
- Editorial: Towards Computer Aided Mathematics, J.Appl.Logic, 2006.
- Computer Supported Mathematics with OMEGA, J.Appl.Logic, 2006.
- OMEGA, The Seventeen Provers of the World, 2006.
- OMEGA: Computer Supported Mathematics, KI, 2004.
- Proof Development in OMEGA: The Irrationality of Square Root
of 2, Thirty Five Years of Automating Mathematics, 2003.
- Proof Development with OMEGA, CADE, 2002.
- An Interactive Proof Development Environment + Anticipation =
A Mathematical Assistant?, CASYS, 1999.
- Integrating TPS and OMEGA, J.UCS, 1999.
- OMEGA: Towards a mathematical assistant, CADE, 1997.
- Reasoning in Computer Science Ontologies
- Proof Planning and Learning of Proof Methods
- User Interfaces for Theorem Provers
- Mathematical Knowledge Management
- Organisation, Transformation, and Propagation of Mathematical
Knowledge in Omega, Mathematics in Computer Science, 2008.
- A Generic Modular Data Structure for Proof Attempts
Alternating on Ideas and Granularity, MKM, 2005.
- Bridging Theorem Proving and Mathematical Knowledge
Retrieval, Festchrift Siekmann, 2004.
- OMEGA --- From Proof Planning towards Mathematical Knowledge
Management, MKM, 2003.
- Dialog and Tutoring Systems
- Resource-Bounded Modelling and Analysis of Human-Level
Interactive Proofs, Cognitive Technologies, 2010.
- Presenting Proofs with Adapted Granularity, KI, 2009.
- Granularity-Adaptive Proof Presentation, AIED, 2009.
- Proof Granularity as an Empirical Problem?, CSEDU, 2009.
- Proof Step Analysis for Proof Tutoring -- A Learning Approach
to Granularity, Teaching Mathematics and Computer Science, 2008.
- Deep Inference for Automated Proof Tutoring?, KI, 2007.
- An Agent-based Architecture for Dialogue Systems, PSI, 2006.
- Natural Language Dialog with a Tutor System for Mathematical
Proofs, Cognitive Systems, 2007.
- Deep Inference for Automated Proof Tutoring?, KI, 2007.
- A corpus of tutorial dialogs on theorem proving; the
influence of the presentation of the study-material, LREC 2006.
- System Description: A Dialog Manager supporting Tutorial
Natural Language Dialogue on Proofs, UITP, 2005.
- Mathematical Domain Reasoning Tasks in Natural Language
Tutorial Dialog on Proofs, AAAI, 2005.
- An annotated corpus of tutorial dialogs on mathematical theorem proving, LREC, 2004.
- A Wizard of Oz Experiment for Tutorial Dialogues in
Mathematics, AIED, 2003.
- Tutorial Dialogs on Mathematical Proofs, IJCAI-WS, 2003.
- Integration of Symbolic Computation and Symbolic Reasoning
An older description of my research can be found here.
C. Benzmüller (Last modified: Thu Jul 21 22:04:13 CEST 2016 )