On the Generation of Quantified Lemmas
<p dir="ltr">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 calc...
محفوظ في:
| المؤلف الرئيسي: | |
|---|---|
| مؤلفون آخرون: | , , , |
| منشور في: |
2018
|
| الموضوعات: | |
| الوسوم: |
إضافة وسم
لا توجد وسوم, كن أول من يضع وسما على هذه التسجيلة!
|
| الملخص: | <p dir="ltr">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.</p><h2 dir="ltr">Other Information</h2><p dir="ltr">Published in: Journal of Automated Reasoning<br>License: <a href="https://creativecommons.org/licenses/by/4.0" target="_blank">https://creativecommons.org/licenses/by/4.0</a><br>See article on publisher's website: <a href="https://dx.doi.org/10.1007/s10817-018-9462-8" target="_blank">https://dx.doi.org/10.1007/s10817-018-9462-8</a></p> |
|---|