{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:32Z","timestamp":1760202632720,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615118"},{"type":"electronic","value":"9783540686873"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61511-3_107","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:51:05Z","timestamp":1330293065000},"page":"463-477","source":"Crossref","is-referenced-by-count":31,"title":["On Shostak's decision procedure for combinations of theories"],"prefix":"10.1007","author":[{"given":"David","family":"Cyrluk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patrick","family":"Lincoln","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natarajan","family":"Shankar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,4]]},"reference":[{"key":"44_CR1","volume-title":"A Computational Logic Handbook","author":"R. S. Boyer","year":"1988","unstructured":"R. S. Boyer and J S. Moore. A Computational Logic Handbook. Academic Press, New York, NY, 1988."},{"key":"44_CR2","unstructured":"User Guide for theEhdmSpecification Language and Verification System, Version 6.1. Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993. Three volumes."},{"key":"44_CR3","unstructured":"Jeffrey V. Cook, Ivan V. Filippenko, Beth H. Levy, Leo G. Marcus, and Telis K. Menas. Formal computer verification in the state delta verification system (SDVS). In AIAA Computing in Aerospace VIII, pages 77\u201387, Baltimore, MD, October 1991. AIAA paper 91-3715."},{"key":"44_CR4","series-title":"volume 551 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/3-540-54834-3_24","volume-title":"VDM '91: Formal Software Development Methods","author":"D. Craigen","year":"1991","unstructured":"Dan Craigen, Sentot Kromodimoeljo, Irwin Meisels, Bill Pase, and Mark Saaltink. EVES: An overview. InPrehn and Toetenel [15]., pages 389\u2013405."},{"key":"44_CR5","unstructured":"S. Crocker. Comparison of Shostak's and Oppen's solvers. Unpublished manuscript, 1988."},{"issue":"4","key":"44_CR6","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, October 1980.","journal-title":"Journal of the ACM"},{"key":"44_CR7","doi-asserted-by":"crossref","unstructured":"D. Kozen. Complexity of finitely represented algebras. In Proc. 9th ACM STOC, pages 164\u2013177, 1988.","DOI":"10.1145\/800105.803406"},{"key":"44_CR8","volume-title":"CSD Report STAN-CS-79-731","author":"D. C. Luckham","year":"1979","unstructured":"D. C. Luckham, S. M. German, F. W. von Henke, R. A. Karp, P. W. Milne, D. C. Oppen, W. Polak, and W. L. Scherlis. Stanford Pascal Verifier user manual. CSD Report STAN-CS-79-731, Stanford University, Stanford, CA, March 1979."},{"key":"44_CR9","volume-title":"ONTIC: A Knowledge Representation System for Mathematics","author":"D. A. McAllester","year":"1989","unstructured":"David A. McAllester. ONTIC: A Knowledge Representation System for Mathematics. MIT Press, Cambridge, MA, 1989."},{"issue":"2","key":"44_CR10","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":"44_CR11","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":"44_CR12","volume-title":"Technical Report csl-81-10","author":"G. Nelson","year":"1981","unstructured":"Greg Nelson. Techniques for program verification. Technical Report csl-81-10, Xerox Palo Alto Research Center, Palo Alto, CA, June 1981."},{"key":"44_CR13","first-page":"748","volume-title":"volume 607 of Lecture Notes in Artificial Intelligence","author":"S. Owre","year":"1992","unstructured":"S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748\u2013752, Saratoga, NY, June 1992. Springer-Verlag."},{"issue":"2","key":"44_CR14","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, February 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"44_CR15","series-title":"volume 551 of Lecture Notes in Computer Science","volume-title":"VDM '91: Formal Software Development Methods","year":"1991","unstructured":"S. Prehn and W. J. Toetenel, editors. VDM '91: Formal Software Development Methods, volume 551 of Lecture Notes in Computer Science, Noordwijkerhout, The Netherlands, October 1991. Springer-Verlag. Volume 1: Conference Contributions."},{"key":"44_CR16","volume-title":"Technical Report SRI-CSL-89-3R","author":"J. Rushby","year":"1989","unstructured":"John Rushby and Friedrich von Henke. Formal verification of the Interactive Convergence clock synchronization algorithm using Ehdm. Technical Report SRI-CSL-89-3R, Computer Science Laboratory, SRI International, Menlo Park, CA, February 1989 (Revised August 1991). Original version also available as NASA Contractor Report 4239, June 1989."},{"issue":"7","key":"44_CR17","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1145\/359545.359570","volume":"21","author":"R. E. Shostak","year":"1978","unstructured":"Robert E. Shostak. An algorithm for reasoning about equality. Communications of the ACM, 21(7):583\u2013585, July 1978.","journal-title":"Communications of the ACM"},{"issue":"1","key":"44_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R. E. Shostak","year":"1984","unstructured":"Robert E. Shostak. Deciding combinations of theories. Journal of the ACM, 31(1):1\u201312, January 1984.","journal-title":"Journal of the ACM"},{"key":"44_CR19","volume-title":"Technical Report 132","author":"R. E. Shostak","year":"1984","unstructured":"Robert E. Shostak. Deciding combinations of theories. Technical Report 132, SRI-CSL, Menlo Park, CA, January 1984."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 Cade-13"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61511-3_107.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:20:43Z","timestamp":1742599243000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61511-3_107"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615118","9783540686873"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-61511-3_107","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}