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

Ziel ist die Weiterentwicklung von koooperativem höherstufigen-erststufigen automatischen Beweisen zum Schließen in Ontologien. Adam Pease博士（Articulate Software，美国）进行的一次合作。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 eststufigen Repräsentation auch signifikante Anteile an höherstufigen Kodierungen.在英国剑桥大学的一个实验室里，我已经完成了LEO-II自动化装置的研制[21，17，5，16，15，40]，该装置具有先进的工作原理[20]。在欧盟THFTPTP项目中，我与Geoff Sutcliffe教授（迈阿密大学）合作，设计了一个用于自动化的硬件结构[5，35] --用于逻辑的TPTP硬件结构[39]。我和我的博士弗兰克·泰斯、杰夫·萨特克利夫和亚当·皮斯一起为SUMO和TPTP的结构做了进一步的研究。因此，必须解决以下问题：（1）将SUMO与LEO-II的结合引入韦尔登中;（2）将SUMO引入韦尔登中，并与LEO-II的合作伙伴进行合作;（3）将LEO-II引入韦尔登中;（4）将LEO-II引入韦尔登中，使LEO-II用于卫星定位。

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.