PD Dr.-Ing. Christoph Benzmüller
Heisenberg Fellow of the German Research Foundation
Department of Mathematics and Computer Science
Free University Berlin

c.benzmueller[at]googlemail.com
 
Short Biography | Full Curriculum Vitae | Research | Publications | Talks | Lecture Courses
 
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
  OMEGA: Agent-oriented Proof Planning
  DIALOG: NL-based Interaction with a Mathematics Assistance System
  CALCULEMUS: Integration of Symbolic Reasoning and Symbolic Computation
  OANTS: Agent-oriented Theorem Proving
 
Recommended events (personal involvement): IWIL-2012, PAAR-2012, ICAART-2012 

Some Recent Publications (for a complete list and for downloads please see here; please obey existing copyrights)
 
* Higher-Order Aspects and Context in SUMO, Journal of Web Semantics, 2011.
* Quantified Conditional Logics are Fragments of HOL, NCMPL'11, 2011.
* Embedding and Automating Conditional Logics in Classical Higher-Order Logic. arXiv.org, 2011.
* Knowledge Engineering Tools. Chapter with A. Pease in book Ontology: A Practical Guide (by A. Pease), 2011
* Combining and Automating Classical and Non-Classical Logics in Classical Higher-Order Logic. Annals of Mathematics and AI, 2011.
* Sigma: An Integrated Development Environment for Formal Ontology. AI Communications, to appear.
* Quantified Multimodal Logics in Simple Type Theory. Logica Universalis, to appear.
* Adaptive Assertion Level Proofs. IJCAR 2010 Workshop EMS+QMS, 2010.
* Human-Oriented Proof Techniques are Relevant for Proof Tutoring. CICM 2010 Workshop MIPS, 2010.
* Verifying the Modal Logic Cube is an Easy Task (for HO Autom. Reasoners). Festschrift C. Walther, 2010.
* Reasoning with Embedded Formulas and Modalities in SUMO. ECAI 2010 Workshop ARCOE'10, 2010.
* Ontology Archaeology: Mining a Decade of Effort on the SUMO. ECAI 2010 Workshop ARCOE'10, 2010.
* Sigma: An Integr. Devel. 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. J. of Formalized Reason., 2010.
* Multimodal and Intuitionistic Logics in Simple Type Theory. Logic Journal of the IGPL, 2010.
* 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.
* Jacques Herbrand: Life, Logic, and Automated Deduction. 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 ... Teaching Mathematics and Computer Science. 2009.
* LEO-II - A Cooperative Automatic Theorem Prover for Higher-Order Logic. IJCAR'08.
 
Hobbies
 
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, 2012