Silvio Ranise, DIST, Univ. di Genova
Title: Constraint Contextual Rewriting (joint work with Alessandro Armando)
Abstract. 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 talk we describe the specification of CCR emphasizing the control issues related to its termination. Finally, we very briefly overview the system Rewrite and Decision procedure Laboratory (RDL) which implements CCR.
Constraint Contextual Rewriting Project Home Page