Partial matching for analogy discovery in proofs and counter-examples

Abstract

The problem of analogy in theorem proving has been studied for several years now (see [5, 10, 12] for example). Those works restrict the use of analogy to proofs, disregarding the possibilities of using analogy also for counter-examples construction. Moreover, they deal with the problem of proving a new theorem once an appropriate source theorem has been provided as a guideline. We overcome these drawbacks by using a method for model construction developed in our group and by generalizing proofs (or counter-examples constructions) before including them in the database of source examples. Analogy discovery relies on partial matching between a target statement, and a source (generalized) refutation or counter-example construction, thus allowing more targets to be regarded as “analogous” to a source. It increases the power of an analogy-based prover, by recognizing subgoals within a source refutation or model building. We use in this purpose notions of graph cut sets, and incremental update of statements.

Funded by DRET-France

Funded by MRE-France