CONSTRUCTING PREDICATE MAPPINGS FOR GOAL-DEPENDENT ABSTRACTION

In theorem proving with abstraction, it is required for system designe rs to provide a useful abstraction. However, such a task is so difficu lt that it would be worth studying an automatic construction of abstra ction. In this paper, we propose a new framework of coal-Dependent Abs traction in which an appropriate abstraction is selected according to each goal to be proved. Towards Goal-Dependent Abstraction, we present an algorithm for constructing an appropriate abstraction for a given goal. The appropriateness is defined in terms of Upward-Property and D ownward-Property. Since our abstraction is based on predicate mapping, the algorithm in fact computes predicate mappings based on which appr opriate abstractions can be constructed. Given a goal, candidate predi cate mappings are generated and then tested for their appropriateness for the goal. In order to find appropriate mappings efficiently, we pr esent a property to prune useless candidate generations. The numbers o f pruned candidates are evaluated in the best and worst cases. Further more some experimental results show that many useless candidates can b e pruned with the property and the obtained appropriate predicate mapp ings (abstractions) fit our intuition. From the experimental results, we could expect our study in this paper to contribute to the fields of analogical reasoning and case-based reasoning as well as theorem-prov ing.