Abstract
If there exist efficient procedures (canonizers) for reducing terms of two first-order theories to canonical form, can one use them to construct such a procedure for terms of the disjoint union of the two theories? We prove this is possible whenever the original theories are convex. As an application, we prove that algorithms for solving equations in the two theories (solvers) cannot be combined in a similar fashion. These results are relevant to the widely used Shostak’s method for combining decision procedures for theories. They provide the first rigorous answers to the questions about the possibility of directly combining canonizers and solvers.
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.
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
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, United Kingdom (1998)
Baader, F., Tinelli, C.: Deciding the word problem in the union of equational theories. Information and Computation 178, 346–390 (2002)
Barrett, C.: Checking Validity of Quantifier-free formulas in Combinations of First- Order Theories. PhD thesis, Stanford University (2002)
Barrett, C., Dill, D., Levitt, J.: Validity checking for combinations of theories with equality. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 187–201. Springer, Heidelberg (1996)
Barrett, C.W., Dill, D.L., Stump, A.: A generalization of Shostak’s method for combining decision procedures. In: Armando, A. (ed.) FroCos 2002. LNCS (LNAI), vol. 2309, pp. 132–147. Springer, Heidelberg (2002)
Bjørner, N., et al.: Deductive-algorithmic verification of reactive and real-time systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 415–418. Springer, Heidelberg (1996)
Conchon, S., Krstić, S.: Strategies for combining decision procedures. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 537–552. Springer, Heidelberg (2003)
Cyrluk, D., Lincoln, P., Shankar, N.: On Shostak’s decision procedure for combinations of theories. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS (LNAI), vol. 1104, pp. 463–477. Springer, Heidelberg (1996)
Ganzinger, H.: Shostak light. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 332–347. Springer, Heidelberg (2002)
Kapur, D.: A rewrite rule based framework for combining decision procedures. In: Armando, A. (ed.) FroCos 2002. LNCS (LNAI), vol. 2309, pp. 87–103. Springer, Heidelberg (2002)
Krstić, S., Conchon, S.: Canonization for disjoint union of theories. Technical Report CSE-03-003, OHSU (2003)
Manna, Z., Zarba, C.G.: Combining decision procedures. In: Aichernig, B.K., Maibaum, T. (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol. 2757, pp. 381–422. Springer, Heidelberg (2003)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems 1(2), 245–257 (1979)
Owre, S., Rushby, J., Shankar, N., von Henke, F.: Formal verification for faulttolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering 21(2), 107–125 (1995)
Pigozzi, D.: The join of equational thories. Colloquium Mathematicum 30, 15–25 (1974)
Rueß, H., Shankar, N.: Deconstructing Shostak. In: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS-2001), pp. 19–28. IEEE Computer Society Press, Los Alamitos (2001)
Shankar, N.: Little engines of proof. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 1–20. Springer, Heidelberg (2002)
Shankar, N., Rueß, H.: Combining Shostak theories. In: Tison, S. (ed.) RTA 2002. LNCS, vol. 2378, pp. 1–19. Springer, Heidelberg (2002)
Shostak, R.E.: Deciding combinations of theories. Journal of the ACM 31(1), 1–12 (1984)
Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson–Oppen combination procedure. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems: Proceedings of the 1st International Workshop, Munich, Germany. Applied Logic, pp. 103–120. Kluwer, Dordrecht (1996)
Tinelli, C., Ringeissen, C.: Unions of non-disjoint theories and combinations of satisfiability procedures. Theoretical Computer Science 290, 291–353 (2003)
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
Krstić, S., Conchon, S. (2003). Canonization for Disjoint Unions of Theories. In: Baader, F. (eds) Automated Deduction – CADE-19. CADE 2003. Lecture Notes in Computer Science(), vol 2741. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45085-6_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-45085-6_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40559-7
Online ISBN: 978-3-540-45085-6
eBook Packages: Springer Book Archive