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
|
| الموضوعات: | |
| الوسوم: |
إضافة وسم
لا توجد وسوم, كن أول من يضع وسما على هذه التسجيلة!
|
| _version_ | 1864513522158796800 |
|---|---|
| author | Gabriel Ebner (23277217) |
| author2 | Stefan Hetzl (23277220) Alexander Leitsch (23277223) Giselle Reis (23276149) Daniel Weller (8409270) |
| author2_role | author author author author |
| author_facet | Gabriel Ebner (23277217) Stefan Hetzl (23277220) Alexander Leitsch (23277223) Giselle Reis (23276149) Daniel Weller (8409270) |
| author_role | author |
| dc.creator.none.fl_str_mv | Gabriel Ebner (23277217) Stefan Hetzl (23277220) Alexander Leitsch (23277223) Giselle Reis (23276149) Daniel Weller (8409270) |
| dc.date.none.fl_str_mv | 2018-03-23T09:00:00Z |
| dc.identifier.none.fl_str_mv | 10.1007/s10817-018-9462-8 |
| dc.relation.none.fl_str_mv | https://figshare.com/articles/journal_contribution/On_the_Generation_of_Quantified_Lemmas/31446001 |
| dc.rights.none.fl_str_mv | CC BY 4.0 info:eu-repo/semantics/openAccess |
| dc.subject.none.fl_str_mv | Information and computing sciences Artificial intelligence Mathematical sciences Pure mathematics Cut-introduction Herbrand’s theorem Proof theory Lemma generation The resolution calculus |
| dc.title.none.fl_str_mv | On the Generation of Quantified Lemmas |
| dc.type.none.fl_str_mv | Text Journal contribution info:eu-repo/semantics/publishedVersion text contribution to journal |
| description | <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> |
| eu_rights_str_mv | openAccess |
| id | Manara2_1eeaa56b43b41c9e27296f7d8f6403be |
| identifier_str_mv | 10.1007/s10817-018-9462-8 |
| network_acronym_str | Manara2 |
| network_name_str | Manara2 |
| oai_identifier_str | oai:figshare.com:article/31446001 |
| publishDate | 2018 |
| repository.mail.fl_str_mv | |
| repository.name.fl_str_mv | |
| repository_id_str | |
| rights_invalid_str_mv | CC BY 4.0 |
| spelling | On the Generation of Quantified LemmasGabriel Ebner (23277217)Stefan Hetzl (23277220)Alexander Leitsch (23277223)Giselle Reis (23276149)Daniel Weller (8409270)Information and computing sciencesArtificial intelligenceMathematical sciencesPure mathematicsCut-introductionHerbrand’s theoremProof theoryLemma generationThe resolution calculus<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>2018-03-23T09:00:00ZTextJournal contributioninfo:eu-repo/semantics/publishedVersiontextcontribution to journal10.1007/s10817-018-9462-8https://figshare.com/articles/journal_contribution/On_the_Generation_of_Quantified_Lemmas/31446001CC BY 4.0info:eu-repo/semantics/openAccessoai:figshare.com:article/314460012018-03-23T09:00:00Z |
| spellingShingle | On the Generation of Quantified Lemmas Gabriel Ebner (23277217) Information and computing sciences Artificial intelligence Mathematical sciences Pure mathematics Cut-introduction Herbrand’s theorem Proof theory Lemma generation The resolution calculus |
| status_str | publishedVersion |
| title | On the Generation of Quantified Lemmas |
| title_full | On the Generation of Quantified Lemmas |
| title_fullStr | On the Generation of Quantified Lemmas |
| title_full_unstemmed | On the Generation of Quantified Lemmas |
| title_short | On the Generation of Quantified Lemmas |
| title_sort | On the Generation of Quantified Lemmas |
| topic | Information and computing sciences Artificial intelligence Mathematical sciences Pure mathematics Cut-introduction Herbrand’s theorem Proof theory Lemma generation The resolution calculus |