{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:18Z","timestamp":1761611118514,"version":"3.41.0"},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2001,2,1]],"date-time":"2001-02-01T00:00:00Z","timestamp":980985600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2001,2,1]],"date-time":"2001-02-01T00:00:00Z","timestamp":980985600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[2001,2]]},"DOI":"10.1023\/a:1026517200045","type":"journal-article","created":{"date-parts":[[2003,11,6]],"date-time":"2003-11-06T17:11:16Z","timestamp":1068138676000},"page":"161-203","source":"Crossref","is-referenced-by-count":45,"title":["Structured Theory Development for a Mechanized Logic"],"prefix":"10.1007","volume":"26","author":[{"given":"Matt","family":"Kaufmann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J Strother","family":"Moore","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"268567_CR1","volume-title":"A Computational Logic","author":"R. S. Boyer","year":"1979","unstructured":"Boyer, R. S. and Moore, J S.: A Computational Logic, Academic Press, New York, 1979."},{"key":"268567_CR2","doi-asserted-by":"crossref","unstructured":"Boyer, R. S., Goldschlag, D., Kaufmann, M. and Moore, J S.: Functional instantiation in first order logic, in Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, Academic Press, 1991, pp. 7\u201326.","DOI":"10.1016\/B978-0-12-450010-5.50007-4"},{"issue":"2","key":"268567_CR3","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0898-1221(94)00215-7","volume":"5","author":"R. S. Boyer","year":"1995","unstructured":"Boyer, R. S., Kaufmann, M. and Moore, J S.: The Boyer-Moore theorem prover and its interactive enhancement, Comput. Math. Appl.\n5(2) (1995), 27\u201362.","journal-title":"Comput. Math. Appl."},{"key":"268567_CR4","doi-asserted-by":"crossref","unstructured":"Brock, B., Kaufmann, M. and Moore, J S.: ACL2 theorems about commercial microprocessors, in M. Srivas and A. Camilleri (eds.), Proceedings of Formal Methods in Computer-Aided Design (FMCAD'96), Springer-Verlag, November 1996, pp. 275\u2013293.","DOI":"10.1007\/BFb0031816"},{"key":"268567_CR5","volume-title":"A Computational Logic Handbook","author":"R. S. Boyer","year":"1997","unstructured":"Boyer, R. S. and Moore, J S.: A Computational Logic Handbook, 2nd edn, Academic Press, London, 1997.","edition":"2nd edn"},{"key":"268567_CR6","unstructured":"Brock, B. and Moore, J S.: A mechanically checked proof of a comparator sort algorithm, URL http:\/\/www.cs.utexas.edu\/users\/moore\/publications\/csort\/main.ps.Z (submitted for publication), 1999."},{"key":"268567_CR7","unstructured":"Gamboa, R. and Kaufmann, M.: Non-standard analysis in ACL2, in preparation. See also R. Gamboa's Ph.D. dissertation at URL http:\/\/www.lim.com\/~ruben\/research\/thesis\/ web\/index.html."},{"key":"268567_CR8","unstructured":"Greve, D. A., Hardin, D. S. and Wilding, M. M.: Efficient simulation using a simple formal processor model, Technical Report, Advanced Technology Center, Rockwell Collins Avionics and Communications, Cedar Rapids, IA 52498, April, 1998."},{"key":"268567_CR9","unstructured":"Kaufmann, M. and Moore, J S.: ACL2: A Computational Logic for Applicative Common Lisp, the user's manual, URL: http:\/\/www.cs.utexas.edu\/users\/moore\/acl2."},{"key":"268567_CR10","unstructured":"Kaufmann, M. and Moore, J S.: High-level correctness of ACL2: A story, URL http:\/\/www.-cs.utexas.edu\/users\/moore\/publications\/story.txt, October, 1995."},{"key":"268567_CR11","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P. and Moore, J S.: Computer-Aided Reasoning: An Approach, Kluwer Academic Publishers, 2000.","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"268567_CR12","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P. and Moore, J S. (eds.): Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Publishers, 2000.","DOI":"10.1007\/978-1-4757-3188-0"},{"key":"268567_CR13","unstructured":"Kaufmann, M. and Moore, J S.: A precise description of the ACL2 logic, URL http:\/\/www.-cs.utexas.edu\/users\/moore\/acl2\/reports\/km97a.ps.Z."},{"key":"268567_CR14","doi-asserted-by":"crossref","unstructured":"Kaufmann, M. and Moore, J: An industrial strength theorem prover for a logic based on Common Lisp, in IEEE Transactions on Software Engineering 23(4), April 1997, pp. 203\u2013213.","DOI":"10.1109\/32.588534"},{"key":"268567_CR15","doi-asserted-by":"crossref","unstructured":"Kaufmann, M.: ACL2 support for verification projects, in C. Kirchner and H. Kirchner (eds.), Proceedings 15th Int'l Conf. Automated Deduction, Lecture Notes in Artif. Intell. 1421, Springer-Verlag, July 1998, pp. 220\u2013238.","DOI":"10.1007\/BFb0054262"},{"issue":"9","key":"268567_CR16","doi-asserted-by":"crossref","first-page":"913","DOI":"10.1109\/12.713311","volume":"47","author":"J Moore","year":"1998","unstructured":"Moore, J, Lynch, T. and Kaufmann, M.: A mechanically checked proof of the AMD5K86 floating-point division program, IEEE Trans. Comput.\n47(9) (1998), 913\u2013926. See also URL http:\/\/devil.ece.utexas.edu\/~lynch\/divide\/divide.html.","journal-title":"IEEE Trans. Comput."},{"key":"268567_CR17","unstructured":"Russinoff, D.: A mechanically checked proof of correctness of the AMD5K86 floating-point square root microcode, in Formal Methods in System Design. Special Issue on Arithmetic Circuits, 1997."},{"key":"268567_CR18","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1112\/S1461157000000176","volume":"1","author":"D. M. Russinoff","year":"1998","unstructured":"Russinoff, D. M.: A mechanically checked proof of IEEE compliance of the floating point multiplication, division, and square root algorithms of the AMD-K7TM processor, LMS J. Comput. and Math.\n1 (1998), 148\u2013200. See also URL http:\/\/www.onr.com\/user\/russ\/-david\/k7-div-sqrt.html.","journal-title":"LMS J. Comput. and Math."},{"key":"268567_CR19","doi-asserted-by":"crossref","first-page":"1137","DOI":"10.2307\/2275878","volume":"60","author":"J. Schmerl","year":"1995","unstructured":"Schmerl, J.: A reflection principle and its applications to nonstandard models, J. Symbolic Logic\n60 (1995), 1137\u20131152.","journal-title":"J. Symbolic Logic"},{"key":"268567_CR20","volume-title":"Mathematical Logic","author":"J. R. Shoenfield","year":"1967","unstructured":"Shoenfield, J. R.: Mathematical Logic, Addison-Wesley, Reading, MA, 1967."},{"key":"268567_CR21","volume-title":"Common Lisp: The Language","author":"G. L. Steele Jr.","year":"1990","unstructured":"Steele, G. L., Jr.: Common Lisp: The Language, 2nd edn, Digital Press, Burlington, MA, 1990.","edition":"2nd edn"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1026517200045.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1026517200045\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1026517200045.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:43:23Z","timestamp":1749123803000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1026517200045"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,2]]},"references-count":21,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2001,2]]}},"alternative-id":["268567"],"URL":"https:\/\/doi.org\/10.1023\/a:1026517200045","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2001,2]]}}}