CERES in aussagenlogischen Beweisschemata 7 1 0 MASTERARBEIT 2 n a zur Erlangung des akademischen Grades J 8 1 Master of Science ] O im Rahmen des Studiums L . s c Computational Logic [ 1 eingereicht von v 1 5 Andrea Condoluci 2 5 Matrikelnummer 1528762 0 . 1 0 7 1 anderFakultätfürInformatik : v derTechnischenUniversitätWien i X r Betreuung:Univ.Prof.Dr.phil.AlexanderLeitsch a Wien,7.Oktober2016 AndreaCondoluci AlexanderLeitsch Technische Universität Wien A-1040 Wien Karlsplatz 13 Tel. +43-1-58801-0 www.tuwien.ac.at CERES in Propositional Proof Schemata MASTER’S THESIS submitted in partial fulfillment of the requirements for the degree of Master of Science in Computational Logic by Andrea Condoluci Registration Number 1528762 totheFacultyofInformatics attheTUWien Advisor:Univ.Prof. Dr.phil. AlexanderLeitsch Vienna,7th October,2016 AndreaCondoluci AlexanderLeitsch Technische Universität Wien A-1040 Wien Karlsplatz 13 Tel. +43-1-58801-0 www.tuwien.ac.at Erklärung zur Verfassung der Arbeit AndreaCondoluci Favoritenstraße9-11,1040Wien,Austria Hiermit erkläre ich, dass ich diese Arbeit selbständig verfasst habe, dass ich die verwen- deten Quellen und Hilfsmittel vollständig angegeben habe und dass ich die Stellen der Arbeit – einschließlich Tabellen, Karten und Abbildungen –, die anderen Werken oder dem Internet im Wortlaut oder dem Sinn nach entnommen sind, auf jeden Fall unter Angabe der Quelle als Entlehnung kenntlich gemacht habe. Wien,7.Oktober2016 AndreaCondoluci v Acknowledgements This thesis is the conclusion of my Master’s studies, therefore these acknowledgements apply not only to the hundred pages of the following scientific text, but also to the last seven hundred astounding days of my life. Firstly, my gratitude to Alex for the challenging and interesting topic, for always guiding me in the right direction, and for patiently proofreading the whole text – carefully spotting every single little inaccuracy. Thanks to my family for being a northern star, which I expect not to be as constant, but rather to shift with me across the constellations of life. My parents, my brother, my dog sister; my cousins, and all the relatives and friends which walk with me everyday in a gene or a gesture or a WhatsApp message. Last but not least, many thanks to Matteo and Nika. Thanks Matteo for taking care of me and feeding me, specifically feeding me the italianity which I longed for when away from home. And Nika, for making me question my beliefs, for growing up with me, for being the most breathtaking drug I’ve swallowed in my life. ∗∗∗ Per prima cosa, la mia gratitudine va ad Alex, per la sfida che mi ha fornito con il tema di questa tesi, per guidarmi sempre nella direzione giusta, e per leggere con pazienza questo testo parola per parola – indicandomi con cura ogni imprecisione. Grazie alla mia famiglia per essere una stella polare, che mi aspetto non altrettanto costante, ma che piuttosto scivoli con me attraverso le costellazioni della vita. I miei genitori, mio fratello, la mia sorella cane; le mie cugine, tutti i parenti e gli amici e le amiche che ogni giorno camminano con me in un gene o in gesto o in un messaggio WhatsApp. Ultimimanonperimportanza, graziemilleaMatteoeNika. GrazieMatteoperprendersi cura di me e darmi da mangiare, in particolare nutrirmi di quell’italianità di cui avevo fame quando lontano da casa. E a Nika, per mettere in discussione quello in cui credo, per crescere insieme a me, per essere la droga più mozzafiato che io abbia mandato giù nella mia vita. vii Kurzfassung Die Schnittelimination, eines der bekanntesten Probleme in der Beweistheorie, wurde für Sequenzenkalüle erster Ordnung von Gentzen in seinem gefeierten Hauptsatz definiert und gelöst. Ceres bezeichnet einen anderen Algorithmus zur Schnittelimination erster und höhe- rer Ordnung in der klassischen Logik. Er beruht auf der Idee einer charakteristischen Klauselmenge, die aus einem Beweis des Sequenzenkalküls extrahiert wurde und stets widerlegbar bleibt. Eine Resolutionswiderlegung dieser Klauselmenge dient als Gerüst für einen Beweis, der lediglich atomare Schnitte enthält. Das wird erreicht, indem die Klauseln der Resolutionswiderlegung durch die entsprechenden Beweisprojektionen des Originalbeweises ersetzt werden. Ceres wurde auf Beweisschemata ausgedehnt, die als Schablonen für gewöhnliche Beweise erster Ordnung dienen, die natürliche Zahlen als Parameter haben. Jede Instantiierung der Parameter durch konkrete Zahlen ergibt einen neuen Beweis erster Ordnung. Das Anwenden existierender Algorithmen der Schnittelimination auf jeden Beweis dieser unendlichen Sequenz würde zu einer ebenfalls unendlichen Folge von schnittfrei Beweisen führen. Das Ziel in der Logik erster Ordnung von Ceres ist es nun, stattdessen eine einheitliche, schematische Beschreibung dieser Sequenz schnittfrei Beweise zu liefern. Um dieses Ziel zu erreichen, wurde jedes Konzept in Ceres schematisch entworfen: es enthält Schemata der charakteristischen Klauselmenge, Schemata der Resolutionswiderlegung, Projektionsschemata etc. Während Ceres ein vollständiger Algorithmus zur Schnittelimination in der Logik erster Ordnung gilt, ist nicht klar, ob dies auch für die Schemata erster Ordnung zutrifft: liefert Ceres stets ein Schema schnittfreier Beweise, wenn ein Beweisschema mit Schnitten eingegeben wird? Die Schwierigkeit besteht darin, ein passendes Widerlegungsschema für das charakteristische Termschema eines Beweisschemas zu finden und darzustellen. In der vorliegenden Arbeit beschäftigen wir uns mit der Lösung dieses Problems, in- dem wir Ceres auf aussagenlogische Schemata einschränken, welche als Schablonen für aussagenlogische Beweise dienen. Durch die adäquate Beschränkung der Aussagekraft der aussagenlogischen Schemata und Beweisschemata wollen wir eine Version schemati- schen Ceres’ vorlegen, welche einen vollständigen Algorithmus der Schnittelimination für aussagenlogische Schemata liefert. Wir konzentrieren uns dabei auf einen bestimmten ix Schritt von Ceres: Schemata der Resolutionswiderlegung. Zuerst beweisen wir, dass durch das einfache Adaptieren von Ceres für Schemata erster Ordnung für unseren Fall der Algorithmus unvolständig ist. Danach modifizieren wir das Konzept des Schemas der Resolutionswiderlegung: um eine Klauselmenge zu widerlegen, bringen wir sie zuerst in eine allgemeine Form, um im Anschluss eine festgelegte Widerlegung dieser allgemeinen Klauselmenge zu benutzen. Unsere Variation von schematischem Ceres stellt den ersten Schritt in Richtung einer Vollständigkeit aussagenlogischer Schemata dar.