Lectures and Talks
Related links
Alessandro Armando
Silvio Ranise
Università di Genova

The Constraint Contextual Rewriting Project


Papers about CCR

Maple's Evaluation Process as Constraint Contextual Rewriting.
Alessandro Armando and Clemens Ballarin.
In the Proceedings of the International Symposium on Symbolic and Algebraic Computation (ISSAC'2001). July 22 - 25, 2001, ORCCA and University of Western Ontario.
Maple's evaluator, together with a feature that is usually known as the assume facility, is a combination of modules with specialised reasoning capabilities. These modules are identified, their interfaces are specified, and their interplay is reconstructed as Constraint Contextual Rewriting (CCR), a powerful form of conditional rewriting that incorporates the services provided by a decision procedure. Finally we show how Maple's evaluation process can be strengthened by borrowing ideas from CCR.

System Description: RDL---Rewrite and Decision procedure Laboratory
Alessandro Armando, Luca Compagna, and Silvio Ranise.
In Proceedings of the International Joint Conference on Automated Reasoning (IJCAR 2001), June 18-23, Siena, Italy. ©Springer-Verlag
RDL is a system for formula simplification in a quantifier-free first-order logic with equality. It implements Constraint Contextual Rewriting (CCR, for short), a sound and terminating schema for the tight integration of rewriting and decision procedures. The current system takes a clause and a set of facts as input and returns a simplified version of the input clause. RDL is fully automatic. We describe the current version of the system focusing on the relationships between the implementation and an abstract architecture derived from CCR.

Termination of Constraint Contextual Rewriting
Alessandro Armando & Silvio Ranise.
In Proceedings of the 3rd International Workshop on Frontiers of Combining Systems (FroCoS'2000). Nancy (France), March 22-24, 2000. ©Springer-Verlag
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.

Constraint Contextual Rewriting
Alessandro Armando & Silvio Ranise.
In Proceedings of the International Workshop on First order Theorem Proving (FTP'98). Schloss Wilhelminenberg, Vienna, Austria, November 23 - 25, 1998
We are interested in the problem of integrating decision procedures with rewriting as in many state-of-the-art verification systems. We define Constraint Contextual Rewriting (CCR) as a generalization of Contextual Rewriting, whereby the rewriting context is processed by the available decision procedures. We show how CCR accounts for for some of the most important integration schemas adopted in state-of-the-art verification systems. The rule-based presentation of CCR given in this paper contrasts the practice of describing the integration either by examples or in informal ways with high-level ideas intermixed with implementation details. Important properties (e.g. soundness) of the proposed integration schema can be formally stated and proved. Moreover, the approach is amenable of operationalization. This has allowed us to easily fast-prototype and validate the integration schemas described in this paper.

Papers related to CCR

Uniform Derivation of Decision Procedures by Superposition
Alessandro Armando, Silvio Ranise, and Michael Rusinowtich.
In the Proceedings on the Annual Conference on Computer Science Logic (CSL01), Paris, France, 10-13 September 2001.©Springer-Verlag
We show how a well-known superposition-based inference system for first-order equational logic can be used almost directly as a decision procedure for various theories including lists, arrays, extensional arrays and combinations of them. We also give a superposition-based decision procedure for homomorphism.

A Practical Extension Mechanism for Decision Procedures: the Case Study of Universal Presburger Arithmetic
Alessandro Armando & Silvio Ranise.
In ``Tools for System Design and Verification'', Special Issue of Journal of Universal Computer Science, volume 7, issue 2, pages 124--140.
In this paper, we propose a generic mechanism for extending decision procedures by means of a lemma speculation mechanism. This problem is important in order to widen the scope of decision procedures incorporated in state-of-the-art verification systems. Soundness and termination of the extension schema are formally stated and proved. As a case study, we consider extensions of a decision procedure for the quantifier-free fragment of Presburger Arithmetic to significant fragments of non-linear arithmetic.

A Practical Extension Mechanism for Decision Procedures
Alessandro Armando & Silvio Ranise.
In Proceedings of the 4th Workshop on Tools for System Design and Verification (FM-TOOLS 2000). Reisenburg Castle near Ulm, Germany. Monday 10 July - Thursday 13 July 2000.
The lack of automated support is probably the main obstacle to the application of formal method techniques in the industrial setting. The only way to meet the requirements posed by many industrial applications is to combine the expressiveness of general purpose provers with the efficiency of specialized reasoners. Unfortunately this is a difficult task. The main problem is that only a tiny portion of the proof obligations arising in many practical applications falls exactly in the domain the specialized reasoners are designed to solve. In this paper we propose a general extension mechanism which allows decision procedures to tackle problems falling outside the scope they have been originally designed for, thereby considerably enhancing their usefulness in practical applications. We provide instances of the proposed extension mechanism that enable a decision procedure for the quantifier-free fragment of Presburger Arithmetic to tackle non-linear problems of significant difficulty.

Note. An extended version of the paper is available.

Constraint Solving in Logic Programming and in Automated Deduction: a Comparison
Alessandro Armando, Erica Melis & Silvio Ranise.
In Proceedings of the 8th International Conference on Artificial Intelligence: Methodology, Systems, Applications (AIMSA98). Sozopol, Bulgaria, September 21-23, 1998. LNAI, Vol. 1480, pp. 28-38, Springer. ©Springer-Verlag
Constraint solving has been successfully employed in diverse areas such as Operation Research, Planning, Logic Programming, and Automated Deduction. This has led to the development of a number of specialised approaches as well as to the adoption of different integration schemes and methodologies. In this paper we introduce an approach to incorporate constraint solving in term rewriting and we compare it with the Constraint Logic Programming scheme. We compare the two approaches both at the theoretical and at the implementational level and discuss potentials for cross-fertilisation.

From Integrated Reasoning Specialists to ``Plug-and-Play'' Reasoning Components
Alessandro Armando & Silvio Ranise.
In Proceedings of the Fourth International Conference Artificial Intelligence and Symbolic Computation (AISC98). Plattsburgh, NY, USA. September 16-18, 1998. LNCS vol. 1476, p. 42-54. Springer. ©Springer-Verlag
There is an increasing evidence that a new generation of reasoning systems will be obtained via the integration of different reasoning paradigms. In the verification arena, several proposals have been advanced on the integration of theorem proving with model checking. At the same time, the advantages of integrating symbolic computation with deductive capabilities has been recognized and several proposals to this end have been put forward. We propose a methodology for turning reasoning specialists integrated in state-of-the-art reasoning systems into reusable and implementation independent reasoning components to be used in a ``plug-and-play'' fashion. To test our ideas we have used the Boyer and Moore's linear arithmetic procedure as a case study. We report experimental results which confirm the viability of the approach.

[ Home | Overview | Publications | Lectures and Talks | Software | Related links ]

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