{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:35:10Z","timestamp":1759638910634,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439318"},{"type":"electronic","value":"9783540456209"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45620-1_29","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T07:18:26Z","timestamp":1186903106000},"page":"347-362","source":"Crossref","is-referenced-by-count":13,"title":["Formal Verification of a Combination Decision Procedure"],"prefix":"10.1007","author":[{"given":"Jonathan","family":"Ford","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natarajan","family":"Shankar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"29_CR1","volume-title":"A Computational Logic","author":"R. S. Boyer","year":"1979","unstructured":"R. S. Boyer and J. S. Moore. A Computational Logic. Academic Press, New York, NY, 1979."},{"key":"29_CR2","volume-title":"The Correctness Problem in Computer Science","author":"R. S. Boyer","year":"1981","unstructured":"R. S. Boyer and J. S. Moore. Metafunctions: Proving them correct and using them efficiently as new proof procedures. In R. S. Boyer and J. S. Moore, editors, The Correctness Problem in Computer Science. Academic Press, London, 1981."},{"key":"29_CR3","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"},{"key":"29_CR4","unstructured":"J. Ford and I. A. Mason. Establishing a General Context Lemma in PVS. In Proceedings of the 2nd Australasian Workshop on Computational Logic, AWCL\u201901, 2001. submitted."},{"key":"29_CR5","doi-asserted-by":"crossref","unstructured":"J. Ford and I. A. Mason. Operational techniques in PVS\u2014a preliminary evaluation. In Proceedings of the Australasian Theory Symposium, CATS\u2019 01, Gold Coast, Queensland, Australia, January-February 2001.","DOI":"10.1016\/S1571-0661(04)80882-X"},{"key":"29_CR6","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":"29_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanized Logic of Computation","author":"M. Gordon","year":"1979","unstructured":"M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979."},{"issue":"2","key":"29_CR8","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"},{"key":"29_CR9","doi-asserted-by":"crossref","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.","DOI":"10.1007\/3-540-55602-8_217"},{"key":"29_CR10","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"},{"issue":"4","key":"29_CR11","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/BF00244278","volume":"1","author":"N. Shankar","year":"1985","unstructured":"N. Shankar. Towards mechanical metamathematics. Journal of Automated Reasoning, 1(4):407\u2013434, 1985.","journal-title":"Journal of Automated Reasoning"},{"key":"29_CR12","volume-title":"Project report","author":"N. Shankar","year":"1999","unstructured":"N. Shankar. Efficiently executing PVS. Project report, Computer Science Laboratory, SRI International, Menlo Park, CA, November 1999. Available at http:\/\/www.csl.sri.com\/shankar\/PVSeval.ps.gz ."},{"key":"29_CR13","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":"29_CR14","doi-asserted-by":"crossref","unstructured":"Laurent Th\u00e9ry. A certified version of Buchberger\u2019s algorithm. In H. Kirchner and C. Kirchner, editors, Proceedings of CADE-15, number 1421 in Lecture Notes in Artificial Intelligence, pages 349\u2013364, Berlin, Germany, July 1998. Springer-Verlag.","DOI":"10.1007\/BFb0054271"},{"key":"29_CR15","volume-title":"Technical Report 3859","author":"K.N. Verma","year":"2000","unstructured":"K.N. Verma and J. Goubault-Larrecq. Reflecting BDDs in Coq. Technical Report 3859, INRIA, Rocquencourt, France, January 2000."},{"key":"29_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/BFb0055152","volume-title":"Proc. Intl. Conf. on Theorem Proving in Higher Order Logics","author":"F. W. Henke von","year":"1998","unstructured":"F. W. von Henke, S. Pfab, H. Pfeifer, and H. Rue\u00df. Case studies in meta-level theorem proving. In Jim Grundy and Malcolm Newey, editors, Proc. Intl. Conf. on Theorem Proving in Higher Order Logics, number 1479 in Lecture Notes in Computer Science, pages 461\u2013478. Springer-Verlag, September 1998."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-18"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45620-1_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T08:51:47Z","timestamp":1737363107000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_29","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}