Abstract
Implementing efficient algorithms for combining decision procedures has been a challenge and their correctness precarious. In this paper we describe an inference system that has the classical Nelson-Oppen procedure at its core and includes several optimizations: variable abstraction with sharing, canonization of terms at the theory level, and Shostak’s streamlined generation of new equalities for theories with solvers. The transitions of our system are fine-grained enough to model most of the mechanisms currently used in designing combination procedures. In particular, with a simple language of regular expressions we are able to describe several combination algorithms as strategies for our inference system, from the basic Nelson-Oppen to the very highly optimized one recently given by Shankar and Rueβ. Presenting the basic system at a high level of generality and nondeterminism allows transparent correctness proofs that can be extended in a modular fashion whenever a new feature is introduced in the system. Similarly, the correctness proof of any new strategy requires only minimal additional proof effort.
The research reported in this paper was supported by the NSF Grant CCR-9703218. It was performed while S. Conchon was with OGI School of Science & Engineering.
Chapter PDF
References
L. Bachmair, A. Tiwari, and L. Vigneron. Abstract congruence closure. Journal of Automated Reasoning, 2002. To appear.
C. Barrett. Checking Validity of Quantifier-free formulas in Combinations of First-Order Theories. PhD thesis, Stanford University, 2002.
C. W. Barrett, D. L. Dill, and A. Stump. A generalization of Shostak’s method for combining decision procedures. In Frontiers of Combining Systems (FROCOS), volume 2309 of Lecture Notes in Artificial Intelligence, pages 132–147. Springer-Verlag, 2002.
S. Conchon and S. Krstic. Strategies for combining decision procedures. Technical Report CSE-03-001, OHSU, 2003.
J.-C. Filliatre, S. Owre, H. Rueβ, and N. Shankar. ICS: Integrated Canonization and Solving (Tool presentation). In G. Berry, H. Comon, and A. Finkel, editors, Proceedings of CAV’2001, volume 2102 of Lecture Notes in Computer Science, pages 246–249. Springer-Verlag, 2001.
H. Ganzinger. Shostak light. In A. Voronkov, editor, Automated Deduction-CADE-18, volume 2392 of Lecture Notes in Artificial Intelligence, pages 332–347. Springer-Verlag, 2002.
D. Kapur. A rewrite rule based framework for combining decision procedures. In Frontiers of Combining Systems (FROCOS), volume 2309 of Lecture Notes in Artificial Intelligence, pages 87–103. Springer-Verlag, 2002.
G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245–257, 1979.
G. Nelson and D. C. Oppen. Fast decision procedures based on congruence closure. JACM, 27(2):356–364, 1980.
Ch. Ringeissen. Cooperation of Decision Procedures for the Satisfiability Problem. In F. Baader and K. U. Schulz, editors, Frontiers of Combining Systems: Proceedings of the 1st International Workshop, Applied Logic, pages 121–140. Kluwer Academic Publishers, 1996.
H. Rueβ and N. Shankar. Deconstructing Shostak. In Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS-01), pages 19–28. IEEE Computer Society, 2001.
N. Shankar. Little engines of proof. In L.-H. Eriksson and P. Lindsay, editors, FME 2002: Formal Methods-Getting IT Right, pages 1–20, Copenhagen, 2002. Springer-Verlag.
N. Shankar and H. Rueβ. Combining Shostak theories. In S. Tison, editor, Rewriting Techniques and Applications (RTA), volume 2378 of Lecture Notes in Computer Science, pages 1–19. Springer-Verlag, 2002.
R. E. Shostak. Deciding combinations of theories. Journal of the ACM, 31(1):1–12, 1984.
A. Stump, C. Barrett, and D. Dill. CVC: a Cooperating Validity Checker. In 14th International Conference on Computer-Aided Verification, 2002.
C. Tinelli and M. T. Harandi. A new correctness proof of the Nelson-Oppen combination procedure. In F. Baader and K. U. Schulz, editors, Frontiers of Combining Systems: Proceedings of the 1st International Workshop, Applied Logic, pages 103–120. Kluwer Academic Publishers, 1996.
A. Tiwari. Decision Procedures in Automated Deduction. PhD thesis, University of Stony Brook, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Conchon, S., Krstić, S. (2003). Strategies for Combining Decision Procedures. In: Garavel, H., Hatcliff, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2003. Lecture Notes in Computer Science, vol 2619. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36577-X_39
Download citation
DOI: https://doi.org/10.1007/3-540-36577-X_39
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00898-9
Online ISBN: 978-3-540-36577-8
eBook Packages: Springer Book Archive