Title: On the Generation of Quantified Lemmas
Language: English
Authors: Ebner, Gabriel 
Hetzl, Stefan
Leitsch, Alexander 
Reis, Giselle 
Weller, Daniel 
Category: Research Article
Forschungsartikel
Issue Date: 2018
Journal: Journal of Automated Reasoning
ISSN: 0168-7433
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.
Keywords: Cut-introduction; Herbrand’s theorem; Proof theory; Lemma generation; The resolution calculus
DOI: 10.1007/s10817-018-9462-8
Library ID: AC15324292
URN: urn:nbn:at:at-ubtuw:3-5141
Organisation: E104 - Institut für Diskrete Mathematik und Geometrie 
Publication Type: Article
Artikel
Appears in Collections:Article

Files in this item:

Show full item record

Page view(s)

37
checked on Jun 20, 2021

Download(s)

94
checked on Jun 20, 2021

Google ScholarTM

Check


This item is licensed under a Creative Commons License Creative Commons