Cuts without quantifier alternations and their effect on expansion trees

Abstract

Das Ziel dieser Arbeit ist es, aus einem Beweis eines Sequents eine Herbrand-Menge zu extrahieren, also eine tautologische Menge von Instanzen dieses Sequents. Zunächst befassen wir uns mit Gentzens Sequentialkalkül und dem Schnitteliminations-Algorithmus. Danach entwickeln wir die Theorie der Expansionsbäume, -sequente und -beweise im Rahmen der Logik erster Stufe und zeigen, dass aus einem Sequentialbeweis, der nur einfache Schnitte enthält, ein Expansionsbeweis gewonnen werden kann. Dieser Expansionsbeweis kann dann wiederum in eine Herbrand-Menge umgewandelt werden. Im dritten Kapitel definieren wir eine neue Art von Baumgrammatik, die sogenannten constrained grammars, und zeigen dass wir damit total rigide Grammatiken emulieren und gleichzeitig weitere Beschränkungen erzwingen können. Zu guter Letzt werden die vorhergenden Ergebnisse kombiniert, um zu zeigen, dass wir aus einem Sequentialbeweis eine constrained grammar gewinnen können, deren Sprache eine tautologische Menge von Instanzen ist. Zum Beweis verwenden wir, dass 1) die Sprache durch Schnittreduktion nie größer wird und 2) für (beinahe) schnittfreie Beweise die Sprache genau der Herbrand-Menge entspricht, die wir aus einem Expansionsbeweis bekämen. Damit ergibt sich insgesamt, dass wir mittels constrained grammars eine Herbrand-Menge aus einem Beweis berechnen können, ohne tatsächlich Schnittelimination durchführen zu müssen.

The aim of this thesis is to extract an Herbrand set, that is a tautological set of instances of a sequent, from a proof of that sequent that may contain cuts. We first present the basics of Gentzen's sequent calculus and the cut reduction algorithm. Next we develop the theory of expansion trees, sequents and proofs in a first-order setting and show that we can extract an expansion proof from a sequent proof that contains only certain simple kinds of cuts. Such an expansion proof can in turn be converted into a Herbrand set. In the third chapter, we invent a new type of tree grammar, the so-called constrained grammars, and show that they can emulate totally rigid tree grammars while also enforcing additional restrictions. Finally, the previous efforts are combined to show that from a sequent proof we can extract a constrained whose language is a tautological set of instances. We show this by establishing 1) that the language of the grammar does not expand under cut reduction and 2) for (nearly) cut-free proofs the language corresponds to the Herbrand set we would extract via the expansion proof method. It follows that using constrained grammars, we can compute an Herbrand set from a proof without performing cut elimination.