The DFG Project BE 2501/6-1 and BE 2501/8-1 (ONTOLEO)

Applications of LEO-II in Ontology Reasoning were investigated in a project funded by a ''Forschungsstipendium'' of the German Research Foundation (DFG).

The ONTOLEO project developed a bridge between the SUMO ontology and the LEO-II higher-order automated theorem prover. Moreover, LEO-II was significantly improved during the project and adapted for the task. Due to these improvements LEO-II did win the CASC-J5 world championships in the TPTP THF category in 2010. The project ONTOLEO also fostered the further developement of the TPTP THF infrastructure for higher-order automated theorem proving in various ways. Another contribution of ONTOLEO is an approach for combining classical and non-classical classical higher-order logics. This work has been used in the project for the automation of combinations of modal contexts in SUMO with LEO-II.

Principal Investigator

Christoph Benzmüller

Project Duration

07/2009--04/2011 BE 2501/6-1 (includes a 12 months parental leave)
07/2009--04/2011 BE 2501/8-1

Collaborators and Friends (that supported the project)

Adam Pease, Geoff Sutcliffe, Frank Theiss, Larry Paulson, Nik Sultana, Nick Siegel, Stephan Schulz, Valerio Genovese, Dov Gabbay, Chad Brown, Jasmin Blanchette, Jens Otten, Florian Rabe, Carsten Schürmann, Till Mossakowski

Publications

Books/Chapter in Books

  • A. Pease and C. Benzmüller, Knowledge Engineering Tools. Chapter in A. Pease, Ontology: A Practical Guide, 2010. Articulate Software Press, Angwin, CA, USA. [Download: bib,link]
  • C. Benzmüller, Verifying the Modal Logic Cube is an Easy Task (for Higher-Order Automated Reasoners). Festschrift in honor of Prof. Christoph Walther's 60's Birthday, LNCS vol. 6463, pp. 117-128, 2010. © Springer. [Download: bib,pdf]

Journals

  • C. Benzmüller and A. Pease, Higher-Order Aspects and Context in SUMO. Web Semantics: Science, Services and Agents on the World Wide Web (Special issue on Reasoning with context in the Semantic Web), (2012) 12-13:104-117. ISSN 1570-8268 © Elsevier [Download: bib,pdf,doi: 10.1016/j.websem.2011.11.008]
  • C. Benzmüller, Combining and Automating Classical and Non-Classical Logics in Classical Higher-Order Logics. Annals of Mathematics and Artificial Intelligence (Special issue Computational logics in Multi-agent Systems (CLIMA XI)), (2011) 62(1-2):103-128. ISSN 1012-2443 © Springer. [Download: bib,pdf,doi: 10.1007/s10472-011-9249-7]
  • A. Pease and C. Benzmüller, Sigma: An Integrated Development Environment for Formal Ontology. AI Communications (Special Issue on Intelligent Engineering Techniques for Knowledge Bases), in print. [Download: bib, pdf]
  • C. Benzmüller and L. C. Paulson, Quantified Multimodal Logics in Simple Type Theory. Logica Universalis, 2012. [Download: bib, pdf, doi: 10.1007/s11787-012-0052-y]
  • G. Sutcliffe and C. Benzmüller, Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure. Journal of Formalized Reasoning, (2010) 3(1):1-27. ISSN 1972-5787. [Download: bib,pdf, ee]
  • C. Benzmüller and L. C. Paulson, Multimodal and Intuitionistic Logics in Simple Type Theory. The Logic Journal of the IGPL. © Oxford University Press, (2010) 18(6): 881-892. ISSN 1367-0751. [Download: bib, pdf, doi: 10.1093/jigpal/jzp080]

