{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T12:45:08Z","timestamp":1649076308896},"reference-count":12,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2008,1,15]],"date-time":"2008-01-15T00:00:00Z","timestamp":1200355200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2008,5]]},"DOI":"10.1007\/s10817-007-9095-9","type":"journal-article","created":{"date-parts":[[2008,1,14]],"date-time":"2008-01-14T10:17:34Z","timestamp":1200305854000},"page":"293-306","source":"Crossref","is-referenced-by-count":6,"title":["Rewriting with Equivalence Relations in ACL2"],"prefix":"10.1007","volume":"40","author":[{"given":"Bishop","family":"Brock","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matt","family":"Kaufmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J Strother","family":"Moore","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2008,1,15]]},"reference":[{"key":"9095_CR1","doi-asserted-by":"crossref","unstructured":"Boyer, R., Goldschlag, D., 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 (1991)","DOI":"10.1016\/B978-0-12-450010-5.50007-4"},{"key":"9095_CR2","volume-title":"A Computational Logic Handbook","author":"R.S. Boyer","year":"1997","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic Handbook, 2nd edn. Academic Press, New York (1997)","edition":"2"},{"key":"9095_CR3","unstructured":"Brock, B.: An Experimental Implementation of Equivalence Reasoning in the Boyer-Moore Theorem Prover. Internal Note #104, Computational Logic, Inc. (1989)"},{"key":"9095_CR4","doi-asserted-by":"crossref","unstructured":"Greve, D.: Parameterized congruences in ACL2. In: ACM International Conference Proceeding Series, vol. 205. The ACM Digital Libary (2006)","DOI":"10.1145\/1217975.1217981"},{"key":"9095_CR5","doi-asserted-by":"crossref","unstructured":"Grundy, J.: Window inference in the HOL system. In: Archer, M., Joyce, J.J., Levitt, K.N., Windley, P.J. (eds.) Proceedings of the International Workshop on the HOL Theorem Proving System and its Applications, pp. 177\u2013189. IEEE Computer Society Press, University of California at Davis (1991)","DOI":"10.1109\/HOL.1991.596285"},{"key":"9095_CR6","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Theorem Proving with the Real Numbers. Springer-Verlag (1998)","DOI":"10.1007\/978-1-4471-1591-5"},{"key":"9095_CR7","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, MA (2000)"},{"issue":"2","key":"9095_CR8","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1023\/A:1026517200045","volume":"26","author":"M. Kaufmann","year":"2001","unstructured":"Kaufmann, M., Moore, J.S.: Structured theory development for a mechanized logic. J. Autom. Reason. 26(2), 161\u2013203 (2001)","journal-title":"J. Autom. Reason."},{"key":"9095_CR9","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Moore, J.S.: Double rewriting for equivalential reasoning in ACL2. In: ACM International Conference Proceeding Series, vol. 205. The ACM Digital Libary (2006)","DOI":"10.1145\/1217975.1217997"},{"key":"9095_CR10","unstructured":"Kaufmann, M., Moore, J.S.: The ACL2 home page. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/ (2007)"},{"issue":"1","key":"9095_CR11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/4904.4905","volume":"33","author":"Z. Manna","year":"1986","unstructured":"Manna, Z., Waldinger, R.: Special relations in automated deduction. J. ACM 33(1), 1\u201359 (1986)","journal-title":"J. ACM"},{"key":"9095_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-order Logic. Springer-Verlag, London, UK (2002)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-007-9095-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-007-9095-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-007-9095-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T01:21:48Z","timestamp":1559265708000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-007-9095-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,1,15]]},"references-count":12,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2008,5]]}},"alternative-id":["9095"],"URL":"https:\/\/doi.org\/10.1007\/s10817-007-9095-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,1,15]]}}}