Title: Inductive theorem proving based on tree grammars
Other Titles: Induktives Beweisen mit Baumgrammatiken
Language: English
Authors: Ebner, Gabriel 
Qualification level: Doctoral
Advisor: Hetzl, Stefan 
Issue Date: 2021
Number of Pages: 256
Qualification level: Doctoral
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.
Keywords: Beweistheorie; Automatisches Beweisen; Induktion; Baumgrammatiken
proof theory; automated deduction; induction; tree grammars
URI: https://doi.org/10.34726/hss.2021.55608
DOI: 10.34726/hss.2021.55608
Library ID: AC16140047
Organisation: E104 - Institut für Diskrete Mathematik und Geometrie 
Publication Type: Thesis
Appears in Collections:Thesis

Files in this item:

Show full item record

Page view(s)

checked on May 27, 2021


checked on May 27, 2021

Google ScholarTM


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.