

The Constraint Contextual Rewriting Project
Overview
For a complete introduction to Constraint Contextual Rewriting the
interested reader is referred to the two following papers:
[ccrftp98] and
[ccrfrocos2000]. For
a description of the practical extension mechanism for decision
procedure the reader is referred to the paper [edpjucs2001].
The Problem 
The effective integration of decision procedures in formula
simplification constitutes one of the key ingredients in many
stateoftheart 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 [edpjucs2001]
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 stateoftheart
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.

[ Home
 Overview
 Publications
 Lectures and Talks
 Software
 Related links
]
This web site is maintained by the AIlab webmaster.
Last updated: 14Dec2006
