DSpace-CRIS at TU Wienhttps://repositum.tuwien.atThe reposiTUm digital repository system captures, stores, indexes, preserves, and distributes digital research material.Sun, 25 Jul 2021 22:42:59 GMT2021-07-25T22:42:59Z5021Finding loop invariants using tree grammarshttp://hdl.handle.net/20.500.12708/3747Title: Finding loop invariants using tree grammars
Authors: Ebner, Gabriel
Abstract: This thesis applies a method for inductive theorem proving based on tree grammars developed by Eberhard and Hetzl to the generation of loop invariants. We consider the verification of simple loops, which do not contain nested loops, and invariants with a single universal quantifier. The verification of this class of programs is reduced to the existing method for inductive proofs, giving an automated method for finding loop invariants. Chapter 1 contains a new exposition of the existing work on tree grammars, culminating in an efficient algorithm to find a minimal grammar covering a given language. Such a minimal grammar consists of productions in a normal form---these normal forms are described using a logic of term algebras. We also investigate the relation to anti-unification. In chapters 2 and 3 we summarize the existing work on proofs and their grammars. The extraction of Herbrand sequents from cut-free proofs is generalized to proofs with universally quantified cuts: there we can extract a totally rigid tree grammar; for proofs with a single induction, we obtain sip grammars. Inverting this extraction allows us introduce cuts, or induction, respectively. The case of inductive proofs and their sip grammars is slightly generalized to allow for the reduction of loop verification problems. In chapters 4 and 5 the verification of loops without nested loops is reduced to the inductive case. This reduction induces a class of grammars; we give an algorithm for efficiently finding a minimal grammar in this class that covers a given language.
Thu, 01 Jan 2015 00:00:00 GMThttp://hdl.handle.net/20.500.12708/37472015-01-01T00:00:00ZInductive theorem proving based on tree grammarshttp://hdl.handle.net/20.500.12708/16832Title: Inductive theorem proving based on tree grammars
Authors: Ebner, Gabriel
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.
Description: Arbeit an der Bibliothek noch nicht eingelangt - Daten nicht geprüft; Abweichender Titel nach Übersetzung der Verfasserin/des Verfassers
Fri, 01 Jan 2021 00:00:00 GMThttp://hdl.handle.net/20.500.12708/168322021-01-01T00:00:00Z