Kooperatives höherstufiges automatisches Beweisen zum Schließen in Ontologien
Zusammenfassung der Projektergebnisse
Das Projekt ONTOLEO untersuchte Techniken zum Schließen in expressiven Ontologien. Konkret betrachtet wurde die SUMO Ontologie (http://ontologyportal.org), welche mit der ebenfalls sehr bekannten CYC Ontologie (http://www.cyc.com) verwandt ist. SUMO unsterstützt einerseits die Modellierung einfacher Taxonomien (man denke hierbei an die Sprache OWL-DL und an Semantic Web Anwendungen). Andererseits stellt SUMO zusätzliche Sprachmittel bereit, um die auf Taxonomie-Ebene eingeführten Konzepte konkreter und präziser zu beschreiben. Diese zusätzlichen Sprachmittel umfassen auch Konzepte aus der Logik höherer Stufe, und deshalb stellt das Automatische Schließen für die SUMO Ontologie eine besondere Herausforderung dar. Unter Verwendung von automatischen Beweisern für die Logik erster Stufe wurden in der Vergangenheit zwar leistungsfähige Techniken zum Schließen in SUMO entwickelt, unglücklicherweise decken diese wichtige Konstrukte in SUMO aber nur unzureichend ab. Beispiele sind eingebettete Formeln, Lambda-Abstraktionen, sowie Funktions- und Prädikatsvariablen. Dieser Problematik stellte sich das Projekt ONTOLEO indem es (als Ergänzung zu bestehenden Techniken) Lösungen basierend auf dem automatischen Beweisen in Logik höherer Stufe erarbeitete und den Beweiser LEO-II (http://leoprover.org) für diese Anwendung zielgerichtet verbesserte. Eng kooperiert hat ONTOLEO dabei mit der TPTP THF Initiative, die in den zurückliegenden Jahren durch den Aufbau einer internationalen Infrastruktur für das höherstufige automatische Beweisen wichtige praktische und theoretische Fortschritte auf diesem Gebiet gefordert hat. Die Verbesserungen an LEO-II führten in 2010 zum Gewinn der TPTP CASC Weltmeisterschaften in der THF Kategorie. Eine im Projekt unerwartet aufgetretene, theoretische wie praktisch anspruchsvolle Herausforderung, konnte erfolgreich gemeistert werden: Durch die frische Herangehensweise war die Kontraintuitivität der bisherigen Annahme einer reinen klassischen Semantik für SUMO nachgewiesen worden. Dies stellte wiederum den uniformen Einsatz des klassischen höherstufigen Beweisers LEO-II im Projekt in Frage. Als Ausweg wurde in ONTOLEO ein Ansatz zur flexiblen Kombination von klassischen und nichtklassischen Logiken entwickelt. Dieser Ansatz basiert auf einer expliziten Modellierung von Kripke Strukturen in klassischer Logik höherer Stufe. Er ermöglicht den uniformen Einsatz von klassischen, höherstufigen Beweisern wie LEO-II für das Schließen mit klassischen und nichtklassischen Anteilen in SUMO. Diese Forschung adressiert die anspruchsvollen Themenkomplexe ’Kontextmodellierung’ und ’(flexible) Kombinationen von Logiken’ und ist damit weit über den Rahmen von ONTOLEO hinaus von Bedeutung. LEO-II wurde durch diese Arbeiten zu einem universellen automatischen Beweiser für flexible Logikkombinationen. Trotz erschwerter Rahmenbedingungen (Schließung der International University in Germany) wurden im Projekt insgesamt signifikante Fortschritte erzielt.
Projektbezogene Publikationen (Auswahl)
- Combining and automating classical and non-classical logics in classical higher-order logics. Annals of Mathematics and Artificial Intelligence (CLIMA XI Special Issue)
C. Benzmüller
(Siehe online unter https://dx.doi.org/10.1007/s10472-011-9249-7) - Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure. Journal of Formalized Reasoning, (2010) 3(1):1-27. ISSN 1972-5787
G. Sutcliffe and C. Benzmüller
- Progress in Automating Higher-Order Ontology Reasoning. The IJCAR’10 Workshop on Practical Aspects of Automated Reasoning (PAAR’08), Edinburgh, UK, 2010
C. Benzmüller, 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
C. Benzmüller and A. Pease
