An Abstraction for Proof Planning : The S-Abstraction

Abstract

This paper presents a new kind of abstraction, which has been developed for the purpose of proof planning. The basic idea of this paper is to abstract a given theorem and to find an abstract proof of it. Once an abstract proof has been found, this proof has to be refined to a real proof of the original theorem. We present a goal oriented abstraction for the purpose of equality proof planning, which is parameterized by common parts of the left- and right-hand sides of the given equality. Therefore, this abstraction technique provides an abstract equality problem which is more adequate than those generated by the abstractions known so far. The presented abstraction also supports the heuristic search process based on the difference reduction paradigm. We give a formal definition of the abstract space including the objects and their manipulation. Furthermore, we prove some properties in order to allow an efficient implementation of the presented abstraction.