Algorithms for quantified cut-introduction

Abstract

Diese Arbeit beschäftigt sich mit einer Methode zur Einführung von Schnitten in Beweise des Sequential-Kalküls und bietet damit Möglichkeit zur Kompression der Beweise, dadurch eine eventuelle Verbesserung der Lesbarkeit und impliziert möglicherweise neue Einblicke in die Beweistheorie Das Problem der Schnitteinführung in schnittfreie Beweise des Sequential-Kalküls ist recht komplex, kann bereits durch verschiedene Methoden durchgeführt werden. Die, in dieser Arbeit beschriebene, Methode realisiert die Kompression mittels einiger aufeinanderfolgenden Schritte. Zuerst werden essentielle Teile des Beweises extrahiert, welche auch als Herbrand Sequent bezeichnet werden, und in eine Termsprache umgewandelt. Diese Sprache repräsentiert alle notwendigen Instanzen der quantifizierten Formeln. Es wird weiters versucht jene durch eine minimale Grammatik zu komprimieren. Das Problem eine minimale Grammatik für eine gegebene Sprache zu finden wird auf das MinCostSAT Problem reduziert und aus einer eventuell resultierenden Interpretation generiert. Diese Grammatik stellt das Fundament für die weitere Konstruktion eines erweiterten Herbrand Sequents dar, welches ein notwendiger Zwischenschritt ist um schlussendlich einen Beweis mit eingeführten Schnitten zu generieren. Auf Basis von [3] wurde ein Algorithmus zur Beweiskomprimierung konstruiert, welcher durch eine umfangreiche Serie an Experimenten getestet wurde. Obwohl die Effizienz bereits existierender Methoden zur Schnitteinführung in Beweise des Sequentialkalküls nicht übertroffen wurden, bietet diese neue Methode eine Erweiterung zu der bestehenden Funktionalität, durch die Möglichkeit mehr als einen einfach quantifizierten Schnitt auf einmal einzuführen. Während ein kleiner Schritt in der Richtung der Schnitteinführung gemacht werden konnte, welche in Zukunft darauf abzielen wird Schnitte mit immer komplexeren Schnittformeln einzuführen, könnte diese neue Methode ebenso neue Einblicke in die Beweistheorie geben.

The possibility of quantified cut-introduction, which this thesis is dedicated to, offers the possiblity of compressing a proof in sequent calculus, to improve readability and provide interesting new insights into proof theory. The problem of introducing quantified cuts into a cut-free proof in sequent calculus is a quite complex procedure, which can be accomplished in various ways. The method described in this thesis realised this by applying several consecutive steps. First essential parts of the proof are extracted, namely the Herbrand sequent, from which a term language is generated. This term language represents all needed instantiations of quantified formulas and will be tried to be compressed by a minimal grammar. The problem of finding a minimal grammar for this language is achieved by reducing it to the MinCostSAT problem and thus generate it via the resulting interpretation. This grammar forms the base for the further construction of an extended Herbrand sequent, which again illustrates an intermediate step to build a proof with cuts. On the basis of [3] an algorithm was constructed performing this minimal grammar computation, which was tested via a large series of experiments. Although previously developed methods, capable of cut-introduction, were not outperformed by this new method, the methods were extended by the possibility of introducing not just one single-quantified cut, but multiple single-quantified cuts at once. Possible new insights may be gained by this implemented method, where simultaneously a small step towards cut-introduction for cuts with more complex cut-formulas was made.