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

• 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.
• Extensional 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


• The Inconsistency in Gödels Ontological Argument: A Success Story for AI in Metaphysics, IJCAI 2016.
• The 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, CSR, 2015.
• Quantified Multimodal Logics in Simple Type Theory, Logica Universalis, 2013.
• 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


• Free Logic in HOL, ICMS, 2016.


• 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


• Agent-Based 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, 2001.
• 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


• Proofs 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


• Automated Consistency Checking of Expressive Ontologies --- Beware of the Wrong Interpretation of Success!, ARCOE-LogIC, 2013.
• Sigma: An Integrated Development Environment for Formal Ontology, AI Communications, 2013.
• Progress in Automating Higher-Order Ontology Reasoning, PAAR, 2012.
• Higher-order Aspects and Context in SUMO, J. of Web Semantics, 2012.


• Proof Planning and Learning of Proof Methods


• Automatic Learning of Proof Methods in Proof Planning, Logic J.IGPL, 2003.
• Towards Learning New Methods in Proof Planning, Symb. Comp. and Autom. Reas., 2000.
• Assertion Application in Theorem Proving and Proof Planning, IJCAI, 2003.


• User Interfaces for Theorem Provers


• PLATO: A Mediator between Text-Editors and Proof Assistance Systems, ENTCS, 2007.
• DiaWOz-II - A Tool for Wizard-of-Oz Experiments in Mathematics, KI, 2006.
• LOUI: Lovely OMEGA User Interface, Formal Aspects of Computing, 1999.


• 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


• The CALCULEMUS Final Report, EU report, 2004.
• Systems for Integrated Computation and Deduction -- Interim Report of the CALCULEMUS IHP Network, EU report, 2003.
• CALCULEMUS-II: Computer-supported Mathematical Knowledge Evolution, EU Proposal, 2003.
• The CALCULEMUS research training network: A short overview, CALCULEMUS, 2003.
• CALCULEMUS Autumn School 2002: Course Notes, 2002.

An older description of my research can be found here.