{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:24:10Z","timestamp":1725560650770},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540283720"},{"type":"electronic","value":"9783540318200"}],"license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11541868_11","type":"book-chapter","created":{"date-parts":[[2010,7,20]],"date-time":"2010-07-20T19:12:52Z","timestamp":1279653172000},"page":"163-178","source":"Crossref","is-referenced-by-count":18,"title":["Meta Reasoning in ACL2"],"prefix":"10.1007","author":[{"suffix":"Jr","given":"Warren A.","family":"Hunt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matt","family":"Kaufmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert Bellarmine","family":"Krug","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J Strother","family":"Moore","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eric Whitman","family":"Smith","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","volume-title":"The Correctness Problem in Computer Science","author":"R.S. Boyer","year":"1981","unstructured":"Boyer, R.S., Moore, J.: Metafunctions: proving them correct and using them efficiently as proof procedures. In: Boyer, R.S., Moore, J. (eds.) The Correctness Problem in Computer Science. Academic Press, London (1981)"},{"key":"11_CR2","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"11_CR3","unstructured":"Harrison, J.: Metatheory and Reflection in Theorem Proving: A Survey and Critique"},{"volume-title":"Computer-Aided Reasoning: An Approach","year":"2000","key":"11_CR4","unstructured":"Kaufmann, M., Manolios, P., Moore, J. (eds.): Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Dordrecht (2000)"},{"volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","year":"2000","key":"11_CR5","unstructured":"Kaufmann, M., Manolios, P., Moore, J. (eds.): Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"11_CR6","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1109\/CMPASS.1996.507872","volume-title":"Proceedings of the Eleventh Annual Conference on Computer Assurance (COMPASS 1996)","author":"M. Kaufmann","year":"1996","unstructured":"Kaufmann, M., Moore, J.: ACL2: An Industrial Strength Version of Nqthm. In: Proceedings of the Eleventh Annual Conference on Computer Assurance (COMPASS 1996), pp. 23\u201334. IEEE Computer Society Press, Los Alamitos (1996)"},{"key":"11_CR7","unstructured":"Smith, E., Nelesen, S., Greve, D., Wilding, M., Richards, R.: An ACL2 Library for Bags (MultiSets). In: Fifth International ACL2 workshop (2004), \n                    \n                      http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2004\/index.html"},{"key":"11_CR8","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"1999","unstructured":"Wenzel, M.: Isar \u2014 a Generic Interpretive Approach to Readable Formal Proof Documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999, vol.\u00a01690, p. 167. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11541868_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,29]],"date-time":"2020-01-29T21:50:53Z","timestamp":1580334653000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11541868_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540283720","9783540318200"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/11541868_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}