Abstract
RDL1 simplifies clauses in a quantifier-free first-order logic with equality using a tight integration between rewriting and decision procedures. On the one hand, this kind of integration is considered the key ingredient for the success of state-of-the-art verification systems, such as ACL2 [10], STeP [8], Tecton [9], and Simplify [7]. On the other hand, obtaining a principled and effective integration poses some difficult problems. Firstly, there are no formal accounts of the incorporation of decision procedures in rewriting. This makes it difficult to reason about basic properties such as soundness and termination of the implementation of the proposed schema. Secondly, most integration schemas are targeted to a given decision procedure and they do not allow to easily plug new decision procedures in the rewriting activity. Thirdly, only a tiny portion of the proof obligations arising in many practical verifition efforts falls exactly into the theory decided by the available decision procedure. RDL solves the problems above as follows:
-
1
RDL is based on CCR (Constraint Contextual Rewriting) [1 2], a formally specified integration schema between (ordered) conditional rewriting and a satisfability decision procedure [11]. RDL inherits the properties of soundness [1] and termination [2] of CCR. It is also fully automatic.
-
2
RDL is an open system which can be modularly extended with new decision procedures provided these offer certain interface functionalities (see [2] for details). In its current version, RDL offers ‘plug-and-play’ decision procedures for the theories of Universal Presburger Arithmetic over Integers (UPAI), Universal Theory of Equality (UTE), and UPAI extended with uninterpreted function symbols [13].
-
3
RDL implements instances of a generic extension schema for decision procedures [3]. The key ingredient of such a schema is a lemma speculation mechanism which ‘reduces’ the validity problem of a given theory to the validity problem of one of its sub-theories for which a decision procedure is available. The proposed mechanism is capable of generating lemmas which are entailed by the union of the theory decided by the available decision procedure and the facts stored in the current context. Three instances of the extension schema lifting a decision procedure for UPAI are available. First, augmentation copes with user-defined functions whose properties can be ex- pressed by conditional lemmas. Second, affinization is a mechanism for the ‘on-the-fly’ generation of lemmas to handle a significant class of formulae in the theory of Universal Arithmetic over Integers (UAI). Third, a combination of augmentation and affinization puts together the flexibility of the former with the automation of the latter. Finally, RDL can be extended with new lemma speculation mechanisms provided these meet certain requirements (see [3] for details).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
A. Armando and S. Ranise. Constraint Contextual Rewriting. In Proc. of the 2nd Intl. Workshop on First Order Theorem Proving (FTP’98), Vienna (Austria), pages 65–75, 1998.
A. Armando and S. Ranise. Termination of Constraint Contextual Rewriting. In Proc. of the 3rd Intl. Workshop on Frontiers of Combining Systems (FroCos’2000), LNCS 1794, pages 47–61, March 2000.
A. Armando and S. Ranise. A Practical Extension Mechanism for Decision Procedures: the Case Study of Universal Presburger Arithmetic. J. of Universal Computer Science (Special Issue: Formal Methods and Tools), 7(2):124–140, 2001.
N. S. Bjørner. Integrating Decision Procedures for Temporal Verification. PhD thesis, Computer Science Department, Stanford University, 1998.
R.S. Boyer and J S. Moore. A Computational Logic. Academic Press, 1979.
R.S. Boyer and J S. Moore. Integrating Decision Procedures into Heuristic Theorem Provers: A Case Study of Linear Arithmetic. Machine Intelligence, 11:83–124, 1988.
D. L. Detlefs, G. Nelson, and J. Saxe. Simplify: the ESC Theorem Prover. Technical report, DEC, 1996.
Z. Manna et. al. STeP: The Stanford Temporal Prover. Technical Report CS-TR-94-1518, Stanford University, June 1994.
D. Kapur, D.R. Musser, and X. Nie. An Overview of the Tecton Proof System. Theoretical Computer Science, Vol. 133, October 1994.
M. Kaufmann and J S. Moore. Industrial Strength Theorem Prover for a Logic Based on Common Lisp. IEEE Trans. on Software Engineering, 23(4):203–213, April 1997.
G. Nelson and D. Oppen. Fast Decision Procedures Based on Congruence Closure. J. of the ACM, 27(2):356–364, April 1980.
L. C Paulson. Proving termination of normalization functions for conditional expressions. J. of Automated Reasoning, pages 63–74, 1986.
R.E. Shostak. Deciding Combination of Theories. Journal of the ACM, 31(1):1–12, 1984.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Armando, A., Compagna, L., Ranise, S. (2001). System Description: RDL Rewrite and Decision Procedure Laboratory. In: Goré, R., Leitsch, A., Nipkow, T. (eds) Automated Reasoning. IJCAR 2001. Lecture Notes in Computer Science, vol 2083. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45744-5_54
Download citation
DOI: https://doi.org/10.1007/3-540-45744-5_54
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42254-9
Online ISBN: 978-3-540-45744-2
eBook Packages: Springer Book Archive