{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T09:10:02Z","timestamp":1737364202944,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439165"},{"type":"electronic","value":"9783540456100"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45610-4_1","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T06:47:11Z","timestamp":1186901231000},"page":"1-18","source":"Crossref","is-referenced-by-count":22,"title":["Combining Shostak Theories"],"prefix":"10.1007","author":[{"given":"Natarajan","family":"Shankar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Harald","family":"Rue\u00df","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"key":"1_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/BFb0031808","volume-title":"Formal Methods in Computer-Aided Design (FMCAD\u2019 96)","author":"C. Barrett","year":"1996","unstructured":"Clark Barrett, David Dill, and Jeremy Levitt. Validity checking for combinations of theories with equality. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer-Aided Design (FMCAD\u2019 96), volume 1166 of Lecture Notes in Computer Science, pages 187\u2013201, Palo Alto, CA, November 1996. Springer-Verlag."},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Clark W. Barrett, David L. Dill, and Aaron Stump. A generalization of Shostak\u2019s method for combining decision procedures. In A. Armando, editor, Frontiers of Combining Systems, 4th International Workshop, FroCos 2002, number 2309 in Lecture Notes in Artificial Intelligence, pages 132\u2013146, Berlin, Germany, April 2002. Springer-Verlag.","DOI":"10.1007\/3-540-45988-X_11"},{"key":"1_CR3","unstructured":"Nikolaj Bj\u00f8rner. Integrating Decision Procedures for Temporal Verification. PhD thesis, Stanford University, 1999."},{"key":"1_CR4","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1006\/jsco.1996.0009","volume":"21","author":"F. Baader","year":"1996","unstructured":"F. Baader and K. Schulz. Unification in the union of disjoint equational theories: Combining decision procedures. J. Symbolic Computation, 21:211\u2013243, 1996.","journal-title":"J. Symbolic Computation"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Leo Bachmair, Ashish Tiwari, and Laurent Vigneron. Abstract congruence closure. Journal of Automated Reasoning, 2002. To appear.","DOI":"10.1023\/B:JARS.0000009518.26415.49"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"David Cyrluk, Patrick Lincoln, and N. Shankar. On Shostak\u2019s decision procedure for combinations of theories. In M. A. McRobbie and J. K. Slaney, editors, Automated Deduction\u2014CADE-13, volume 1104 of Lecture Notes in Artificial Intelligence, pages 463\u2013477, New Brunswick, NJ, July\/August 1996. Springer-Verlag.","DOI":"10.1007\/3-540-61511-3_107"},{"issue":"4","key":"1_CR7","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1145\/322217.322228","volume":"27","author":"P.J. Downey","year":"1980","unstructured":"P.J. Downey, R. Sethi, and R.E. Tarjan. Variations on the common subexpressions problem. Journal of the ACM, 27(4):758\u2013771, 1980.","journal-title":"Journal of the ACM"},{"key":"1_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1007\/3-540-44585-4_22","volume-title":"Computer-Aided Verification, CAV\u2019 2001","author":"J.-C. Filli\u00e2tre","year":"2001","unstructured":"J.-C. Filli\u00e2tre, S. Owre, H. Rue\u00df, and N. Shankar. ICS: Integrated Canonization and Solving. In G. Berry, H. Comon, and A. Finkel, editors, Computer-Aided Verification, CAV\u2019 2001, volume 2102 of Lecture Notes in Computer Science, pages 246\u2013249, Paris, France, July 2001. Springer-Verlag."},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Jonathan Ford and Natarajan Shankar. Formal verification of a combination decision procedure. In A. Voronkov, editor, Proceedings of CADE-19, Berlin, Germany, 2002. Springer-Verlag.","DOI":"10.1007\/3-540-45620-1_29"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Harald Ganzinger. Shostak light. In A. Voronkov, editor, Proceedings of CADE-19, Berlin, Germany, 2002. Springer-Verlag.","DOI":"10.1007\/3-540-45620-1_28"},{"key":"1_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/3-540-62950-5_59","volume-title":"International Conference on Rewriting Techniques and Applications, RTA \u201897","author":"D. Kapur","year":"1997","unstructured":"Deepak Kapur. Shostak\u2019s congruence closure as completion. In H. Comon, editor, International Conference on Rewriting Techniques and Applications, RTA \u201897, number 1232 in Lecture Notes in Computer Science, pages 23\u201337, Berlin, 1997. Springer-Verlag."},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Dexter Kozen. Complexity of finitely presented algebras. In Conference Record of the Ninth Annual ACM Symposium on Theory of Computing, pages 164\u2013177, Boulder, Colorado, 2\u20134 May 1977.","DOI":"10.1145\/800105.803406"},{"key":"1_CR13","unstructured":"Jeremy R. Levitt. Formal Verification Techniques for Digital Systems. PhD thesis, Stanford University, 1999."},{"issue":"2","key":"1_CR14","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245\u2013257, 1979.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"1_CR15","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"G. Nelson and D. C. Oppen. Fast decision procedures based on congruence closure. Journal of the ACM, 27(2):356\u2013364, 1980.","journal-title":"Journal of the ACM"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Harald Rue\u00df and Natarajan Shankar. Deconstructing Shostak. In 16th Annual IEEE Symposium on Logic in Computer Science, pages 19\u201328, Boston, MA, July 2001. IEEE Computer Society.","DOI":"10.1109\/LICS.2001.932479"},{"key":"1_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/3-540-44755-5_3","volume-title":"Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001","author":"N. Shankar","year":"2001","unstructured":"Natarajan Shankar. Using decision procedures with a higher-order logic. In Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001, volume 2152 of Lecture Notes in Computer Science, pages 5\u201326, Edinburgh, Scotland, September 2001. Springer-Verlag. Available at ftp:\/\/ftp.csl.sri.com\/pub\/users\/shankar\/tphols2001.ps.gz."},{"key":"1_CR18","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1145\/359545.359570","volume":"21","author":"R. Shostak","year":"1978","unstructured":"R. Shostak. An algorithm for reasoning about equality. Comm. ACM, 21:583\u2013585, July 1978.","journal-title":"Comm. ACM"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Robert E. Shostak. Deciding combinations of theories. Journal of the ACM, 31(1):1\u201312, January 1984.","DOI":"10.1145\/2422.322411"},{"key":"1_CR20","series-title":"PhD thesis","volume-title":"Decision Procedures in Automated Deduction","author":"A. Tiwari","year":"2000","unstructured":"Ashish Tiwari. Decision Procedures in Automated Deduction. PhD thesis, State University of New York at Stony Brook, 2000."}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45610-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T08:50:17Z","timestamp":1737363017000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45610-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439165","9783540456100"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-45610-4_1","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}