{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T12:24:07Z","timestamp":1754396647098,"version":"3.37.3"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2018,12,17]],"date-time":"2018-12-17T00:00:00Z","timestamp":1545004800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"ForrestHunt Inc."}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2020,3]]},"DOI":"10.1007\/s10817-018-09505-9","type":"journal-article","created":{"date-parts":[[2018,12,17]],"date-time":"2018-12-17T12:12:56Z","timestamp":1545048776000},"page":"391-422","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Limited Second-Order Functionality in a First-Order Setting"],"prefix":"10.1007","volume":"64","author":[{"given":"Matt","family":"Kaufmann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9628-1702","authenticated-orcid":false,"given":"J Strother","family":"Moore","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,12,17]]},"reference":[{"issue":"4","key":"9505_CR1","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1016\/j.jal.2005.10.002","volume":"4","author":"PB Andrews","year":"2006","unstructured":"Andrews, P.B., Brown, C.E.: TPS: a hybrid automatic-interactive system for developing proofs. J. Appl. Log. 4(4), 367\u2013395 (2006)","journal-title":"J. Appl. Log."},{"key":"9505_CR2","unstructured":"Beeson, M.: Otter-lambda, a theorem-prover with untyped lambda-unification. In: Sutcliffe, G., Schulz, S., Tammet, T. (eds.) Proceedings of the ESFOR Workshop at IJCAR 2004 (2004)"},{"issue":"4","key":"9505_CR3","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/s10817-015-9348-y","volume":"55","author":"C Benzm\u00fcller","year":"2015","unstructured":"Benzm\u00fcller, C., Sultana, N., Paulson, L.C., Thei\u00df, F.: The higher-order prover LEO-II. J. Autom. Reason. 55(4), 389\u2013404 (2015)","journal-title":"J. Autom. Reason."},{"key":"9505_CR4","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2010","unstructured":"Bertot, Y., Castran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions, 1st edn. Springer, Berlin (2010)","edition":"1"},{"issue":"1","key":"9505_CR5","first-page":"101","volume":"9","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formaliz. Reason. 9(1), 101\u2013148 (2016)","journal-title":"J. Formaliz. Reason."},{"issue":"2","key":"9505_CR6","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF00244392","volume":"4","author":"R Boyer","year":"1988","unstructured":"Boyer, R., Moore, J.S.: The addition of bounded quantification and partial functions to a computational logic and its theorem prover. J. Autom. Reason. 4(2), 117\u2013172 (1988)","journal-title":"J. Autom. Reason."},{"key":"9505_CR7","volume-title":"A Computational Logic Handbook","author":"RS Boyer","year":"1997","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic Handbook, 2nd edn. Academic Press, New York (1997)","edition":"2"},{"key":"9505_CR8","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1016\/B978-0-12-450010-5.50007-4","volume-title":"Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy","author":"RS Boyer","year":"1991","unstructured":"Boyer, R.S., Goldschlag, D.M., Kaufmann, M., Moore, J.S.: Functional instantiation in first-order logic. In: Lifschitz, V. (ed.) Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pp. 7\u201326. Academic Press, London (1991)"},{"issue":"4","key":"9505_CR9","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/s10817-007-9095-9","volume":"40","author":"B Brock","year":"2008","unstructured":"Brock, B., Kaufmann, M., Moore, J.S.: Rewriting with equivalence relations in ACL2. J. Autom. Reason. 40(4), 293\u2013306 (2008)","journal-title":"J. Autom. Reason."},{"key":"9505_CR10","doi-asserted-by":"crossref","unstructured":"Brown, C.E.: Satallax: an automatic higher-order prover. In: Automated Reasoning: 6th International Joint Conference, IJCAR 2012, Manchester, UK, 26\u201329 June 2012. Proceedings, pp. 111\u2013117 (2012)","DOI":"10.1007\/978-3-642-31365-3_11"},{"key":"9505_CR11","doi-asserted-by":"publisher","first-page":"27","DOI":"10.4204\/EPTCS.152.3","volume":"152","author":"Harsh Raju Chamarthi","year":"2014","unstructured":"Chamarthi, H., Dillinger, P.C., Manolios, P.: Data definitions in the ACL2 sedan. In: ACL2 \u201914, pp. 27\u201348. EPTCS (2014)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"9505_CR12","doi-asserted-by":"crossref","unstructured":"Goel, S., Hunt, W.A., Kaufmann, M.: Simulation and formal verification of x86 machine-code programs that make system calls. In: Claessen, K., Kuncak, V. (eds.) FMCAD\u201914: Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design, pp. 91\u201398. EPFL, Switzerland (2014)","DOI":"10.1109\/FMCAD.2014.6987600"},{"key":"9505_CR13","unstructured":"Goel, S.: Formal verification of application and system programs based on a validated x86 ISA model. Ph.D. thesis, University of Texas at Austin (2016)"},{"issue":"4","key":"9505_CR14","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1093\/comjnl\/22.4.376","volume":"22","author":"MJC Gordon","year":"1979","unstructured":"Gordon, M.J.C.: On the power of list iteration. Comput. J. 22(4), 376\u2013379 (1979)","journal-title":"Comput. J."},{"volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","year":"1993","key":"9505_CR15","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, New York (1993)"},{"issue":"01","key":"9505_CR16","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1017\/S0956796807006338","volume":"18","author":"D Greve","year":"2008","unstructured":"Greve, D., Kaufmann, M., Manolios, P., Moore, J.S., Ray, S., Ruiz-Reina, J.L., Sumners, R., Vroon, D., Wilding, M.: Efficient execution in an automated reasoning environment. J. Funct. Program. 18(01), 15\u201346 (2008)","journal-title":"J. Funct. Program."},{"issue":"2104","key":"9505_CR17","doi-asserted-by":"publisher","first-page":"20150399","DOI":"10.1098\/rsta.2015.0399","volume":"375","author":"Warren A. Hunt","year":"2017","unstructured":"Hunt Jr., W.A., Kaufmann, M., Moore, J.S., Slobodova, A.: Industrial hardware and software verification with ACL2. In: Gardner, P., O\u2019Hearn, P., Gordon, M., Morrisett, G., Schneider, F.B. (eds.) Verified Trustworthy Software Systems. Philosophical Transactions A, vol. 374. Royal Society Publishing (2017). \nhttps:\/\/doi.org\/10.1098\/rsta.2015.0399","journal-title":"Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences"},{"key":"9505_CR18","unstructured":"Kaufmann, M.: Trusted extension of ACL2 system code: towards an open architecture. In: Workshop on Trusted Extensions of Interactive Theorem Provers (2010). See \nhttps:\/\/urldefense.proofpoint.com\/v2\/url?u=http-3A__www.cs.utexas.edu_users_&d=DwIBAg&c=vh6FgFnduejNhPPD0fl_yRaSfZy8CWbWnIf4XJhSqx8&r=r2aSgYn6PHMQXXmeBiKsnvfFG9T9U5fmdQ67xEVmgo0&m=vRrFUnX1Q3Fr5E71n8Ud63k_ILtVVBNdQNbV_UAOm4E&s=NXMiBg4nq_C3pnEnk6Tdql75ei8JA-JX02usDOKVdmM&e=kaufmann\/itp-trusted-extensions-aug-2010\/\n\n. Accessed 2018"},{"key":"9505_CR19","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-4449-4","volume-title":"Computer-Aided Reasoning: An Approach","author":"M Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Press, Boston (2000)"},{"key":"9505_CR20","unstructured":"Kaufmann, M., Moore, J.S.: The ACL2 home page. In: Department of Computer Sciences, University of Texas at Austin (2018). \nhttps:\/\/urldefense.proofpoint.com\/v2\/url?u=http-3A__www.cs.utexas.edu_users_moore_acl2_&d=DwIBAg&c=vh6FgFnduejNhPPD0fl_yRaSfZy8CWbWnIf4XJhSqx8&r=r2aSgYn6PHMQXXmeBiKsnvfFG9T9U5fmdQ67xEVmgo0&m=vRrFUnX1Q3Fr5E71n8Ud63k_ILtVVBNdQNbV_UAOm4E&s=gWfwZpi-faeBogx3pJCo6I5MQjZlJlpVPXbBI0MGPUQ&e=\n\n. Accessed 2018"},{"key":"9505_CR21","unstructured":"Kaufmann, M., Moore, J.S.: ACL2 User Community: ACL2 sources and ACL2 community books on GitHub. In: GitHub (2018). \nhttps:\/\/urldefense.proofpoint.com\/v2\/url?u=https-3A__github.com_acl2_acl2&d=DwIBAg&c=vh6FgFnduejNhPPD0fl_yRaSfZy8CWbWnIf4XJhSqx8&r=r2aSgYn6PHMQXXmeBiKsnvfFG9T9U5fmdQ67xEVmgo0&m=vRrFUnX1Q3Fr5E71n8Ud63k_ILtVVBNdQNbV_UAOm4E&s=NrpdCC6fmnRh_I8oVVLD24qw6YElaOcVQiS7xqUk3eg&e=\n\n. Accessed 2018"},{"key":"9505_CR22","doi-asserted-by":"crossref","unstructured":"Kun\u010dar, O.: Correctness of Isabelle\u2019s cyclicity checker: implementability of overloading in proof assistants. In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP \u201915, pp. 85\u201394, New York, NY, USA. ACM (2015)","DOI":"10.1145\/2676724.2693175"},{"issue":"4","key":"9505_CR23","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1145\/367177.367199","volume":"3","author":"J McCarthy","year":"1960","unstructured":"McCarthy, J.: Recursive functions of symbolic expressions and their computation by machine (part I). CACM 3(4), 184\u2013195 (1960)","journal-title":"CACM"},{"key":"9505_CR24","unstructured":"McCune, W.: Otter 3.0 reference manual and guide. Technical report ANL-94\/6, Argonne National Laboratory, Argonne, IL (1994). See also \nhttps:\/\/urldefense.proofpoint.com\/v2\/url?u=http-3A__www.mcs.anl.gov_AR_otter_&d=DwIBAg&c=vh6FgFnduejNhPPD0fl_yRaSfZy8CWbWnIf4XJhSqx8&r=r2aSgYn6PHMQXXmeBiKsnvfFG9T9U5fmdQ67xEVmgo0&m=vRrFUnX1Q3Fr5E71n8Ud63k_ILtVVBNdQNbV_UAOm4E&s=bQ9nItKqAZKGDoFo__COKKQuPtL-9Qhqa7CZa4HLPgg&e=\n\n. Accessed 2018"},{"issue":"1","key":"9505_CR25","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/s10817-007-9085-y","volume":"40","author":"J Meng","year":"2008","unstructured":"Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Autom. Reason. 40(1), 35\u201360 (2008)","journal-title":"J. Autom. Reason."},{"issue":"7","key":"9505_CR26","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1016\/j.jlap.2012.06.003","volume":"81","author":"J Meseguer","year":"2012","unstructured":"Meseguer, J.: Twenty years of rewriting logic. J. Log. Algebr. Program. 81(7), 721\u2013781 (2012)","journal-title":"J. Log. Algebr. Program."},{"key":"9505_CR27","volume-title":"ML for the Working Programmer","author":"LC Paulson","year":"1991","unstructured":"Paulson, L.C.: ML for the Working Programmer. Cambridge University Press, New York (1991)"},{"key":"9505_CR28","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover. LNCS 828","author":"LC Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle: A Generic Theorem Prover. LNCS 828. Springer, Berlin (1994)"},{"key":"9505_CR29","unstructured":"Pitman, K.: The common lisp HyperSpec. See \nhttps:\/\/urldefense.proofpoint.com\/v2\/url?u=http-3A__www.lispworks.com_documentation_common-2Dlisp&d=DwIBAg&c=vh6FgFnduejNhPPD0fl_yRaSfZy8CWbWnIf4XJhSqx8&r=r2aSgYn6PHMQXXmeBiKsnvfFG9T9U5fmdQ67xEVmgo0&m=vRrFUnX1Q3Fr5E71n8Ud63k_ILtVVBNdQNbV_UAOm4E&s=_Wd_KHgA45uc-8RythKrUZF9qgc-wNTUA3k7JyZh1zE&e=.html\n\n. Accessed 2018"},{"issue":"4","key":"9505_CR30","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1023\/A:1010027404223","volume":"11","author":"JC Reynolds","year":"1998","unstructured":"Reynolds, J.C.: Definitional interpreters for higher-order programming languages. High. Order Symbol. Comput. 11(4), 363\u2013397 (1998)","journal-title":"High. Order Symbol. Comput."},{"key":"9505_CR31","volume-title":"Common Lisp the Language","author":"GL Steele Jr","year":"1990","unstructured":"Steele Jr., G.L.: Common Lisp the Language, 2nd edn. Digital Press, Burlington (1990)","edition":"2"},{"key":"9505_CR32","unstructured":"The Haskell home page. \nhttps:\/\/urldefense.proofpoint.com\/v2\/url?u=https-3A__www.haskell.org&d=DwIBAg&c=vh6FgFnduejNhPPD0fl_yRaSfZy8CWbWnIf4XJhSqx8&r=r2aSgYn6PHMQXXmeBiKsnvfFG9T9U5fmdQ67xEVmgo0&m=vRrFUnX1Q3Fr5E71n8Ud63k_ILtVVBNdQNbV_UAOm4E&s=MIT0gLXrGfuoJ3pMHEAFlrqshodFFiClh_eQ8wpP7FA&e=\n\n. Accessed 2018"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-09505-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-09505-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-09505-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,2,29]],"date-time":"2020-02-29T04:03:26Z","timestamp":1582949006000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-09505-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,12,17]]},"references-count":32,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,3]]}},"alternative-id":["9505"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-09505-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2018,12,17]]},"assertion":[{"value":"22 October 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 December 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 December 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}