Superposition and decision procedures back and forth

Abstract

Two apparently different approaches to automating deduction are mentioned in the title; they are the subject of a debate on "big engines vs. little engines of proof';. The contributions in this thesis advocate that these two strands of research can interplay in subtle and sometimes unexpected ways, such that mutual pervasion can lead to intriguing results: Firstly, superposition can be run on top of decision procedures. This we demonstrate for the class of Shostak theories, incorporating a little engine into a big one. As another instance of decision procedures within superposition, we show that ground confluent rewrite systems, which decide entailment problems in equational logic, can be harnessed for detecting redundancies in superposition derivations. Secondly, superposition can be employed as proof-theoretic means underneath combined decision procedures: We re-establish the correctness of the Nelson-Oppen procedure as an instance of the completeness of superposition. Thirdly, superposition can be used as a decision procedure for many interesting theories, turning a big engine into a little one. For the theory of bits and of fixed-size bitvectors, we suggest a rephrased axiomatization combined with a transformation of conjectures, based on which superposition decides the universal fragment. Furthermore, with a modification of lifting, we adapt superposition to the theory of bounded domains and give a decision procedure, which captures the Bernays-Schönfinkel class as well.

Zwei augenscheinlich verschiedene Ansätze zum Automatisieren der Deduktion werden im Titel angeführt. Die Beiträge in dieser Dissertation zeigen auf, daß diese zwei Ansätze in subtiler und manchmal unerwarteter Weise im Wechselspiel stehen, so daß wechselseitige Durchdringung zu verblüffenden Ergebnissen führen kann: Erstens kann Superposition modulo Entscheidungsverfahren betrieben werden; wir zeigen dies für die Klasse der Shostak-Theorien. Als ein weiteres Beispiel von Entscheidungsverfahren innerhalb von Superposition zeigen wir, daß in Superpositionsableitungen mit grundkonfluenten Reduktionssysteme, die bekanntlich das gleichungslogische Wortproblem entscheiden, Redundanzen erkannt werden können. Zweitens kann man mit Superposition als beweistheoretischem Werkzeug die Kombination von Entscheidungsverfahren fundieren: Wir rekonstruieren die Korrektheit des Nelson-Oppen-Verfahrens aus der Vollständigkeit der Superposition. Drittens kann Superposition verwendet werden als Entscheidungsverfahren für viele wichtige Theorien. Für die Theorie der Bits und der Bitvektoren fester Länge stellen wir eine umformulierte Axiomatisierung zusammen mit einer Transformation von Konjekturen vor, so daß sich mit Superposition das universelle Fragment entscheiden l¨aßt. Weiterhin passen wir Superposition mittels eines geänderten Liftings an die Theorie beschränkter Domänen an und geben ein Entscheidungsverfahren an; dieses entscheidet auch die Bernays-Schönfinkel-Klasse.