<div class="csl-bib-body">
<div class="csl-entry">Lolić, A. (2020). <i>Automated proof analysis by CERES</i> [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2020.47184</div>
</div>
-
dc.identifier.uri
https://doi.org/10.34726/hss.2020.47184
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/1075
-
dc.description
Abweichender Titel nach Übersetzung der Verfasserin/des Verfassers
-
dc.description.abstract
Aus mathematischen Beweisen lässt sich explizite Information gewinnen, welche nicht im Theorem sichtbar ist. Um diese Art von Information aus Beweisen gewinnen zu können, arbeitet man mit Beweisen in Normalform, also analytischen Beweisen ohne Schnittregeln. In dieser Arbeit interessieren wir uns insbesondere für Herbrand Sequenzen. Herbrand Sequenzen sind propositional gültige Sequenzen, welche aus Instanzen des entsprechenden Theorems erstellt werden und realisieren dadurch den Satz von Herbrand im Sequenzenkalkül. Bisher wurden Herbrand Sequenzen aus Beweisen in Normalform mit einer effizienten Schnitteliminationsmethode, der Methode CERES, extrahiert. Wir zeigen, dass Beweise nicht unbedingt in Normalform sein müssen um Herbrand Sequenzen extrahieren zu können. Unsere Methode beruht auf speziellen Eigenschaften der CERES Methode für die Beweisanalyse. Da Herbrand Sequenzen nur aus Beweisen von pränexen Endsequenzen extrahiert werden können, verallgemeinern wir die Methode um Expansionsbeweise (eine Verallgemeinerung von Herbrand Sequenzen) zu gewinnen. Die entwickelten Methoden sind implementiert und an einigen Beispielbeweisen veranschaulicht. In einem letzten Schritt verallgemeinern wir unsere Methoden um auch mit Beweisen, welche Induktionsregeln beinhalten, arbeiten zu können. Wir wählen die Darstellung von Beweisen als Beweisschemata, welche die Erstellung von sogenannten Herbrand Systemen ermöglichen, und entwickeln eine schematische CERES Methode, welche mit komplizierteren Sätzen arbeiten kann als bestehende Methoden zur Beweisanalyse induktiver Beweise. Das Ziel dieser Forschung ist eine völlig automatisierte Analyse von interessanten mathematischen Beweisen, wie zum Beispiel von Fürstenbergs Beweis über die Unendlichkeit der Primzahlen. Obwohl eine völlig automatisierte Analyse dieses Beweises noch nicht erreicht werden konnte, stellt diese Arbeit einen wichtigen Schritt in der Entwicklung dar.
de
dc.description.abstract
Mathematical proofs can be used to extract explicit information about mathematical objects that is not visible in the theorem itself. In general, this kind of information can be extracted only from proofs in normal form, i.e. analytic proofs without cuts. In this work we are particularly interested in the extraction of Herbrand sequents from proofs. Herbrand sequents are propositionally valid sequents composed of instances of a corresponding theorem, thus they are a realization of Herbrands theorem in sequent calculus. So far, Herbrand sequents are extracted from proofs in normal form using the method CERES, which is a method specifically designed for efficient cut-elimination. In this work we show that for Herbrand sequent extraction proofs need not be in normal form. This novel method is based on specific features of the CERES method and simplifies and outperforms the current CERES method for proof analysis. Moreover, as the usual method for Herbrand sequent extraction only works for proofs of prenex end-sequents, we generalize our novel method to the extraction of expansion proofs (a generalization of Herbrand sequents in a non-prenex setting). The developed methods are implemented and we demonstrate some experiments with mathematical proofs. In a last step we lift our methods to the case with induction rules. We represent induction via schemata of proofs, as proof schemata allow the extraction of so-called Herbrand systems. We define a schematic CERES method that is capable of handling several induction parameters and thus allows to analyze more complicated proofs outside the range of previously defined methods. The overall goal is to develop a fully automated analysis of interesting mathematical proofs, as for instance Fürstenbergs proof of the infinitude of primes. Though a fully automated analysis of this proof is not yet within reach, this work can be seen as a major step in the development.
en
dc.language
English
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
Beweistheorie
de
dc.subject
Beweis-Schemata
de
dc.subject
Proof Theory
en
dc.subject
Cut-Elimination
en
dc.subject
Proof Schemata
en
dc.subject
Induction
en
dc.subject
Proof Mining
en
dc.subject
Herbrand's Theorem
en
dc.title
Automated proof analysis by CERES
en
dc.title.alternative
Automatische Beweisanalyse mit CERES
de
dc.type
Thesis
en
dc.type
Hochschulschrift
de
dc.rights.license
In Copyright
en
dc.rights.license
Urheberrechtsschutz
de
dc.identifier.doi
10.34726/hss.2020.47184
-
dc.contributor.affiliation
TU Wien, Österreich
-
dc.rights.holder
Anela Lolić
-
dc.publisher.place
Wien
-
tuw.version
vor
-
tuw.thesisinformation
Technische Universität Wien
-
dc.contributor.assistant
Baaz, Matthias
-
tuw.publication.orgunit
E192 - Institut für Logic and Computation
-
dc.type.qualificationlevel
Doctoral
-
dc.identifier.libraryid
AC15645004
-
dc.description.numberOfPages
176
-
dc.identifier.urn
urn:nbn:at:at-ubtuw:1-137929
-
dc.thesistype
Dissertation
de
dc.thesistype
Dissertation
en
tuw.author.orcid
0000-0002-4753-7302
-
dc.rights.identifier
In Copyright
en
dc.rights.identifier
Urheberrechtsschutz
de
tuw.advisor.staffStatus
staff
-
tuw.assistant.staffStatus
staff
-
item.openaccessfulltext
Open Access
-
item.openairecristype
http://purl.org/coar/resource_type/c_db06
-
item.grantfulltext
open
-
item.mimetype
application/pdf
-
item.languageiso639-1
en
-
item.openairetype
doctoral thesis
-
item.fulltext
with Fulltext
-
item.cerifentitytype
Publications
-
crisitem.author.dept
E192-02 - Forschungsbereich Databases and Artificial Intelligence