Skip to main content
SpringerLink
Log in

Canonization for Disjoint Unions of Theories

  • Conference paper
Automated Deduction – CADE-19 (CADE 2003)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2741))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, United Kingdom (1998)

    Google Scholar 

  2. Baader, F., Tinelli, C.: Deciding the word problem in the union of equational theories. Information and Computation 178, 346–390 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  3. Barrett, C.: Checking Validity of Quantifier-free formulas in Combinations of First- Order Theories. PhD thesis, Stanford University (2002)

    Google Scholar 

  4. 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)

    Chapter  Google Scholar 

  5. 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)

    Chapter  Google Scholar 

  6. 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)

    Google Scholar 

  7. 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)

    Chapter  Google Scholar 

  8. 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)

    Google Scholar 

  9. Ganzinger, H.: Shostak light. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 332–347. Springer, Heidelberg (2002)

    Google Scholar 

  10. 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)

    Chapter  Google Scholar 

  11. Krstić, S., Conchon, S.: Canonization for disjoint union of theories. Technical Report CSE-03-003, OHSU (2003)

    Google Scholar 

  12. 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)

    Chapter  Google Scholar 

  13. Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems 1(2), 245–257 (1979)

    Article  MATH  Google Scholar 

  14. 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)

    Article  Google Scholar 

  15. Pigozzi, D.: The join of equational thories. Colloquium Mathematicum 30, 15–25 (1974)

    MATH  MathSciNet  Google Scholar 

  16. 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)

    Chapter  Google Scholar 

  17. 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)

    Chapter  Google Scholar 

  18. Shankar, N., Rueß, H.: Combining Shostak theories. In: Tison, S. (ed.) RTA 2002. LNCS, vol. 2378, pp. 1–19. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  19. Shostak, R.E.: Deciding combinations of theories. Journal of the ACM 31(1), 1–12 (1984)

    Article  MATH  MathSciNet  Google Scholar 

  20. 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)

    Google Scholar 

  21. Tinelli, C., Ringeissen, C.: Unions of non-disjoint theories and combinations of satisfiability procedures. Theoretical Computer Science 290, 291–353 (2003)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. OGI School of Science & Engineering at Oregon Health & Sciences University,  

    Sava Krstić

  2. École des Mines de Nantes,  

    Sylvain Conchon

Authors
  1. Sava Krstić
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sylvain Conchon
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Theoretical Computer Science, TU Dresden, Germany

    Franz Baader

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation