{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:05:46Z","timestamp":1749125146987},"reference-count":14,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1992,12,1]],"date-time":"1992-12-01T00:00:00Z","timestamp":723168000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[1992,12]]},"DOI":"10.1007\/bf00245295","type":"journal-article","created":{"date-parts":[[2004,11,7]],"date-time":"2004-11-07T23:31:19Z","timestamp":1099870279000},"page":"355-372","source":"Crossref","is-referenced-by-count":11,"title":["An extension of the Boyer-Moore Theorem Prover to support first-order quantification"],"prefix":"10.1007","volume":"9","author":[{"given":"Matt","family":"Kaufmann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","volume-title":"A Computational Logic Handbook","author":"R. S. Boyer","year":"1988","unstructured":"BoyerR. S. and MooreJ S., A Computational Logic Handbook, Academic Press, Boston (1988)."},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"Goldschlag David M., ?Mechanically verifying concurrent programs with the Boyer-Moore prover?, IEEE Transactions on Software Engineering, SE-16(9) (September 1990).","DOI":"10.1109\/32.58787"},{"key":"CR3","doi-asserted-by":"crossref","unstructured":"Goldschlag, David M., ?Proving proof rules: A proof system for concurrent programs?, Compass '90 (June 1990).","DOI":"10.1109\/CMPASS.1990.175405"},{"key":"CR4","unstructured":"Goldschlag, David M., ?Mechanizing Unity?, in: Proceedings of the IFIP TC2 Working Conference on Programming Concepts and Methods, M. Broy and C. B. Jones (Eds.), Elsevier Science Publishers B.V. (1990)."},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"Yu Yuan, ?Computer proofs in group theory?, J. Automated Reasoning, 6(3) (September 1990).","DOI":"10.1007\/BF00244488"},{"key":"CR6","unstructured":"Kaufmann, Matt, ?A user's manual for an interactive enhancement to the Boyer-Moore Theorem Prover?, Tech. Report 19, Computational Logic, Inc. (May 1988)."},{"key":"CR7","unstructured":"Kaufmann, Matt, ?Addition of free variables to an interactive enhancement of the Boyer-Moore Theorem Prover?, Tech. Report 42, Computational Logic, Inc. (May 1989)."},{"key":"CR8","doi-asserted-by":"crossref","first-page":"633","DOI":"10.1145\/6490.6491","volume":"33","author":"D. Champeaux de","year":"1986","unstructured":"deChampeauxD., ?Subproblem finder and instance checker, two cooperating modules for theorem provers?, J. Assoc. Comp. Mach. 33, 633?657 (October 1986).","journal-title":"J. Assoc. Comp. Mach."},{"key":"CR9","unstructured":"Kaufmann, Matt, ?DEFN-SK: An extension of the Boyer-Moore Theorem Prover to handle first-order quantifiers?, Tech. Report 43, Computational Logic, Inc. (May 1989)."},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"McCarthy, J., Abrahams, P. W., Edwards, D. J., Hart, T. P., and Levin, M. I., MIT LISP 1.5 Programmer's Manual, MIT (1962).","DOI":"10.21236\/AD0406138"},{"key":"CR11","volume-title":"Mathematical Logic","author":"J. R. Shoenfield","year":"1967","unstructured":"ShoenfieldJ. R., Mathematical Logic, Addison-Wesley, Reading, Mass. (1967)."},{"key":"CR12","unstructured":"Boyer, Robert S., Goldschlag, David M., Kaufmann, Matt, and Moore, J Strother, ?Functional instantiation in first order logic?, Tech. Report 44, Computational Logic, Inc. (May 1989)."},{"key":"CR13","unstructured":"Ketonen, Jussi, ?EKL ? Ramsey theorem?, Tech. Report, Department of Computer Science, Stanford University (December 1986)."},{"key":"CR14","volume-title":"Set Theory: An Introduction to Independence Proofs","author":"Kenneth Kunen","year":"1980","unstructured":"KunenKenneth, Set Theory: An Introduction to Independence Proofs, North-Holland, New York (1980)."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00245295.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00245295\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00245295","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T21:43:25Z","timestamp":1585950205000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00245295"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,12]]},"references-count":14,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1992,12]]}},"alternative-id":["BF00245295"],"URL":"https:\/\/doi.org\/10.1007\/bf00245295","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992,12]]}}}