DSpace-CRIS at TU Wienhttps://repositum.tuwien.atThe reposiTUm digital repository system captures, stores, indexes, preserves, and distributes digital research material.Mon, 27 Sep 2021 17:10:43 GMT2021-09-27T17:10:43Z5011On the Generation of Quantified Lemmashttp://hdl.handle.net/20.500.12708/565Title: On the Generation of Quantified Lemmas
Authors: Ebner, Gabriel; Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Weller, Daniel
Abstract: In this paper we present an algorithmic method of lemma introduction. Given a proof in predicate logic with equality the algorithm is capable of introducing several universal lemmas. The method is based on an inversion of Gentzenâ€™s cut-elimination method for sequent calculus. The first step consists of the computation of a compact representation (a so-called decomposition) of Herbrand instances in a cut-free proof. Given a decomposition the problem of computing the corresponding lemmas is reduced to the solution of a second-order unification problem (the solution conditions). It is shown that that there is always a solution of the solution conditions, the canonical solution. This solution yields a sequence of lemmas and, finally, a proof based on these lemmas. Various techniques are developed to simplify the canonical solution resulting in a reduction of proof complexity. Moreover, the paper contains a comprehensive empirical evaluation of the implemented method and gives an application to a mathematical proof.
Mon, 01 Jan 2018 00:00:00 GMThttp://hdl.handle.net/20.500.12708/5652018-01-01T00:00:00Z