<div class="csl-bib-body">
<div class="csl-entry">Ebner, G. (2021). <i>Inductive theorem proving based on tree grammars</i> [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2021.55608</div>
</div>
-
dc.identifier.uri
https://doi.org/10.34726/hss.2021.55608
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/16832
-
dc.description
Abweichender Titel nach Übersetzung der Verfasserin/des Verfassers
-
dc.description.abstract
One novel approach to understand cut-elimination based on formal languages was introduced by Hetzl, introducing a connection between a class of proofs where cut formulas are restricted to purely universally or existentially quantified prenex formulas and totally rigid regular tree grammars. In this approach there is a function that assigns to every proof a grammar such that the language generated by the grammar corresponds to a Herbrand disjunction, which essentially contains the quantifier inferences in the cut-free proof. This correspondence has been extended to a class of proofs with induction by Eberhard and Hetzl.Understanding induction- and cut-elimination on the level of grammars allows us to reverse this process, and produce proofs with induction from cut-free proofs. The cut-free proofs can for example be produced by automated theorem provers, resulting in an automated inductive theorem prover. The approach proceeds in two steps, first generating a grammar that covers the Herbrand disjunctions of the cut-free proofs,and then solving a formula equation induced by the grammar.This thesis builds a practical implementation of this approach to automated inductive theorem proving. First we investigate the complexity of a number of decision problems on classes of tree grammars corresponding to proofs. These complexity results directly transfer to proof-theoretic complexity results about Herbrand disjunctions aftercut-elimination. We also study three concrete algorithms to find covering grammars and evaluate implementations of them.Two algorithms to solve formula equations are presented. A new undecidability result on formula equations induced by grammars for proofs with induction illustrates the inherent complexity of the problem.Practically, Herbrand disjunctions are obtained by extracting them from proofs by automated theorem provers, which use efficient superpositioncalculi. A new algorithm that directly converts such proofs to expansion proofs, a generalization of Herbrand disjunctions, is introduced and benchmarked.Finally, these puzzle pieces are combined in a practical implementation,which is evaluated on real-world benchmarks. The results of this evaluation uncover an interesting difference between automatically generated proofs and proofs generated by induction elimination. A detailed case study illustrates this fundamental difference.
en
dc.language
English
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
Beweistheorie
de
dc.subject
Automatisches Beweisen
de
dc.subject
Induktion
de
dc.subject
Baumgrammatiken
de
dc.subject
proof theory
en
dc.subject
automated deduction
en
dc.subject
induction
en
dc.subject
tree grammars
en
dc.title
Inductive theorem proving based on tree grammars
en
dc.title.alternative
Induktives Beweisen mit Baumgrammatiken
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.2021.55608
-
dc.contributor.affiliation
TU Wien, Österreich
-
dc.rights.holder
Gabriel Ebner
-
dc.publisher.place
Wien
-
tuw.version
vor
-
tuw.thesisinformation
Technische Universität Wien
-
tuw.publication.orgunit
E104 - Institut für Diskrete Mathematik und Geometrie
-
dc.type.qualificationlevel
Doctoral
-
dc.identifier.libraryid
AC16140047
-
dc.description.numberOfPages
256
-
dc.thesistype
Dissertation
de
dc.thesistype
Dissertation
en
dc.rights.identifier
In Copyright
en
dc.rights.identifier
Urheberrechtsschutz
de
tuw.advisor.staffStatus
staff
-
tuw.advisor.orcid
0000-0002-6461-5982
-
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
E104-02 - Forschungsbereich Computational Logic
-
crisitem.author.parentorg
E104 - Institut für Diskrete Mathematik und Geometrie