On the Generation of Quantified Lemmas

Gabriel Ebner, Stefan Hetzl*, Alexander Leitsch, Giselle Reis, Daniel Weller

*Corresponding author for this work

Research output: Contribution to JournalArticleAcademicpeer-review

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.

Original languageEnglish
Pages (from-to)95-126
Number of pages32
JournalJournal of Automated Reasoning
Volume63
Issue number1
DOIs
Publication statusPublished - 15 Jun 2019
Externally publishedYes

Keywords

  • Cut-introduction
  • Herbrand’s theorem
  • Lemma generation
  • Proof theory
  • The resolution calculus

Fingerprint Dive into the research topics of 'On the Generation of Quantified Lemmas'. Together they form a unique fingerprint.

  • Cite this