Detailansicht
Automated deduction for intuitionistic logic via embedding into classical logic
Alexander Pluska
Art der Arbeit
Masterarbeit
Universität
Universität Wien
Fakultät
Fakultät für Mathematik
Studiumsbezeichnung bzw. Universitätlehrgang (ULG)
Masterstudium Mathematik
Betreuer*in
Matthias Aschenbrenner
DOI
10.25365/thesis.72249
URN
urn:nbn:at:at-ubw:1-18731.51693.682792-1
Link zu u:search
(Print-Exemplar eventuell in Bibliothek verfügbar)
Abstracts
Abstract
(Deutsch)
Die berühmte Double Negation Translation stellt eine Einbettung von klassischer in intuitionistische Logik dar. Interessanterweise ist die umgekehrte Richtung in der Literatur noch nicht behandelt worden. Wir präsentieren eine effektive Einbettung von intuitionistischer in klassische Logik, sowohl im Fall der Aussagenlogik als auch im Fall der Prädikatenlogik, sowie eine effektive Einbettung von intuitionistischer Aussagenlogik in quantifizierte boolesche Formeln. Darüber hinaus implementieren wir ein System, das intuitionistische Probleme der Prädikatenlogik im tptp-Dateiformat als Input nimmt und die Transformation durchführt. Dies ermöglicht die Verwendung von klassischen Beweissystemen zur Überprüfung intuitionistischer Gültigkeit. Wir testen unsere Implementierung mithilfe des Vampire-Beweissystems an der ILTP-Datenbank. Schließlich diskutieren wir, wie die generierten klassischen Beweise des transformierten Problems in intuitionistische Beweise des ursprünglichen Problems zurückübersetzt werden können. Insgesamt wird damit ein neuartiger Ansatz zum automatisiertem Theorembeweis für intuitionistische Logik etabliert und ein erster Proof of Concept erbracht.
Abstract
(Englisch)
The famous double negation translation establishes an embedding from classical into intuitionistic logic. Curiously, the reverse direction has not been covered in literature. We present an effective embedding from intuitionistic into classical logic, both in the propositional and first-order case, as well as an effective embedding of intuitionistic propositional logic into quantified boolean formulas. Furthermore, we implement a system that takes intuitionistic first-order problems in the tptp file format as an input and performs our transformation. This allows the use of classical theorem provers for checking intuitionistic validity. We benchmark our implementation using the Vampire theorem prover on the ILTP problem set. Finally, we discuss how the generated classical proofs of the transformed problem can be translated back into intuitionistic proofs of the original problem. All in all, this establishes a novel approach to theorem proving for intuitionistic logic and provides a first proof of concept.
Schlagwörter
Schlagwörter
(Deutsch)
Logik Intuitionistische Logik Konstruktive Mathematik Automatisierter Theorembeweis Beweistheorie
Schlagwörter
(Englisch)
Logic Intuitionistic logic Constructive mathematics Automated theorem proving Proof theory
Autor*innen
Alexander Pluska
Haupttitel (Englisch)
Automated deduction for intuitionistic logic via embedding into classical logic
Paralleltitel (Deutsch)
Automatisiertes Theorembeweisen für intuitionistische Logik durch Einbettung in klassische Logik
Publikationsjahr
2022
Umfangsangabe
56 Seiten : Diagramme
Sprache
Englisch
Beurteiler*in
Matthias Aschenbrenner
Klassifikationen
31 Mathematik > 31.10 Mathematische Logik, Mengenlehre ,
54 Informatik > 54.10 Theoretische Informatik
AC Nummer
AC16607839
Utheses ID
64411
Studienkennzahl
UA | 066 | 821 | |