Overview

The Constraint Contextual Rewriting Project

Overview

For a complete introduction to Constraint Contextual Rewriting the interested reader is referred to the two following papers: [ccr-ftp98] and [ccr-frocos2000]. For a description of the practical extension mechanism for decision procedure the reader is referred to the paper [edp-jucs2001].

The Problem

The effective integration of decision procedures in formula simplification constitutes one of the key ingredients in many state-of-the-art automated reasoning systems such as Acl2 (NQTHM), PVS, Tecton, and STeP. In many cases the interplay between the reasoning modules is so tight and complicated that providing an accurate description of the integration is a challenge. As a matter of fact, the description available in the literature are given by examples or in informal ways with design decision often intermixed with implementation details. As a consequence, most of the existing integration schemas are difficult to grasp, making it very difficult any attempt to modify, extend, reuse, and reason about. The goal of the CCR Project is the integration of reasoning specialists in simplifiers.

Our solution

This goal can be achieved in two ways. First, (in many cases) the integration of decision procedure in a verification systems is performed by means of a tight cooperation between a rewriting engine and a decision procedure. Making this cooperation effective is a daunting task and it requires sophisticated techniques. The difficulties lie in both formalizing and proving the desired properties (e.g. termination) of the designed integration schema. Second, the decision procedure can be extended by means of a lemma speculation mechanism in such a way that it is capable of tackling problems falling outside the scope it has been originally designed for. Devising sound, terminating, complete (at least for certain subclasses of formulae), and efficient mechanisms to extend decision procedure is a very difficult task. In the following, we analize the proposed solutions in more details.

Based on the integration of a linear arithmetic decision procedure in the rewriting activty of the Boyer and Moore prover, we propose a new form of contextual rewriting called Constraint Contextual Rewriting where the decision procedure is allowed to access and modify the rewriting context. Under the assumption that certain interface functionalities (satisying some abstract properties) are provided by the decision procedure DP, CCR enjoys the following properties (which have been formally stated and proved): it is parametric in DP, it is sound, and it is terminating.
The formalization of CCR relies on the notion of Contextual Reduction System (CRS, for short), which generalizes the standard notion of abstract reduction system. Informally, a CRS is defined by a set of ternary relations toghether with a set of inference roles that define the relations by (mutual) induction. The concept of CRS is the starting point for formally specifying and reasoning about integration schemas between rewriting and decision procedures.
In order to tackle the second problem, there are two options. First, we can devise practical extension mechanisms to lift a decision procedure for a theory T to proof procedures for a theory T' containing T. We propose such an extension mechanism in [edp-jucs2001] generalizing the augmentation technique devised by Boyer and Moore. We have proved the soundness and the termination of the schema. In this case, we neglect completeness on pragmatical grounds: the goal is to make decision procedures (available in state-of-the-art verification systems) capable of coping with the wide variety of proof obligations arising in real theorem proving efforts. Second, we can insist on the issue of completeness in order to lift a decision procedure for a theory T to a decision procedure for a theory T' containing T. Work is undergone to lift a decison procedure for ground equality based on congruence closure to decision procedures for the theories of lists, commutativity, cancellation, arrays, and homomorphism. In this case, we have an axiom instantiation mechanism which feeds the decision procedure for ground equality all the ground instances of the axioms which allow to decide any formula in the extended theory. The decision procedure based on congruence closure is modelled as a completion procedure. The paramodolation calculus (one of the most important rewriting techniques in literature) plays two roles. First, the paramodolation rule is used as a tool to design the axiom instantiation mechanism for the extended theory. Second, the refutational completeness of the paramodolation calculus is the key property to prove the (refutational) completeness of the decision procedure for the extended theory.

This web site is maintained by the AI-lab webmaster.
Last updated: 14-Dec-2006