{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:48:30Z","timestamp":1762458510558},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540677789"},{"type":"electronic","value":"9783540449805"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10721975_15","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T15:43:04Z","timestamp":1167406984000},"page":"214-228","source":"Crossref","is-referenced-by-count":5,"title":["An Algebra of Resolution"],"prefix":"10.1007","author":[{"given":"Georg","family":"Struth","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-7118-2","volume-title":"Canonical Equational Proofs","author":"L. Bachmair","year":"1991","unstructured":"Bachmair, L.: Canonical Equational Proofs. Birkh\u00e4user, Basel (1991)"},{"key":"15_CR2","series-title":"Rewriting Techniques, ch. 1","first-page":"1","volume-title":"Resolution of Equations in Algebraic Structures","author":"L. Bachmair","year":"1989","unstructured":"Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: A\u00eft-Kacy, H., Nivat, M. (eds.) Resolution of Equations in Algebraic Structures. Rewriting Techniques, ch. 1, vol.\u00a02, pp. 1\u201330. Academic Press, London (1989)"},{"issue":"4","key":"15_CR3","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/S0747-7171(85)80019-5","volume":"1","author":"L. Bachmair","year":"1985","unstructured":"Bachmair, L., Plaisted, D.: Termination orderings for associative-commutative rewriting systems. J. Symbolic Computation\u00a01(4), 329\u2013349 (1985)","journal-title":"J. Symbolic Computation"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-15983-5","volume-title":"Rewriting Techniques and Applications","author":"B. Buchberger","year":"1985","unstructured":"Buchberger, B.: Basic features and development of the critical-pair\/completion procedure. In: Jouannaud, J.-P. (ed.) RTA 1985. LNCS, vol.\u00a0202, pp. 1\u201345. Springer, Heidelberg (1985)"},{"issue":"2","key":"15_CR5","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/0304-3975(95)00061-5","volume":"159","author":"R. B\u00fcndgen","year":"1996","unstructured":"B\u00fcndgen, R.: Buchberger\u2019s algorithm: The term rewriter\u2019s point of view. Theoretical Computer Science\u00a0159(2), 143\u2013190 (1996)","journal-title":"Theoretical Computer Science"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/3-540-56868-9_29","volume-title":"Rewriting Techniques and Applications","author":"C. Delor","year":"1993","unstructured":"Delor, C., Puel, L.: Extension of the associative path ordering to a chain of associative-commutative symbols. In: Kirchner, C. (ed.) RTA 1993. LNCS, vol.\u00a0690, pp. 389\u2013404. Springer, Heidelberg (1993)"},{"key":"15_CR7","series-title":"Formal Models and Semantics, ch. 6","first-page":"244","volume-title":"Handbook of Theoretical Computer Science","author":"N. Dershowitz","year":"1990","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Formal Models and Semantics, ch. 6, vol.\u00a0B, pp. 244\u2013320. Elsevier, Amsterdam (1990)"},{"key":"15_CR8","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J.-P. Jouannaud","year":"1986","unstructured":"Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput.\u00a015, 1155\u20131194 (1986)","journal-title":"SIAM J. Comput."},{"key":"15_CR9","series-title":"Research Notes in Theoretical Computer Science","volume-title":"Canonical Forms in Finitely Presented Algebras","author":"P. Chenadec Le","year":"1986","unstructured":"Le Chenadec, P.: Canonical Forms in Finitely Presented Algebras. Research Notes in Theoretical Computer Science. Pitman [u.a.], London (1986)"},{"key":"15_CR10","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-60605-2","volume-title":"The Resolution Calculus","author":"A. Leitsch","year":"1997","unstructured":"Leitsch, A.: The Resolution Calculus. Springer, Heidelberg (1997)"},{"key":"15_CR11","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1006\/jsco.1996.0053","volume":"22","author":"J. Levy","year":"1996","unstructured":"Levy, J., Agust\u00ed, J.: Bi-rewrite systems. J. Symbolic Computation\u00a022, 279\u2013314 (1996)","journal-title":"J. Symbolic Computation"},{"issue":"2","key":"15_CR12","doi-asserted-by":"publisher","first-page":"81","DOI":"10.2307\/2266681","volume":"16","author":"P. Lorenzen","year":"1951","unstructured":"Lorenzen, P.: Algebraische und logistische Untersuchungen \u00fcber freie Verb\u00e4nde. The Journal of Symbolic Logic\u00a016(2), 81\u2013106 (1951)","journal-title":"The Journal of Symbolic Logic"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/3-540-52885-7_100","volume-title":"10th International Conference on Automated Deduction","author":"U. Martin","year":"1990","unstructured":"Martin, U., Nipkow, T.: Ordered rewriting and confluence. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol.\u00a0449, pp. 366\u2013380. Springer, Heidelberg (1990)"},{"key":"15_CR14","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1007\/3-540-53904-2_102","volume-title":"4th International Conference on Rewriting Techniques and Applications","author":"R. Socher-Ambrosius","year":"1991","unstructured":"Socher-Ambrosius, R.: Boolean algebra admits no convergent term rewriting system. In: Book, R.E. (ed.) 4th International Conference on Rewriting Techniques and Applications. LNCS, vol.\u00a0488, pp. 264\u2013274. Springer, Heidelberg (1991)"},{"key":"15_CR15","unstructured":"Struth, G.: Non-symmetric rewriting. Technical Report MPI-I-96-2-004, Max- Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken (1996)"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/3-540-62950-5_66","volume-title":"Rewriting Techniques and Applications","author":"G. Struth","year":"1997","unstructured":"Struth, G.: On the word problem for free lattices. In: Comon, H. (ed.) RTA 1997. LNCS, vol.\u00a01232, pp. 128\u2013141. Springer, Heidelberg (1997)"},{"key":"15_CR17","unstructured":"Struth, G.: Canonical Transformations in Algebra, Universal Algebra and Logic. PhD thesis, Institut f\u00fcr Informatik, Universit\u00e4t des Saarlandes (1998)"},{"key":"15_CR18","doi-asserted-by":"crossref","first-page":"466","DOI":"10.1007\/978-3-642-81955-1_28","volume-title":"Automation of Reasoning","author":"G.S. Tseitin","year":"1983","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning, vol.\u00a02, pp. 466\u2013483. Springer, Heidelberg (1983) (reprint)"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10721975_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,23]],"date-time":"2019-03-23T05:38:31Z","timestamp":1553319511000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10721975_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540677789","9783540449805"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/10721975_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}