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

• Antragsteller: Professor Dr.-Ing. Christoph Benzmüller
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2009 bis 2011
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 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-Verfahren: Forschungsstipendien
• Internationaler Bezug: USA
• Gastgeber: Adam Pease