An approximation and refinement approach to first-order automated reasoning

Abstract

With the goal of lifting model-based guidance from the propositional setting to first order logic, I have developed an approximation theorem proving approach based on counterexample-guided abstraction refinement. A given clause set is transformed into a simplified form where satisfiability is decidable. This approximation extends the signature and preserves unsatisfiability: if the simplified clause set is satisfiable, so is the original clause set. A resolution refutation generated by a decision procedure on the simplified clause set can then either be lifted to a refutation in the original clause set, or it guides a refinement excluding the previously found unliftable refutation. This way the approach is refutationally complete. The monadic shallow linear Horn fragment, which is the initial target of the approximation, is well-known to be decidable. It was a long standing open problem how to extend the fragment to the non-Horn case, preserving decidability, that would, e.g., enable to express non-determinism in protocols. I have now proven decidability of the non-Horn monadic shallow linear fragment via ordered resolution. I further extend the clause language with a new type of constraints, called straight dismatching constraints. The extended clause language is motivated by an improved refinement of the approximation-refinement framework. All needed operations on straight dismatching constraints take linear or linear logarithmic time in the size of the constraint. Ordered resolution with straight dismatching constraints is sound and complete and the monadic shallow linear fragment with straight dismatching constraints is decidable. I have implemented my approach based on the SPASS theorem prover. On certain satisfiable problems, the implementation shows the ability to beat established provers such as SPASS, iProver, and Vampire.

Mit dem Ziel die Modell-basierten Methoden der Aussagenlogik auf die Logik erster Stufe anzuwenden habe ich ein approximations Beweis-System entwickelt, das auf der Idee der ’Gegenbeispiel-gelenkten Abstraktions-Verfeinerung’ beruht. Eine gegebene Klausel-Menge wird zunächst in eine vereinfachte Form übersetzt, in der die Erfüllbarkeit entscheidbar ist. Diese sogenannte Approximation erweitert die Signatur, aber erhält Unerfüllbarkeit: Falls die approximierte Klauseln erfüllbar sind, so ist es auch die ursprüngliche Menge. Ein Resolutions-Beweis, der von einer Entscheidungs-Prozedur auf der Approximation erzeugt wurde, kann dann entweder als Basis eines Unerfüllbarkeits Beweises der ursprünglichen Menge dienen oder aber eine Verfeinerung der Approximation aufzeigen, welche den gefundenen Beweis davon ausschließt noch einmal gefunden zu werden. Damit ist der Ansatz widerlegungs vollständig. Das monadisch flache lineare Horn Fragment, das als anfängliches Ziel der Approximation dient, ist bereits seit längerem als entscheidbar bekannt. Es war ein lange offenes Problem, wie man das Fragment auf den nicht-Horn Fall erweitern kann ohne Entscheidbarkeit zu verlieren. Damit lassen sich unter anderem nicht-deterministische Protokolle ausdrücken. Ich habe nun die Entscheidbarkeit des nicht-Horn monadisch flachen linearen Fragments mittels geordneter Resolution bewiesen. Zusätzlich habe ich die Klausel-Sprache durch eine neue Art von Constraints erweitert, die ich als ’straight dismatching constraints’ bezeichne. Diese Erweiterung ist dadurch motiviert dass sie eine Verbesserung der Approximations-Verfeinerung des vorgestellten Systems erlaubt. Alle benötigten Operationen auf diesen Constraints nehmen lediglich lineare oder linear-logarithmische Zeit und Platz in Anspruch. Ich zeige, dass geordnete Resolution mit Constraints korrekt und vollständig ist und dass das monadische flache lineare Fragment mit Constraints entscheidbar ist. Ich habe meinen Ansatz auf dem Theorem-Beweiser SPASS basierend implementiert. Auf bestimmten erfüllbaren Problem schlägt meine Implementierung sogar etablierte Beweiser wie SPASS, iProver und Vampire.