Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Frontiers of Combining Systems

FroCoS 2009: Frontiers of Combining Systems pp 68–83Cite as

Combining Equational Reasoning

  • Conference paper

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

Abstract

Given a theory \(\mathbb{T}\), a set of equations E, and a single equation e, the uniform word problem (UWP) is to determine if \(E\Rightarrow e\) in the theory \(\mathbb{T}\). We recall the classic Nelson-Oppen combination result for solving the UWP over combinations of theories and then present a constructive version of this result for equational theories. We present three applications of this constructive variant. First, we use it on the pure theory of equality (\(\mathbb{T}_{EQ}\)) and arrive at an algorithm for computing congruence closure of a set of ground term equations. Second, we use it on the theory of associativity and commutativity (\(\mathbb{T}_{AC}\)) and obtain a procedure for computing congruence closure modulo AC. Finally, we use it on the combination theory \(\mathbb{T}_{EQ}\cup\mathbb{T}_{AC}\cup\mathbb{T}_{PR}\), where \(\mathbb{T}_{PR}\) is the theory of polynomial rings, to present a decision procedure for solving the UWP for this combination.

Research supported in part by NSF grants CNS-0720721 and CNS-0834810 and NASA grant NNX08AB95A.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Armando, A., Ranise, S., Rusinowitch, M.: Uniform derivation of decision procedures by superposition. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 513–527. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  2. Audemard, G., Bertoli, P., Cimatti, A., Kornilowicz, A., Sebastiani, R.: A SAT based approach for solving formulas over boolean and linear mathematical propositions. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 195–210. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  3. Bachmair, L., Ganzinger, H.: Buchberger’s algorithm: A constraint-based completion procedure. In: Jouannaud, J.-P. (ed.) CCL 1994. LNCS, vol. 845, pp. 285–301. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  4. Bachmair, L., Ramakrishnan, I.V., Tiwari, A., Vigneron, L.: Congruence closure modulo Associativity-Commutativity. In: Kirchner, H. (ed.) FroCos 2000. LNCS (LNAI), vol. 1794, pp. 245–259. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  5. Bachmair, L., Tiwari, A.: D-bases for polynomial ideals over commutative noetherian rings. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 113–127. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  6. Bachmair, L., Tiwari, A.: Abstract congruence closure and specializations. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, pp. 64–78. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  7. Barrett, C., Dill, D., Stump, A.: A generalization of Shostak’s method for combining decision procedures. In: Armando, A. (ed.) FroCos 2002. LNCS (LNAI), vol. 2309, p. 132. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  8. Basu, S., Pollack, R., Roy, M.-F.: Algorithms in real algebraic geometry. Algorithms and Computation in Mathematics, vol. 10. Springer, Heidelberg (2003)

    MATH  Google Scholar 

  9. Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T.A., Ranise, S., van Rossum, P., Sebastiani, R.: Efficient theory combination via boolean search. Information and Computation 204(10), 1493–1525 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  10. Buchberger, B.: An algorithm for finding a basis for the residue class ring of a zero-dimensional ideal. PhD thesis, University of Innsbruck, Austria (1965)

    Google Scholar 

  11. Buchberger, B.: A critical-pair completion algorithm for finitely generated ideals in rings. In: Börger, E., Rödding, D., Hasenjaeger, G. (eds.) Rekursive Kombinatorik 1983. LNCS, vol. 171, pp. 137–161. Springer, Heidelberg (1984)

    Chapter  Google Scholar 

  12. Collins, G.E.: Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975)

    Google Scholar 

  13. Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th ACM Symp. on Principles of Programming Languages, POPL 1977, pp. 238–252 (1977)

    Google Scholar 

  14. de Moura, L., Rueß, H., Sorea, M.: Lazy theorem proving for bounded model checking over infinite domains. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 438–455. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  15. Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  16. Flanagan, C., Joshi, R., Ou, X., Saxe, J.: Theorem proving using lazy proof explication. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 355–367. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  17. Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175–188. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  18. Gulwani, S., Tiwari, A.: Assertion checking over combined abstraction of linear arithmetic and uninterpreted functions. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 279–293. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  19. Gulwani, S., Tiwari, A.: Combining abstract interpreters. In: PLDI (June 2006)

    Google Scholar 

  20. Gulwani, S., Tiwari, A., Necula, G.C.: Join algorithms for the theory of uninterpreted symbols. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 311–323. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  21. Harrison, J.: Theorem proving with the real numbers. Springer, Heidelberg (1998)

    Book  MATH  Google Scholar 

  22. Hong, H.: Quantifier elimination in elementary algebra and geometry by partial cylindrical algebraic decomposition version 13 (1995), http://www.gwdg.de/~cais/systeme/saclib,www.eecis.udel.edu/~saclib/

  23. Karr, M.: Affine relationships among variables of a program. Acta Informatica 6, 133–151 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  24. Lynch, C., Morawska, B.: Automatic decidability. In: IEEE Symposium on Logic in Computer Science, LICS 2002, pp. 7–16. IEEE Society, Los Alamitos (2002)

    Google Scholar 

  25. Mayr, E.W., Meyer, A.R.: The complexity of the word problems for commutative semigroups and polynomial ideals. Advances in Mathematics 46, 305–329 (1982)

    Article  MathSciNet  MATH  Google Scholar 

  26. Microsoft Research. Z3: An efficient SMT solver, http://research.microsoft.com/projects/z3/

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

    Article  MATH  Google Scholar 

  28. Nieuwenhuis, R., Oliveras, A.: Decision procedures for SAT, SAT modulo theories and beyond. The Barcelogictools. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 23–46. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  29. Oppen, D.: Complexity, convexity and combinations of theories. Theoretical Computer Science 12, 291–302 (1980)

    Article  MathSciNet  MATH  Google Scholar 

  30. Pratt, V.R.: Two easy theories whose combination is hard. Technical report, MIT (1977)

    Google Scholar 

  31. SRI International. Yices: An SMT solver, http://yices.csl.sri.com/

  32. Stump, A., Barrett, C.W., Dill, D.L.: CVC: A cooperating validity checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 500–504. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  33. Tarski, A.: A Decision Method for Elementary Algebra and Geometry, 2nd edn. University of California Press, Berkeley (1948)

    MATH  Google Scholar 

  34. Tiwari, A.: Decision procedures in automated deduction. PhD thesis, State University of New York at Stony Brook (2000)

    Google Scholar 

  35. Tiwari, A.: An algebraic approach for the unsatisfiability of nonlinear constraints. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, pp. 248–262. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  36. Wolfman, S., Weld, D.: The LPSAT system and its application to resource planning. In: Proc. 16th Intl. Joint Conf. on Artificial Intelligence (1999)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. SRI International, Menlo Park, CA

    Ashish Tiwari

Authors
  1. Ashish Tiwari
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Università degli Studi di Milano, Via Comelico 39, 20135, Milano, Italy

    Silvio Ghilardi

  2. Dipartemento di Ingegneria e Scienza dell’Informazione, Università di Trento, Facoltà di Scienze, Via Sommarive 14, 38050, Povo, Trento, Italy

    Roberto Sebastiani

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Tiwari, A. (2009). Combining Equational Reasoning. In: Ghilardi, S., Sebastiani, R. (eds) Frontiers of Combining Systems. FroCoS 2009. Lecture Notes in Computer Science(), vol 5749. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04222-5_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-04222-5_4

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-04221-8

  • Online ISBN: 978-3-642-04222-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation