program verification; automated reasoning; Craig interpolation
de
Abstract:
In den letzten Jahren hat sich Propositionale Interpolation als einer der Hauptbestandteile der Modellprüfung etabliert. Aus diesem Grund wurde der Konstruktion von Interpolanten große Aufmerksamkeit gewidmet, wodurch eine Vielzahl an Algorithmen, welche Interpolanten aus Beweisen extrahieren, entstand. Einer dieser Ansätze beruht auf der Idee, Interpolanten aus lokalen Beweisen zu konstruieren. Der erste Beitrag dieser Masterarbeit besteht darin, dass wir einen neuen Interpolationsalgorithmus beschreiben, der Interpolanten aus lokalen Beweisen, die in beliebigen korrekten Beweissystemen in Prädikatenlogik formuliert sind, extrahiert. Der neue Algorithmus verbessert den Stand der Technik, indem er kleinere und strukturell einfachere Interpolanten als bestehende Algorithmen generiert und dabei einen intuitiveren Ansatz verwendet. Danach wenden wir uns der Interpolation in Propositionaler Logik zu: Als zweiten Beitrag beschreiben wir eine Beweistransformation, die einen propositionalen Resolutionsbeweis in einen derartigen lokalen Beweisen transformiert, dass wir auf triviale Weise einen Interpolanten extrahieren können. Weiters leiten wir aus der Transformation ein Interpolationssystem ab, das es ermöglicht, den Interpolanten effizient zu berechnen, indem durch Abstraktion die explizite Berechnung der Transformation vermieden wird.
de
Propositional interpolation has become the corner stone of many contemporary model checking algorithms. Consequently, the construction of interpolants has received ample of attention, resulting in a range of interpolation algorithms which derive interpolants from proofs. One such approch is to generate interpolants from proofs of a special form, i.e. from local proofs. As first contribution of this thesis, we give a new interpolation algorithm for local proofs in an arbitrary sound proof system in first-order logic, which improves the state of the art by generating smaller and simpler interpolants using an arguably more intuitive approach than existing algorithms. Afterwards we look at propositional interpolation: As second contribution, we state a proof transformation, which transforms an arbitrary propositional resolution into a special local proof, from which we can trivially extract an interpolant. Finally we derive an interpolation system as abstraction of the transformation, which enables us to efficiently compute the interpolant by avoiding to explicitly perform the proof transformation.