|
|
|
The Constraint Contextual Rewriting Project
Publications
| [issac2001] |
| 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. |
Abstract.
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.
|
|
| [rdl2001] |
| 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 |
Abstract.
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.
|
|
| [ccr-frocos2000] |
| 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 |
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 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.
|
|
| [ccr-ftp98] |
| 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 |
Abstract.
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.
|
| [edp-csl2001] |
| 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 |
Abstract.
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.
|
|
| [edp-jucs2001] |
| 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. |
Abstract.
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.
|
|
| [fmtools00] |
| 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. |
Abstract.
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.
|
|
| [aimsa98] |
| 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 |
Abstract.
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.
|
|
| [aisc98] |
| 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 |
Abstract.
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
|