Kooperatives höherstufiges automatisches Beweisen zum Schließen in Ontologien

• Applicant: Professor Dr.-Ing. Christoph Benzmüller
• Subject Area: Theoretical Computer Science
• Term: from 2009 to 2011
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 146209618

Ziel ist die Weiterentwicklung von kooperativem höherstufigen-erststufigen automatischen Beweisen zum Schließen in Ontologien. Eine Kooperation soll erfolgen mit Dr. Adam Pease (Articulate Software, USA). Dieser hat die ’Suggested Upper Merged Ontology (SUMO)’ Ontologie [28] entwickelt – die derzeit größte, frei verfügbare allgemeine Standard-Ontologie.1 SUMO, wie auch CYC [27, 32], enthält neben erststufigen Repräsentation auch signifikante Anteile an höherstufigen Kodierungen. In einer Vorarbeit an der Univ. Cambridge, UK habe ich den höherstufigen automatischen Beweiser LEO-II entwickelt [21, 17, 5, 16, 15, 40], der mit Beweisern erster Stufe kooperiert [20]. Im EU Projekt THFTPTP habe ich mit Prof. Geoff Sutcliffe (Univ. Miami) eine Infrastruktur für höherstufiges automatisches Beweisen aufgebaut [5, 35] – als Erweiterung der TPTP Infrastruktur für Logik erster Stufe [39]. Des weiteren habe ich mit meinem Doktoranden Frank Theiss, Geoff Sutcliffe und Adam Pease die Anbindung von SUMO an die TPTP Infrastruktur weiter vorangetrieben. Aufbauend auf diesen Vorarbeiten sollen (I) eine Anbindung von SUMO an LEO-II erreicht werden, (II) geeignete(re) höherstufige Repräsentationen für SUMO entwickelt werden und kooperatives höherstufiges-erststufiges Beweisen mit LEO-II auf diese angewendet werden, und (III) damit begonnen werden, LEO-II für diese Anwendung anzupassen.

• DFG Programme: Research Fellowships
• International Connection: USA
• Host: Adam Pease