Christoph Benzmüller
Articulate Software, Angwin, CA, USA
c.benzmueller@googlemail.com
 
Short Bio | Research | Publications | Talks | Academic Activities | Teaching | Student Projects
 
For more than a decade Christoph Benzmüller has been working as a researcher at the boundry of Automated Reasoning, Computational Logic, Artificial Intelligence, Computer-supported Mathematics, Cognitive Science and Computational Linguistics.
 
Main Projects
 
  ONTOLEO: Higher-Order Ontology-Reasoning with LEO-II (ongoing work)
  LEO-II: An Effective Higher-Order Theorem Prover (World Champion 2010, ongoing work)
  THFTPTP: An Infrastructure for Higher-order Automated Theorem Proving (ongoing work)
  OMEGA: Agent-oriented Proof Planning
  DIALOG: NL based Interaction with a Mathematics Assistance System
  OANTS: Agent-oriented Theorem Proving
 
Recommended (personal involvement): IFCOLOG, MIPS-2010, IFIP-SEC-2010, AISC-2010, IJCAR-2010, AIA-2010, EMS+QMS 2010 , UITP'10
 
Some Recent Publications (for a complete list see here)
 
* Reasoning with Embedded Formulas and Modalities in SUMO. ECAI 2010 Workshop ARCOE'10, 2010.
* Ontology Archaeology: Mining a Decade of Effort on the Suggested Upper Merged Ontology. ECAI 2010 Workshop ARCOE'10, 2010.
* Sigma: An Integrated Development Environment for Logical Theory Development. ECAI 2010 Workshop IKBET'10, 2010.
* Combining Logics in Simple Type Theory. ECAI 2010 Workshop CLIMA XI, 2010.
* Progress in Automating Higher-Order Ontology Reasoning. PAAR-2010.
* Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure. Journal of Formalized Reasoning, 2010.
* Simple Type Theory as Framework for Combining Logics. UNILOG-2010.
* Multimodal and Intuitionistic Logics in Simple Type Theory. Logic Journal of the IGPL, 2010.
* A Note on LEO-II and the Basic Fragment of Simple Type Theory. AAR Newsletter No. 84, July 2009.
* Presenting Proofs with Adapted Granularity. KI-2009, 2009.
* Progress in the Development of Automated Theorem Proving for Higher-order Logic. CADE-22, 2009.
* Granularity-Adaptive Proof Presentation AIED2009, 2009.
* Quantified Multimodal Logics in Simple Type Theory. SEKI Report SR-2009-02, 2009.
* Automating Quantified Multimodal Logics in Simple Type Theory -- A Case Study. SEKI Working-Paper SWP-2009-02, 2009.
* Granularity-Adaptive Proof Presentation SEKI Working-Paper SWP-2009-01, 2009.
  Reasoning in Simple Type Theory -- Festschrift in Honor of Peter B. Andrews. College Publications, 2008.
* Lectures on Jacques Herbrand as a Logician. SEKI Report SR-2009-01, 2009. (See also the related article 'Jacques Herbrand: Life, Logic, and Automated Deduction' in the Handbook of the History of Logic, Elsevier, 2008).
* Proof Granularity as an Empirical Problem? CSEDU, 2009.
* Automating Access Control Logic in Simple Type Theory with LEO-II. IFIP/SEC-2009.
* Cut-Simulation and Impredicativity. Logical Methods in Computer Science, 2009.
* Proof Step Analysis for Proof Tutoring -- A Learning Approach to Granularity. Teaching Mathematics and Computer Science. 2009.
* LEO-II - A Cooperative Automatic Theorem Prover for Higher-Order Logic. IJCAR'08.
* The Core TPTP Language for Classical Higher-Order Logic. IJCAR'08.
* Organisation, Transformation, and Propagation of Mathematical Knowledge in Omega. Mathematics in Computer Science. 2009.
* Resource-bounded Modelling and Analysis of Human-level Interactive Proofs. Book on the SFB 378.
* OMEGA: Resource Adaptive Processes in an Automated Reasoning System. Book on the SFB 378.
* Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II. Festschrift in Honor of Peter B. Andrews, 2008.
* Cut Elimination with Xi-Functionality. Festschrift in Honor of Peter B. Andrews, 2008.
* Combined Reasoning by Automated Cooperation. JAL, 2008.
 
Hobbies (see some pictures)
 
I am still a passionate middle and long-distance runner. More than a decade ago I lived and trained at the Olympic Centre in Saarbrücken. In 1990 I was German Champion with the men's team in cross-country running. Feel free to beat some of my personal records: 2:25min (1000m), 3:49min (1500m), 8:14 (3000m), 14:13min (5000m), 30:04min (10000m). Since 2004 I am occasionally starting again in some street races; here are some recent results.
 
Recently, I have also become an enthusiastic diver. Furthermore, I like skiing and reading newspapers.
 
 
C. Benzmüller, 2010