A framework for the flexible integration of a class of decision procedures into theorem provers

Abstract

The role of decision procedures is often essential in theorem proving. Decision procedures can reduce the search space of heuristic components of a prover and increase its abilities. However, in some ap­plications only a small number of conjectures fall within the scope of the available decision procedures. Some of these conjectures could in an informal sense fall ‘just outside’ that scope. In these situations a problem arises because lemmas have to be invoked or the decision procedure has to communicate with the heuristic component of a theorem prover. This problem is also related to the general problem of how to flexibly integrate decision procedures into heuristic theorem provers. In this paper we ad­dress such problems and describe a framework for the flexible integration of decision procedures into other proof methods. The proposed frame­work can be used in different theorem provers, for different theories and for different decision procedures. New decision procedures can be simply ‘plugged-in’ to the system. As an illustration, we describe an instantia­tion of this framework within the Clam proof-planning system, to which it is well suited. We report on some results using this implementation.