{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T05:42:06Z","timestamp":1747546926861},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540420712"},{"type":"electronic","value":"9783540449904"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44990-6_7","type":"book-chapter","created":{"date-parts":[[2007,8,28]],"date-time":"2007-08-28T14:20:43Z","timestamp":1188310843000},"page":"92-106","source":"Crossref","is-referenced-by-count":1,"title":["Formalizing Rewriting in the ACL2 Theorem Prover"],"prefix":"10.1007","author":[{"given":"Jos\u00e9-Luis","family":"Ruiz-Reina","sequence":"first","affiliation":[]},{"given":"Jos\u00e9-Antonio","family":"Alonso","sequence":"additional","affiliation":[]},{"given":"Mar\u00eda-Jos\u00e9","family":"Hidalgo","sequence":"additional","affiliation":[]},{"given":"Francisco-Jes\u00fas","family":"Mart\u00edn-Mateos","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,5,11]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"F. Baader and T. Nipkow. Term rewriting and all that. Cambridge University Press, 1998.","DOI":"10.1017\/CBO9781139172752"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"L. Bachmair. Canonical equational proofs. Birkh\u00fcser, 1991.","DOI":"10.1007\/978-1-4684-7118-2"},{"key":"7_CR3","unstructured":"R. Boyer and J S. Moore. A Computational Logic Handbook. Academic Press, 2nd edition, 1998."},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"B. Buchberger and R. Loos. Algebraic simplification. In Computer Algebra, Symbolic and Algebraic Computation. Computing Supplementum 4. SV, 1982.","DOI":"10.1007\/978-3-7091-3406-1_2"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"G. Huet. Residual theory in \u03bb-calculus: a formal development. Journal of Functional Programming, (4):475\u2013522, 1994.","DOI":"10.1017\/S0956796800001106"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"M. Kaufmann, P. Manolios and J S. Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, 2000.","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"J.W. Klop. Term rewriting systems. Handbook of Logic in Computer Science, Clarendon Press, 1992.","DOI":"10.1007\/3-540-54317-1_79"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"P. Le Chenadec. Canonical forms in finitely presented algebras. Pitman-Wiley, London, 1985.","DOI":"10.1007\/978-0-387-34768-4_9"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"W. McCune and O. Shumsky. Ivy: A preprocessor and proof checker for firstorder logic. In Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Publishers, 2000, ch. 16.","DOI":"10.1007\/978-1-4757-3188-0_16"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"T. Nipkow. More Church-Rosser proofs (in Isabelle\/HOL). In 13th International Conference on Automated Deduction, LNAI 1104, pages 733\u2013747. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61511-3_125"},{"key":"7_CR11","unstructured":"J.L. Ruiz-Reina, J.A. Alonso, M.J. Hidalgo, and F.J. Mart\u00edn. Mechanical verification of a rule based unification algorithm in the Boyer-Moore theorem prover. In AGP'99 Joint Conference on Declarative Programming, pages 289\u2013304, 1999."},{"issue":"3","key":"7_CR12","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1145\/44483.44484","volume":"35","author":"N. Shankar","year":"1988","unstructured":"N. Shankar. A mechanical proof of the Church-Rosser theorem. Journal of the ACM, 35(3):475\u2013522, 1988.","journal-title":"Journal of the ACM"},{"key":"7_CR13","unstructured":"G.L. Steele. Common Lisp the Language, 2nd edition. Digital Press, 1990."}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence and Symbolic Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44990-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T17:07:57Z","timestamp":1556816877000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44990-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540420712","9783540449904"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-44990-6_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}