Superposition modulo theory

Abstract

This thesis is about the Hierarchic Superposition calculus SUP(T) and its application to reasoning in hierarchic combinations FOL(T) of the free first-order logic FOL with a background theory T where the hierarchic calculus is refutationally complete or serves as a decision procedure. Particular hierarchic combinations covered in the thesis are the combinations of FOL and linear and non-linear arithmetic, LA and NLA resp. Recent progress in automated reasoning has greatly encouraged numerous applications in soft- and hardware verification and the analysis of complex systems. The applications typically require to determine the validity/unsatisfiability of quantified formulae over the combination of the free first-order logic with some background theories. The hierarchic superposition leverages both (i) the reasoning in FOL equational clauses with universally quantified variables, like the standard superposition does, and (ii) powerful reasoning techniques in such theories as, e.g., arithmetic, which are usually not (finitely) axiomatizable by FOL formulae, like modern SMT solvers do. The thesis significantly extends previous results on SUP(T), particularly: we introduce new substantially more effective sufficient completeness and hierarchic redundancy criteria turning SUP(T) to a complete or a decision procedure for various FOL(T) fragments; instantiate and refine SUP(T) to effectively support particular combinations of FOL with the LA and NLA theories enabling a fully automatic mechanism of reasoning about systems formalized in FOL(LA) or FOL(NLA).

Diese Arbeit befasst sich mit dem hierarchischen Superpositionskalkül SUP(T) und seiner Anwendung auf hierarchischen Kombinationen FOL(T) der freien Logik erste Stufe FOL und einer Hintergrundtheorie T, deren hierarchischer Kalkül widerlegungsvollständig ist oder als Entscheidungsverfahren dient. Die behandelten hierarchischen Kombinationen sind im Besonderen die Kombinationen von FOL und linearer und nichtlinearer Arithmetik, LA bzw. NLA. Die jüngsten Fortschritte in dem Bereich des automatisierten Beweisens haben zahlreiche Anwendungen in der Soft- und Hardwareverifikation und der Analyse komplexer Systeme hervorgebracht. Die Anwendungen erfordern typischerweise die Gültigkeit/Unerfüllbarkeit quantifizierter Formeln über Kombinationen der freien Logik erste Stufe mit Hintergrundtheorien zu bestimmen. Die hierarchische Superposition verbindet beides: (i) das Beweisen über FOL-Klauseln mit Gleichheit und allquantifizierten Variablen, wie in der Standardsuperposition, und (ii) mächtige Beweistechniken in Theorien, die üblicherweise nicht (endlich) axiomatisierbar durch FOL-Formeln sind (z. B. Arithmetik), wie in modernen SMT-Solvern. Diese Arbeit erweitert frühere Ergebnisse über SUP(T) signifikant, im Besonderen führen wir substantiell effektiverer Kriterien zur Bestimmung der hinreichenden Vollständigkeit und der hierarchischen Redundanz ein. Mit diesen Kriterien wird SUP(T) widerlegungsvollständig beziehungsweise ein Entscheidungsverfahren für verschiedene FOL(T)-Fragmente. Weiterhin instantiieren und verfeinern wir SUP(T), um effektiv die Kombinationen von FOL mit der LA- und der NLA-Theorie zu unterstützen, und erhalten eine vollautomatische Beweisprozedur auf Systemen, die in FOL(LA) oder FOL(NLA) formalisiert werden können.