Vollautomatisches Beweisen in modaler Prädikatenlogik: Kalküle, Implementierungen und Problemsammlungen
Final Report Abstract
Beweisführung in modaler Prädikatenlogik hat vielfältige Anwendungen, wie zum Beispiel beim Planen, der Verarbeitung natürlicher Sprache, oder beim Entwurf und der Verifikation sicherheitskritischer Software. Bisher reichte die Effizienz automatischer Beweissysteme jedoch nicht aus, um eine hinreichende Computerunterstützung für derartige Anwendungen zu bieten. Ziel dieses Projektes war eine signifikante Steigerung der Effizienz von automatischen Beweissystemen für modale Prädikatenlogik. Hierzu wurden eine Reihe verschiedenartiger Beweiskalküle und automatischer Beweisverfahren entwickelt, implementiert, ausgetestet und optimiert. Der Beweiser MleanSeP auf der Basis analytischer Sequenzenkalküle generiert Beweise, die dem natürlichen logischen Schließen relativ nahe sind. - MleanTAP erweitert das klassische Tableauverfahren um sogenannte modale Präfixe und verwendet einen Präfixunifikationsalgorithmus, um die Suche nach Beweisen effizienter zu gestalten. - MleanCoP basiert auf einer modalen Erweiterung der Konnektionsmethode, die als kompakte Form des Tableauverfahrens angesehen werden kann und sehr effiziente Beweissuche ermöglicht. - f2p-MSPASS generiert mit Hilfe einer modalen Version des Hyperlinking-Verfahrens aussagenlogische Instanzen prädikatenlogischer Formeln, die dann mit einem Beweiser für modale Aussagenlogik auf Gültigkeit überprüft werden. - Die Beweiser M-Satallax und M-Leo-II transformieren modallogische Formeln in eine getypte Logik höherer Stufe und wenden darauf dann Beweisverfahren für diese Logik an. Mit den im Projekt entwickelten Beweisern können insgesamt die Modallogiken K, K4, K5, B, D, D4, T, S4 und S5 mit konstanten, kumulativen und variierenden Domänen und einige Multimodallogiken effizient verarbeitet werden. Die Beweiser M-Satallax und M-Leo-II decken dabei alle dieser Logiken ab, andere bisher nur die Kernlogiken D, D4, T, S4 und S5. Alle Beweiser arbeiten dabei um mindestens 10 Größenordnungen effizienter als der schnellste zu Projektbeginn verfügbare Beweiser (GQML-Prover). Unser leistungsstarkster Beweiser, MleanCoP, erreicht sogar eine eine Effizienzsteigerung um mehr als 50 Größenordnungen und ist damit zur Zeit der mit Abstand schnellste Beweiser für modale Prädikatenlogik. Mit den in diesem Projekt entwickelten und implementierten Systemen stehen nun erstmalig Beweiswerkzeuge zur Verfügung, die effizient genug sind für einen Einsatz in praktischen Anwendungen modaler Prädikatenlogiken. Um einen Vergleich verschiedener Beweissysteme zu ermöglichen und die Effizienz neuer Techniken zu messen, wurde außerdem eine umfangreiche, standardisierte Sammlung von Problemen für modale Prädikatenlogik sowie eine Testumgebung für Beweisverfahren entwickelt und im Internet öffentlich zuganglich gemacht. Diese QMLTP-Problemsammlung hat sich für das Entwickeln und Testen von Beweisverfahren als unerlässlich herausgestellt und trägt wesentlich zum Fortschritt auf dem Gebiet des automatischen Beweisens in modaler Prädikatenlogik bei.
Publications
- Restricting Backtracking in Connection Calculi. AI Communications 23(2–3):159-182, 2010
Jens Otten
- A Non-clausal Connection Calculus. International Conference TABLEAUX 2011, LNAI 6793, S. 226-241. Springer Verlag, 2011
Jens Otten
- Implementing and Evaluating Provers for First-Order Modal Logics. L. De Raedt et al., eds., ECAI 2012, pages 163–168. IOS Press, 2012
C. Benzmüller, T. Raths, J. Otten
- Implementing Connection Calculi for First-order Modal Logics. In E. Ternovska, K. Korovin, S. Schulz, editors, 9th International Workshop on the Implementation of Logics (IWIL- 2012), 2012
Jens Otten
- The QMLTP Problem Library for First-order Modal Logics. IJCAR 2012, LNCS 7364, pages 454-461. Springer, 2012
T. Raths, J. Otten
- Implementing Different Proof Calculi for First-Order Modal Logics. In P. Fontaine, R. Schmidt, S. Schulz, editors, Third Workshop on Practical Aspects of Automated Reasoning, PAAR 2012, CEUR Workshop Proceedings, 2013
C. Benzmüller, J. Otten, T. Raths
