Constraint contextual rewriting

The effective integration of decision procedures in formula simplification is a fundamental problem in mechanical verification. In this paper we address the problem by proposing a general pattern of interaction between rewriting and decision procedures and by providing an account of such a pattern of interaction which is precise and concise at the same time. The first step amounts to a generalization of contextual rewriting which allows the available decision procedure to access and manipulate the rewriting context. We call this generalized form of contextual rewriting constraint contextual rewriting (CCR for short). The second step amounts to providing a rule-based presentation of CCR which is modular, declarative, and formal at the same time. This allows us to give a rigorous account of CCR and to formally state and prove its soundness and termination.