{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:03Z","timestamp":1749125163698},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540672814"},{"type":"electronic","value":"9783540464211"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10720084_5","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T09:36:30Z","timestamp":1167384990000},"page":"62-72","source":"Crossref","is-referenced-by-count":5,"title":["Axioms vs. Rewrite Rules: From Completeness to Cut Elimination"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Dowek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. In: Rapport de Recherche INRIA 3400 (1998)"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/3-540-48685-2_26","volume-title":"Rewriting Techniques and Applications","author":"G. Dowek","year":"1999","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: HOL-lambda-sigma: an intentional first- order expression of higher-order logic. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol.\u00a01631, pp. 317\u2013331. Springer, Heidelberg (1999)"},{"key":"#cr-split#-5_CR3.1","doi-asserted-by":"crossref","unstructured":"Dowek, G., Werner, B.: Proof normalization modulo. In: Altenkirch, T., Naraschewski, W., Reus, B. (eds.) TYPES 1998. LNCS, vol.\u00a01657, pp. 62\u201377. Springer, Heidelberg (1999);","DOI":"10.1007\/3-540-48167-2_5"},{"key":"#cr-split#-5_CR3.2","unstructured":"Rapport de Recherche 3542, INRIA (1998)"},{"key":"5_CR4","unstructured":"Fay, M.J.: First-order unification in an equational theory. In: Fourth Workshop on Automated Deduction, pp. 161\u2013167 (1979)"},{"key":"5_CR5","volume-title":"Logic in computer science","author":"J. Gallier","year":"1986","unstructured":"Gallier, J.: Logic in computer science. Harper and Row, New York (1986)"},{"key":"5_CR6","volume-title":"Types and proofs","author":"J.Y. Girard","year":"1989","unstructured":"Girard, J.Y., Lafont, Y., Taylor, P.: Types and proofs. Cambridge University Press, Cambridge (1989)"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1007\/3-540-10009-1_25","volume-title":"5th Conference on Automated Deduction","author":"J.-M. Hullot","year":"1980","unstructured":"Hullot, J.-M.: Canonical forms and unification. In: Bibel, W., Kowalski, R. (eds.) CADE 1980. LNCS, vol.\u00a087, pp. 318\u2013334. Springer, Heidelberg (1980)"},{"issue":"3","key":"5_CR8","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1145\/116825.116833","volume":"38","author":"J. Hsiang","year":"1991","unstructured":"Hsiang, J., Rusinowitch, M.: Proving refutational completeness of theorem proving strategies: the transfinite semantic tree method. Journal of the ACM\u00a038(3), 559\u2013587 (1991)","journal-title":"Journal of the ACM"},{"key":"5_CR9","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D.E. Knuth","year":"1970","unstructured":"Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press, Oxford (1970)"},{"issue":"1","key":"5_CR10","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1137\/0212006","volume":"12","author":"G. Peterson","year":"1983","unstructured":"Peterson, G.: A Technique for establishing completeness results in theorem proving with equality. Siam J. Comput.\u00a012(1), 82\u2013100 (1983)","journal-title":"Siam J. Comput."},{"key":"5_CR11","first-page":"73","volume":"7","author":"G. Plotkin","year":"1972","unstructured":"Plotkin, G.: Building-in equational theories. Machine Intelligence\u00a07, 73\u201390 (1972)","journal-title":"Machine Intelligence"},{"key":"5_CR12","first-page":"135","volume-title":"Machine Intelligence","author":"G.A. Robinson","year":"1969","unstructured":"Robinson, G.A., Wos, L.: Paramodulation and theorem proving in first-order theories with equality. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol.\u00a04, pp. 135\u2013150. American Elsevier, Amsterdam (1969)"},{"issue":"1","key":"5_CR13","first-page":"285","volume":"4","author":"M. Stickel","year":"1985","unstructured":"Stickel, M.: Automated deduction by theory resolution. Journal of Automated Reasoning\u00a04(1), 285\u2013289 (1985)","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10720084_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,17]],"date-time":"2019-03-17T22:49:42Z","timestamp":1552862982000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10720084_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672814","9783540464211"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/10720084_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}