Effektives höherstufiges automatischen Theorembeweisen

• Antragsteller: Professor Dr.-Ing. Christoph Benzmüller
• Fachliche Zuordnung: Theoretische Informatik ; Bild- und Sprachverarbeitung, Computergraphik und Visualisierung, Human Computer Interaction, Ubiquitous und Wearable Computing
• Förderung: Förderung von 2014 bis 2018
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 241609402

LEO-I und LEO-II haben internationale Anerkennung erfahren als sehr erfolgreiche automatische Beweiser für klassische Logik höherer Stufe. In LEO-I wurde erstmals eine primitive Behandlung (im Gegensatz zur axiomatischen Behandlung) der Extensionalitätsprinzipien erreicht. Neu war auch die Kooperation mit externen Beweisern (wie z.B. dem erststufigen Beweiser E) in einer flexiblen, agentenbasierten Architektur. Die Implementierung von LEO-II hatte signifikanten Einfluss auf die parallele Entwicklung der neuen TPTP THF Infrastruktur für typisierte Logiken höherer Stufe. Diese Infrastruktur führte zu enormen Verbesserungen in höherstufigen Beweisern (z.B. in den automatischen Beweisern ISABELLE/HOL und TPS) und zu Neuentwicklungen im Gebiet (wie z. B. dem Beweiser Satallax). LEO-II gewann den internationalen CASC Beweiserwettbewerb in 2010 und wird zur Zeit in den interaktiven Beweisassistenten ISABELLE/HOL integriert.In diesem Projekt möchten wir LEO-II überführen in einen Beweiser, der auf geordneter Paramodulation/Superposition basiert.Diese Änderungen an LEO-II sind signifikant in Theorie und Praxis. Das resultierende System, bezeichnet als LEO-III, wird der Intergrierbarkeit mit anderen Systemen eine besondere Bedeutung beimessen.

• DFG-Verfahren: Sachbeihilfen