Termination of constraint contextual rewriting

The effective integration of decision procedures in formula simplification is a fundamental problem in mechanical verification. The main source of difficulty occurs when the decision procedure is asked to solve goals containing symbols which are interpreted for the prover but uninterpreted for the decision procedure. To cope with the problem, Boyer & Moore proposed a technique, called augmentation, which extends the information available to the decision procedure with suitably selected facts. Constraint Contextual Rewriting (CCR, for short) is an extended form of contextual rewriting which generalizes the Boyer & Moore integration schema. In this paper we give a detailed account of the control issues related to the termination of CCR. These are particularly subtle and complicated since augmentation is mutually dependent from rewriting and it must be prevented from indefinitely extending the set of facts available to the decision procedure. A proof of termination of CCR is given.