Conferences and Workshops

  • C. Benzmüller and V. Genovese Quantified Conditional Logics are Fragments of HOL. The International Conference on Non-classical Modal and Predicate Logics (NCMPL), Guangzhou (Canton), China, 2011.[Download: bib,pdf]
  • C. Benzmüller, Combining Logics in Simple Type Theory. The 11th International Workshop on Computational Logic in Multi-Agent Systems (CLIMA XI), Lisbon, Portugal, August 16-17, 2010.[Download: bib,pdf]
  • C. Benzmüller and A. Pease, Reasoning with Embedded Formulas and Modalities in SUMO. The ECAI-10 Workshop on Automated Reasoning about Context and Ontology Evolution (ARCOE-10), Lisbon, Portugal, August 16-17, 2010. [Download: bib,pdf]
  • C. Benzmüller and A. Pease, Progress in Automating Higher-Order Ontology Reasoning. IJCAR'10 Workshop on Practical Aspects of Automated Reasoning (PAAR-2008), Edinburgh, UK, 2010. [Download: bib,pdf]
  • A. Pease and C. Benzmüller, Ontology Archaeology: Mining a Decade of Effort on the Suggested Upper Merged Ontology. The ECAI-10 Workshop on Automated Reasoning about Context and Ontology Evolution (ARCOE-10), Lisbon, Portugal, August 16-17, 2010. [Download: bib,pdf]
  • A. Pease and C. Benzmüller, Sigma: An Integrated Development Environment for Logical Theory Development. The ECAI 2010 Workshop on Intelligent Engineering Techniques for Knowledge Bases (IKBET'2010), Lisbon, Portugal, August 16-17, 2010. [Download: bib,pdf]
  • C. Benzmüller, Simple Type Theory as Framework for Combining Logics. World Congress and School on Universal Logic III (UNILOG'2010). UNILOG'2010 contest paper, Lisbon, Portugal, April 18-25, 2010. http://arxiv.org/abs/1004.5500 [Download: bib,pdf]

Conferences and Workshops (supported by project but not directly related)

  • M. Schiller and C. Benzmüller, Adaptive Assertion Level Proofs. The Workshop on Evaluation Methods for Solvers and Quality Metrics for Solutions (EMS+QMS-2010, affiliated with IJCAR 2010 and CAV 2010), Edinburgh, UK, July 20, 2010. [Download: bib,pdf]
  • M. Schiller and C. Benzmüller, Human-Oriented Proof Techniques are Relevant for Proof Tutoring. Workshop on Mathematically Intelligent Proof Search (MIPS 2010, affiliated with CICM 2010), Paris, France, July 10, 2010. [Download: bib,pdf]

Reports and Others

  • C. Benzmüller, A Note on LEO-II and the Basic Fragment of Simple Type Theory. AAR Newsletter No. 84, July 2009. [Download: bib, link]

Presentations

  • (invited) Automating Expressive Non-classical Logics and their Combinations in Classical Higher Order Logic, University of Potsdam, November 15, 2011.
  • (invited) Three presentations at Dagstuhl Seminar 10412 QSTRLib: A Benchmark Problem Repository for Qualitative Spatial and Temporal Reasoning, Dagstuhl, Germany, October 10-13, 2010: Reasoning within and about Combinations of Logics in Simple Type Theory (talk and system demonstration), Participant Introduction, and QSTRLib Use Case: Educational Question Answering on Spatial Configurations of Countries, States, and Cities.
  • Sigma: An Integrated Development Environment for Logical Theory Development, The ECAI 2010 Workshop on Intelligent Engineering Techniques for Knowledge Bases (IKBET'2010), Lisbon, Portugal, August, 17th, 2010.
  • Reasoning with Embedded Formulas and Modalities in SUMO, The ECAI-10 Workshop on Automated Reasoning about Context and Ontology Evolution (ARCOE-10), Lisbon, Portugal, August, 17th, 2010.
  • Ontology Archeology: Mining a Decade of Effort on the Suggested Upper Ontology, The ECAI-10 Workshop on Automated Reasoning about Context and Ontology Evolution (ARCOE-10), Lisbon, Portugal, August, 16th, 2010.
  • Combining Logics in Simple Type Theory, 11th International Workshop on Computational Logic in Multi-Agent Systems (CLIMA XI), Lisbon, Portugal, August, 16th, 2010.
  • Adaptive Assertion-Level Proofs, The IJCAR 2010 Workshop on Evaluation Methods for Solvers and Quality Metrics for Solutions, Edinburgh, UK, July 20, 2010.
  • Winner Presentation: LEO-II – A Cooperative Higher-Order–First-Order ATP, CASC-J5, Fifth International Joint Conference on Automated Reasoning (IJCAR'10), Edinburgh, UK, July, 19th, 2010. [Download: pdf]
  • Progress in Automating Higher-Order Ontology Reasoning, Workshop on Practical Aspects of Automated Reasoning (PAAR-2010), Edinburgh, UK, August 14th, 2010. [Download: pdf]
  • (invited) Combining Logics in Simple Type Theory (and an Application in Ontology Reasoning). SRI International, Menlo Park, USA, Juli 1, 2010. [Download: pdf]
  • Simple Type Theory as Framework for Combining Logics. World Congress and School on Universal Logic III (UNILOG'2010). Contest presentation, Lisbon, Portugal, April 23, 2010. [Download: pdf]

Tools, Software, Formalized Knowledge, etc.

  • Parser for TPTP THF, FOF and CNF. LEO-II is the first theorem prover that supports higher-order TPTP syntax (THF) and first-oder TPTP syntax (FOF,CNF) simultaneously.
  • Translator from SUO-KIF to TPTP THF0. This translator has been implemented in JAVA as part of the open source SIGMA-KEE ontology engineering environment. SIGMA-KEE is available at http://sigmakee.sourceforge.net/
  • 1st THF0 translation of SUMO. This translation can be processed by all THF0 compliant provers including IsabelleP, TPS, Satallax, and our own LEO-II. The translation is available here.
  • Improved versions of the LEO-II prover. The latest versions of our LEO-II prover are available here.
  • Problems for the TPTP THF Library. The project contributed a significant number of example problems to the TPTP library.