{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T21:40:40Z","timestamp":1648590040526},"reference-count":13,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2003,5,1]],"date-time":"2003-05-01T00:00:00Z","timestamp":1051747200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3742,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,5]]},"DOI":"10.1016\/s1571-0661(04)80657-1","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T16:47:47Z","timestamp":1096476467000},"page":"120-132","source":"Crossref","is-referenced-by-count":0,"title":["Canonicity1 1This research was supported in part by the Israel Science Foundation (grant no. 254\/01)."],"prefix":"10.1016","volume":"86","author":[{"given":"Nachum","family":"Dershowitz","sequence":"first","affiliation":[]}],"member":"78","reference":[{"issue":"2","key":"10.1016\/S1571-0661(04)80657-1_NEWBIB1","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/174652.174655","article-title":"Equational inference, canonical proofs, and proof orderings","volume":"41","author":"Leo","year":"1994","journal-title":"J. of the Association for Computing Machinery"},{"key":"10.1016\/S1571-0661(04)80657-1_NEWBIB2","doi-asserted-by":"crossref","unstructured":"Leo Bachmair and Harald Ganzinger. Completion of first-order clauses with equality by strict superposition (Extended abstract). In M. Okada and S. Kaplan, editors, Proceedings of the Second International Workshop on Conditional and Typed Rewriting Systems (Montreal, Canada), volume 516 of Lecture Notes in Computer Science, pages 162\u2013180, Berlin, June 1990. Springer-Verlag.","DOI":"10.1007\/3-540-54317-1_89"},{"key":"10.1016\/S1571-0661(04)80657-1_NEWBIB3","series-title":"Handbook of Automated Reasoning, volume I, chapter 2","first-page":"19","article-title":"Resolution theorem proving","author":"Leo","year":"2001"},{"key":"10.1016\/S1571-0661(04)80657-1_NEWBIB4","unstructured":"Maria Paola Bonacina. Distributed automated deduction. PhD thesis, Department of Computer Science, State University of New York at Stony Brook, December 1992."},{"key":"10.1016\/S1571-0661(04)80657-1_NEWBIB5","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1016\/0304-3975(94)00187-N","article-title":"Towards a foundation of completion procedures as semidecision procedures","volume":"146","author":"Bonacina","year":"1995","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"10.1016\/S1571-0661(04)80657-1_NEWBIB6","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","article-title":"Orderings for term-rewriting systems","volume":"17","author":"Nachum","year":"1982","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80657-1_NEWBIB7","doi-asserted-by":"crossref","unstructured":"Nachum Dershowitz. A maximal-literal unit strategy for Horn clauses. In S. Kaplan and M. Okada, editors, Proceedings of the Second International Workshop on Conditional and Typed Rewriting Systems (Montreal, Canada, June 1990), volume 516 of Lecture Notes in Computer Science, pages 14\u201325, Berlin, 1991. Springer-Verlag.","DOI":"10.1007\/3-540-54317-1_78"},{"key":"10.1016\/S1571-0661(04)80657-1_NEWBIB8","doi-asserted-by":"crossref","unstructured":"Nachum Dershowitz and Claude Kirchner. Abstract saturation-based inference. In Proceedings of the 18th Annual Symposium on Logic in Computer Science, Ottawa, June 2003. IEEE Computer Society Press.","DOI":"10.1109\/LICS.2003.1210046"},{"key":"10.1016\/S1571-0661(04)80657-1_NEWBIB9","series-title":"Handbook of Automated Reasoning, volume I, chapter 9","first-page":"535","article-title":"Rewriting","author":"Nachum","year":"2001"},{"key":"10.1016\/S1571-0661(04)80657-1_NEWBIB10","series-title":"Handbook of Automated Reasoning, volume I, chapter 7","first-page":"371","article-title":"Paramodulation-based theorem proving","author":"Robert","year":"2001"},{"key":"10.1016\/S1571-0661(04)80657-1_NEWBIB11","unstructured":"Micha\u00ebl Rusinowitch. D\u00e9monstration Automatique: Techniques de R\u00e9\u00e9criture. Science Informatique. InterEditions, Paris, 1989."},{"key":"10.1016\/S1571-0661(04)80657-1_NEWBIB12","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1016\/S0747-7171(08)80131-9","article-title":"Theorem-proving with resolution and superposition","volume":"11","author":"Micha\u00ebl","year":"1991","journal-title":"J. Symbolic Computation"},{"key":"10.1016\/S1571-0661(04)80657-1_NEWBIB13","unstructured":"\u201cTerese\u201d (M. Bezem, J. W. Klop and R. de Vrijer, eds.). Term Rewriting Systems. Cambridge University Press, 2003."}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104806571?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104806571?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,2,3]],"date-time":"2019-02-03T10:53:07Z","timestamp":1549191187000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104806571"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,5]]},"references-count":13,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,5]]}},"alternative-id":["S1571066104806571"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80657-1","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,5]]}}}