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

Applications of LEO-II in Ontology Reasoning are currently investigated in a project funded by a ''Forschungsstipendium'' of the German Research Foundation (DFG). This project is funded until 4/2011.

Knowledge-based projects such as SUMO [Niles & Pease, 2001] and Cyc [Matuszek &al., 2006] contain a significant fraction of higher-order constructs. Higher-order representations also play a role in the intermediate MultiNet representations of the German LogAnswer question answering system [Furbach &al., 2008]. In a collaboration with Articulate Software, Angwin, CA, USA, I am currently developing a bridge between the SUMO ontology and LEO-II within the Sigma system [Pease, 2003]. The idea is to exploit LEO-II for solving higher-order proof tasks in SUMO, e.g., tasks involving embedded formulas, epistemic modalities, and time. Another strong argument for adding higher-order ATP to this application area is its demand for natural and human-consumable problem and solution representations, which are hardly achievable after translating original higher-order content into less expressible frameworks such as first-order logic.

Project Report

We here provide a preliminary, regularly updated overview on project results. A detailed project report will follow at a later time. Currently C. Benzmüller is on parental leave. Nevertheless the project is progressing very well.

Awards

World Champion 2010: LEO-II is the winner of the THF division (automation of higher-order logic) at CASC-J5. Moreover, LEO-II did also participate in the CASC-J5 first-order division FOF and CNF and performed reasonably well. At present LEO-II is the only theorem prover available that supports THF, FOF and CNF syntax.

Publications (project related)

  • C. Benzmüller, Combining and Automating Classical and Non-Classical Logics in Classical Higher-Order Logics. Annals of Mathematics and Artificial Intelligence, to appear. [Download: bib,pdf]
  • 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]
  • A. Pease and C. Benzmüller, Sigma: An Integrated Development Environment for Formal Ontology. AI Communications, in revision. [Download: bib, pdf]
  • C. Benzmüller and L. C. Paulson, Quantified Multimodal Logics in Simple Type Theory. Logica Universalis, to appear. [Download: bib,pdf]
  • 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]
  • 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]
  • 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,ee]
  • 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]

Further Publications (supported by project)

  • 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]
  • M. Schiller and C. Benzmüller, Presenting Proofs with Adapted Granularity. KI 2009: Advances in Artificial Intelligence, 32nd Annual German Conference on AI, Paderborn, Germany, September 15-18, Proceedings, LNAI, vol. 5803, pp. 289-297, 2009. © Springer. ISBN 978-3-642-04616-2 [Download: bib,pdf]

Presentations

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