Inductive theorem proving based on tree grammars

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.