Change of Representation in Theorem Proving by Analogy

Abstract

Constructing an analogy between a known and already proven theorem (the base case) and another yet to be proven theorem (the target case) often amounts to finding the appropriate representation at which the base and the target are similar. This is a well-known fact in mathematics, and it was corroborated by our empirical study of a mathematical textbook, which showed that a reformulation of the representation of a theorem and its proof is indeed more often than not a necessary prerequisite for an analogical inference. Thus machine supported reformulation becomes an important component of automated analogy-driven theorem proving too. The reformulation component proposed in this paper is embedded into a proof plan methodology based on methods and meta-methods, where the latter are used to change and appropriately adapt the methods. A theorem and its proof are both represented as a method and then reformulated by the set of metamethods presented in this paper. Our approach supports analogy-driven theorem proving at various levels of abstraction and in principle makes it independent of the given and often accidental representation of the given theorems. Different methods can represent fully instantiated proofs, subproofs, or general proof methods, and hence our approach also supports these three kinds of analogy respectively. By attaching appropriate justifications to meta-methods the analogical inference can often be justified in the sense of Russell. This paper presents a model of analogy-driven proof plan construction and focuses on empirically extracted meta-methods. It classifies and formally describes these meta-methods and shows how to use them for an appropriate reformulation in automated analogy-driven theorem proving.