{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:26:50Z","timestamp":1767929210588,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540439318","type":"print"},{"value":"9783540456209","type":"electronic"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45620-1_28","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T03:18:26Z","timestamp":1186888706000},"page":"332-346","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Shostak Light"],"prefix":"10.1007","author":[{"given":"Harald","family":"Ganzinger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"28_CR1","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/3-540-63104-6_3","volume-title":"Automated Deduction \u2014 CADE-14, 14th International Conference on Automated Deduction","author":"F. Baader","year":"1997","unstructured":"Baader, F. & Tinelli, C. (1997), A new approach for combining decision procedures for the word problem, and its connection to the nelson-oppen combination method, in W. McCune, ed., \u2018Automated Deduction \u2014 CADE-14, 14th International Conference on Automated Deduction\u2019, LNAI 1249, Springer-Verlag, Townsville, North Queensland, Australia, pp. 19\u201333."},{"key":"28_CR2","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/10721959_5","volume-title":"Automated Deduction \u2014 CADE-17, 17th International Conference on Automated Deduction","author":"L. Bachmair","year":"2000","unstructured":"Bachmair, L. & Tiwari, A. (2000), Abstract congruence closure and specializations, in D. McAllester, ed., \u2018Automated Deduction \u2014 CADE-17, 17th International Conference on Automated Deduction\u2019, LNAI 1831, Springer-Verlag, Pittsburgh, PA, USA, pp. 64\u201378."},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Tiwari, A. & Vigneron, L. (2002), \u2018Abstract congruence closure\u2019, J. Automated Reasoning. To appear.","DOI":"10.1023\/B:JARS.0000009518.26415.49"},{"key":"28_CR4","doi-asserted-by":"crossref","unstructured":"Barrett, C., Dill, D. & Levitt, J. (1996), Validity checking for combinations of theories with equality, in M. Srivas & A. Camilleri, eds, \u2018Formal Methods In Computer-Aided Design, Palo Alto\/CA, USA\u2019, Vol. 1166, Springer-Verlag, pp. 187\u2013201. \n                    http:\/\/cite-seer.nj.nec.com\/barrett96validity.html","DOI":"10.1007\/BFb0031808"},{"key":"28_CR5","doi-asserted-by":"crossref","unstructured":"Barrett, C., Dill, D. & Stump, A. (2002), A generalization of Shostak\u2019s method for combining decision procedures, in \u2018Proc. FroCos 2002\u2019, Springer-Verlag. to appear.","DOI":"10.1007\/3-540-45988-X_11"},{"key":"28_CR6","unstructured":"Bj\u00f8rner, N. (1998), Integrating decision procedures for temporal verification, PhD thesis, Stanford University."},{"key":"28_CR7","unstructured":"Huet, G. (1972), Constrained Resolution: A Complete Method for Higher Order Logic, PhD thesis, Case Western Reserve University."},{"key":"28_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/3-540-62950-5_59","volume-title":"Rewriting Techniques and Applications","author":"D. Kapur","year":"1997","unstructured":"Kapur, D. (1997), Shostak\u2019s congruence closure as completion, in H. Comon, ed., \u2018Rewriting Techniques and Applications\u2019, Lecture Notes in Computer Science, Springer, Sitges, Spain, pp. 23\u201337."},{"key":"28_CR9","doi-asserted-by":"crossref","unstructured":"Kapur, D. (2002), A rewrite rule based framework for combining decision procedures, in \u2018Proc. FroCos 2002\u2019, Springer-Verlag. to appear.","DOI":"10.1007\/3-540-45988-X_8"},{"key":"28_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"793","DOI":"10.1007\/3-540-59293-8_237","volume-title":"TAPSOFT","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Anuchitanulu, A., Bj\u00f8rner, N., Browne, A., Chang, E. S., Col\u00f3n, M., de Alfaro, L., Devarajan, H., Kapur, A., Lee, J., Sipma, H. & Uribe, T. E. (1995), STeP: The Stanford Temporal Prover, in \u2018TAPSOFT\u2019, Vol. 915 of Lecture Notes in Computer Science, Springer-Verlag, pp. 793\u2013794."},{"issue":"2","key":"28_CR11","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"2","author":"G. Nelson","year":"1979","unstructured":"Nelson, G. & Oppen, D. C. (1979), \u2018Simplification by cooperating decision procedures\u2019, ACM Transactions on Programming Languages and Systems\n                           2(2), 245\u2013257.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"4","key":"28_CR12","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1006\/jsco.1995.1020","volume":"19","author":"R. Nieuwenhuis","year":"1995","unstructured":"Nieuwenhuis, R. & Rubio, A. (1995), \u2018Theorem proving with ordering and equality constrained clauses\u2019, J. Symbolic Computation\n                           19(4), 321\u2013352.","journal-title":"J. Symbolic Computation"},{"key":"28_CR13","series-title":"LNAI","first-page":"748","volume-title":"11th International Conference on Automated Deduction","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J. M. & Shankar, N. (1992), PVS: A prototype verification system, in D. Kapur, ed., \u201811th International Conference on Automated Deduction\u2019, LNAI 607, Springer-Verlag, Saratoga Springs, New York, USA, pp. 748\u2013752."},{"key":"28_CR14","unstructured":"Rue\u00df, H. & Shankar, N. (2001), Deconstructing Shostak, in \u2018Proceedings of the Sixteenth IEEE Symposium On Logic In Computer Science (LICS\u201901)\u2019, IEEE Computer Society Press, pp. 19\u201328."},{"key":"28_CR15","series-title":"Lect Notes Comput Sci","volume-title":"Proc. RTA 2002","author":"N. Shankar","year":"2002","unstructured":"Shankar, N. & Rue\u00df, H. (2002), Combining Shostak theories, in \u2018Proc. RTA 2002\u2019, Lecture Notes in Computer Science, Springer-Verlag. to appear."},{"issue":"1","key":"28_CR16","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R. E. Shostak","year":"1984","unstructured":"Shostak, R. E. (1984), \u2018Deciding combinations of theories\u2019, J. Association for Computing Machinery\n                           31(1), 1\u201312.","journal-title":"J. Association for Computing Machinery"},{"key":"28_CR17","doi-asserted-by":"crossref","unstructured":"Tinelli, C. & Harandi, M. (1996), A new correctness proof of the Nelson-Oppen combination procedure, in \u20181st Int\u2019l Workshop on Frontiers of Combining Systems (FroCoS\u201996)\u2019, Vol. 3 of Applied Logic Series, Kluwer Academic Publishers.","DOI":"10.1007\/978-94-009-0349-4_5"},{"key":"28_CR18","unstructured":"Tiwari, A. (2000), Decision procedures in automated deduction, PhD thesis, SUNY at Stony Brook."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-18"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45620-1_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T20:53:12Z","timestamp":1558471992000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_28","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]},"assertion":[{"value":"4 July 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}