{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:40Z","timestamp":1749124060791},"publisher-location":"Berlin\/Heidelberg","reference-count":35,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354019343X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0012820","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T01:12:39Z","timestamp":1132708359000},"page":"1-20","source":"Crossref","is-referenced-by-count":21,"title":["First-order theorem proving using conditional rewrite rules"],"prefix":"10.1007","author":[{"given":"Hantao","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Deepak","family":"Kapur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"1_CR1","unstructured":"Bachmair, L., Dershowitz, N., and Hsiang, J., \u201cOrderings for equational proofs,\u201d Proc. IEEE Symp. Logic in Computer Science, Cambridge, MA, 336\u2013357, 1986."},{"key":"1_CR2","unstructured":"Bachmair, L., and Dershowitz, N., \u201cInference rules for rewrite-based first-order theorem proving,\u201d Proc. IEEE Symp. Logic in Computer Science, Ithaca, New York, 1987."},{"key":"1_CR3","volume-title":"Locking: A restriction of resolution","author":"R.S. Boyer","year":"1971","unstructured":"Boyer, R.S., Locking: A restriction of resolution. Ph.D. Thesis, University of Texas, Austin, 1971."},{"key":"1_CR4","volume-title":"A computational logic","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S. and Moore, J.S., A computational logic. Academic Press, New York, 1979."},{"key":"1_CR5","unstructured":"Brand, D., Darringer, J.A., and Joyner, W.H., Completeness of conditional reductions. Research Report RC 7404 IBM, 1978."},{"key":"1_CR6","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/3-540-15976-2_15","volume":"202","author":"B. Buchberger","year":"1985","unstructured":"Buchberger, B., \u201cHistory and basic feature of the critical-pair\/completion procedure,\u201d Rewriting Techniques and Applications, Lect. Notes in Comp. Sci., Vol. 202, Springer-Verlag, Berlin, 301\u2013324, 1985.","journal-title":"Lect. Notes in Comp. Sci."},{"key":"1_CR7","volume-title":"Symbolic logic and mechanical theorem proving","author":"C-L. Chang","year":"1973","unstructured":"Chang, C-L. and Lee, R.C., Symbolic logic and mechanical theorem proving. Academic Press, New York, 1973."},{"key":"1_CR8","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"Dershowitz, N., \u201cTermination of rewriting,\u201d J. of Symbolic Computation Vol. 3, 1987, 69\u2013116.","journal-title":"J. of Symbolic Computation"},{"key":"1_CR9","unstructured":"Drosten K. Toward executable specifications using conditional axioms. Report 83-01, t.U. Braunschweig, 1983."},{"key":"1_CR10","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/0304-3975(85)90011-8","volume":"35","author":"L. Fribourg","year":"1985","unstructured":"Fribourg, L., \u201cA superposition oriented theorem prover\u201d Theoretical Computer Science, Vol. 35, 129\u2013164, 1985.","journal-title":"Theoretical Computer Science"},{"key":"1_CR11","unstructured":"Fribourg, L., \u201cSLOG: A logic programming language interpreter based on clausal superposition and rewriting,\u201d In Proc. 1985 Intl. Symposium on Logic Programming, pp. 172\u2013184, Boston, 1985."},{"key":"1_CR12","volume-title":"Topics in automated theorem proving and program generation","author":"J. Hsiang","year":"1982","unstructured":"Hsiang, J., Topics in automated theorem proving and program generation. Ph.D. Thesis, UIUCDCS-R-82-1113, Univ. of Illinois, Urbana-Champaigne, 1982."},{"key":"1_CR13","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/S0747-7171(87)80024-X","volume":"3","author":"J. Hsiang","year":"1987","unstructured":"Hsiang, J., \u201cRewrite method for theorem proving in first order theory with equality,\u201d J. Symbolics Computation, Vol. 3, 133\u2013151, 1987.","journal-title":"J. Symbolics Computation"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Hsiang, J., and Rusinowitch, M., \u201cA new method for establishing refutational completeness in theorem proving,\u201d Proc. 8th Conf. on Automated Deduction, LNCS No. 230, Springer-Verlag, 141\u2013152, 1986.","DOI":"10.1007\/3-540-16780-3_86"},{"key":"1_CR15","volume-title":"Formal languages: Perspectives and open problems","author":"G. Huet","year":"1980","unstructured":"Huet, G. and Oppen, D., \u201cEquations and rewrite rules: a survey,\u201d in: Formal languages: Perspectives and open problems. (R. Book, ed.), Academic Press, New York, 1980."},{"key":"1_CR16","volume-title":"Fair conditional term rewriting systems: unification, termination and confluence","author":"S. Kaplan","year":"1984","unstructured":"Kaplan S., Fair conditional term rewriting systems: unification, termination and confluence. LRI, Orsay, 1984."},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Kapur, D. and Narendran, P., \u201cAn equational approach to theorem proving in first-order predicate calculus,\u201d 9th IJCAI, Los Angeles, CA, August 1985.","DOI":"10.1145\/1012497.1012521"},{"key":"1_CR18","volume-title":"Proc. 8th Intl Conf. on Automated Deduction (CADE-8)","author":"D. Kapur","year":"1986","unstructured":"Kapur, D., Sivakumar, G., and Zhang, H., \u201cRRL: A Rewrite Rule Laboratory,\u201d Proc. 8th Intl Conf. on Automated Deduction (CADE-8), Oxford, U.K., LNCS 230, Springer-Verlag, 1986."},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Knuth, D., and Bendix, P., \u201cSimple Word Problems in Universal Algebras,\u201d in: Computational problems in abstract algebra. (Leech, ed.) Pergamon Press, 263\u2013297, 1970.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"1_CR20","unstructured":"Kowalski, R., and Hayes, P., \u201cSemantic trees in automatic theorem proving,\u201d in Machine Intelligence, Vol. 5, (Meltzer, B. and Michie, D., eds.) American Elsevier, 1969."},{"key":"1_CR21","volume-title":"Canonical inference. Report ATP-32","author":"D.S. Lankford","year":"1975","unstructured":"Lankford, D.S., Canonical inference. Report ATP-32, Dept. of Mathematics and Computer Sciences, Univ. of Texas, Austin, Texas, 1975."},{"key":"1_CR22","volume-title":"Decision procedures for simple equational theories with commutative-associative axioms: Complete sets of commutative-associative reductions. Memo ATP-39","author":"D.S. Lankford","year":"1977","unstructured":"Lankford, D.S., and Ballantyne, A.M., Decision procedures for simple equational theories with commutative-associative axioms: Complete sets of commutative-associative reductions. Memo ATP-39, Department of Mathematics and Computer Sciences, University of Texas, Austin, TX, August 1977."},{"key":"1_CR23","unstructured":"Lankford, D.S., and Ballantyne, A.M., \u201cThe refutational completeness of blocked permutative narrowing and resolution,\u201d 4th Conf. on Automated Deduction, Austin, Texas, 1979."},{"key":"1_CR24","unstructured":"Lankford, D.S., Some new approaches to the theory and applications of conditional term rewriting systems. Report MTP-6, Math. Dept., Lousiana Tech. University, 1979."},{"key":"1_CR25","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"F.J. Pelletier","year":"1986","unstructured":"Pelletier F.J., \u201cSeventy-five problems for testing automatic theorem provers,\u201d J. of Automated reasoning Vol. 2, 191\u2013216, 1986.","journal-title":"J. of Automated reasoning"},{"key":"1_CR26","unstructured":"Pletat, U., Engels, G., and Ehrich, H.D., \u201cOperational semantics of algebraic specifications with conditional equations,\u201d 7th, CAAP '82, LNCS, Springer-Verlag, 1982."},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Reiter, R., \u201cTwo results on ordering fro resolution with merging and linear format,\u201d JACM, 630\u2013646, 1971.","DOI":"10.1145\/321662.321678"},{"key":"1_CR28","unstructured":"Remy, J.L., Etudes des systemes reecriture conditionnelles et applications aux types abstraits algebriques. These d'etat, Universite Nancy I, 1982."},{"issue":"1","key":"1_CR29","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1137\/0212006","volume":"12","author":"G.E. Peterson","year":"1983","unstructured":"Peterson, G.E., \u201cA technique for establishing completeness results in theorem proving with equality,\u201d SIAM J. Computing Vol. 12, No. 1. 82\u201399, 1983.","journal-title":"SIAM J. Computing"},{"issue":"2","key":"1_CR30","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G.L. Peterson","year":"1981","unstructured":"Peterson, G.L., and Stickel, M.E., \u201cComplete sets of reductions for some equational theories,\u201d JACM Vol. 28 No. 2, 233\u2013264, 1981.","journal-title":"JACM"},{"key":"1_CR31","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/BF00244275","volume":"1","author":"M.E. Stickel","year":"1985","unstructured":"Stickel, M.E., \u201cAutomated deduction by theory resolution,\u201d J. of Automated Reasoning Vol. 1, 333\u2013355, 1985.","journal-title":"J. of Automated Reasoning"},{"key":"1_CR32","unstructured":"Walther, C., \u201cA mechanical solution of Schubert's steamroller by many-sorted resolution,\u201d Proc. of the AAAI-84 National Conf. on Artificial Intelligence, Austin, Texas, 330\u2013334, 1984."},{"key":"1_CR33","first-page":"276","volume-title":"Proc. IRIA Symposium on Automatic Demonstration, Versailles, France, 1968","author":"L.R. Wos","year":"1970","unstructured":"Wos, L.R., and Robinson, G., \u201cParamodulation and set of support,\u201d Proc. IRIA Symposium on Automatic Demonstration, Versailles, France, 1968, Springer-Verlag, Berlin, 276\u2013310, 1970."},{"key":"1_CR34","volume-title":"Reveur 4: Etude et Mise en Oeuvre de la Reecriture Conditionelle","author":"H. Zhang","year":"1984","unstructured":"Zhang, H., Reveur 4: Etude et Mise en Oeuvre de la Reecriture Conditionelle. Thesis of \"Doctorat de 3me cycle\", Universite de Nancy I, France, 1984."},{"key":"1_CR35","doi-asserted-by":"crossref","unstructured":"Zhang, H., and Remy, J.L., \u201cContextual rewriting,\u201d Proc. of rewriting techniques and application, Dijon, France, 1985.","DOI":"10.1007\/3-540-15976-2_2"}],"container-title":["Lecture Notes in Computer Science","9th International Conference on Automated Deduction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0012820","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T00:24:04Z","timestamp":1586564644000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0012820"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354019343X"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/bfb0012820","relation":{},"subject":[]}}