{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:48:07Z","timestamp":1749124087841},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540609834"},{"type":"electronic","value":"9783540497516"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-60983-0_8","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:10:03Z","timestamp":1330290603000},"page":"119-136","source":"Crossref","is-referenced-by-count":6,"title":["Handling equality in logic programming via basic folding"],"prefix":"10.1007","author":[{"given":"Anatoli","family":"Degtyarev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"S. Antoy, R. Echahed, and M. Hanus. A needed narrowing strategy. In ACM Symposium on Principles of Programming Languages, pages 268\u2013279, Portland, 1994.","DOI":"10.1145\/174675.177899"},{"key":"8_CR2","unstructured":"L. Bachmair, N. Dershowitz, and D. Plaisted. Completion without failure. In H. A\u00eft Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, volume 2, pages 1\u201330. Academic Press, 1989."},{"issue":"3","key":"8_CR3","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"L. Bachmair and H. Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217\u2013247, 1994.","journal-title":"Journal of Logic and Computation"},{"key":"8_CR4","first-page":"462","volume-title":"volume 607 of Lecture Notes in Artificial Intelligence","author":"L. Bachmair","year":"1992","unstructured":"L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder. Basic paramodulation and superposition. In D. Kapur, editor, 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 462\u2013476, Saratoga Springs, NY, USA, June 1992. Springer Verlag."},{"key":"8_CR5","doi-asserted-by":"crossref","first-page":"764","DOI":"10.1090\/S0002-9904-1944-08235-9","volume":"50","author":"G. Birkhoff","year":"1944","unstructured":"G. Birkhoff. Subdirect unions in universal algebras. Bull. Amer. Math. Soc., 50:764\u2013768, 1944.","journal-title":"Bull. Amer. Math. Soc."},{"key":"8_CR6","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(88)90095-3","volume":"59","author":"P.G. Bosco","year":"1988","unstructured":"P.G. Bosco, E. Giovanetti, and C. Moiso. Narrowing vs. SLD-resolution. Theoretical Computer Science, 59:3\u201323, 1988.","journal-title":"Theoretical Computer Science"},{"key":"8_CR7","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D. Brand","year":"1975","unstructured":"D. Brand. Proving theorems with the modification method. SIAM Journal of Computing, 4:412\u2013430, 1975.","journal-title":"SIAM Journal of Computing"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"A. Degtyarev, Yu. Koval, and A. Voronkov. Handling equality in logic programming via basic folding. UPMAIL Technical Report 101, Uppsala University, Computing Science Department, March 1995.","DOI":"10.1007\/3-540-60983-0_8"},{"key":"8_CR9","unstructured":"A. Degtyarev and A. Voronkov. Methods of handling equality in machine theorem proving (in Russian). Kibernetika, (3), 1986. English translation in Cybernetics 22 (1986), pp. 298\u2013307."},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"A. Degtyarev and A. Voronkov. A new procedural interpretation of Horn clauses with equality. In Leon Sterling, editor, Proceedings of the Twelfth International Conference on Logic Programming, pages 565\u2013579. The MIT Press, 1995.","DOI":"10.7551\/mitpress\/4298.003.0057"},{"key":"8_CR11","unstructured":"A. Degtyarev and A. Voronkov. Equality elimination for the inverse method and extension procedures. In C.S. Mellish, editor, Proc. International Joint Conference on Artificial Intelligence (IJCAI), volume 1, pages 342\u2013347, Montr\u00e9al, August 1995."},{"key":"8_CR12","series-title":"volume B: Formal Methods and Semantics","first-page":"243","volume-title":"Handbook of Theoretical Computer Science","author":"N. Dershowitz","year":"1990","unstructured":"N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. Van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics, chapter 6, pages 243\u2013309. North Holland, Amsterdam, 1990."},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"E.W. Elcock. Prolog: Subsumption of equality axioms by the homogeneous form. Journal of Logic Programming, pages 45\u201356, 1989.","DOI":"10.1016\/0743-1066(89)90029-0"},{"key":"8_CR14","unstructured":"L. Fribourg. Slog: A logic programming language interpreter based on clausal superposition and rewriting. In IEEE International Symposium on Logic Programming, pages 172\u2013184, Boston, 1985."},{"key":"8_CR15","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/BF00248322","volume":"5","author":"U. Furbach","year":"1989","unstructured":"U. Furbach, S. H\u00f6lldobler, and J. Schreiber. Horn equality theories and paramodulation. Journal of Automated Reasoning, 5:309\u2013337, 1989.","journal-title":"Journal of Automated Reasoning"},{"issue":"3","key":"8_CR16","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0743-1066(89)90028-9","volume":"6","author":"J.H. Gallier","year":"1989","unstructured":"J.H. Gallier and S. Raatz. Extending SLD-resolution to equational Horn clauses using E-unification. Journal of Logic Programming, 6(3):3\u201344, 1989.","journal-title":"Journal of Logic Programming"},{"key":"8_CR17","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/S0747-7171(08)80132-0","volume":"11","author":"H. Ganzinger","year":"1991","unstructured":"H. Ganzinger. A completion procedure for conditional equations. Journal of Symbolic Computations, 11:51\u201381, 1991.","journal-title":"Journal of Symbolic Computations"},{"key":"8_CR18","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1016\/0743-1066(94)90034-5","volume":"19","author":"M. Hanus","year":"1994","unstructured":"M. Hanus. The integration of functions into logic programming: from theory to practice. Journal of Logic Programming, 19,20:583\u2013628, 1994.","journal-title":"Journal of Logic Programming"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"S. H\u00f6lldobler. Foundations of Equational Logic Programming, volume 353 of Lecture Notes in Artificial Intelligence. Springer Verlag, 1989.","DOI":"10.1007\/BFb0015791"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"J.M. Hullot. Canonical forms and unification. In 5th CADE, volume 87 of Lecture Notes in Computer Science, pages 318\u2013334, 1980.","DOI":"10.21236\/ADA087640"},{"key":"8_CR21","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1016\/0304-3975(84)90087-2","volume":"33","author":"S. Kaplan","year":"1984","unstructured":"S. Kaplan. Conditional rewrite rules. Theoretical Computer Science, 33:175\u2013193, 1984.","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"8_CR22","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1016\/S0747-7171(87)80010-X","volume":"4","author":"S. Kaplan","year":"1987","unstructured":"S. Kaplan. Simplifying conditional term rewriting systems: Unification, termination and confluence. Journal of Symbolic Computations, 4(3):295\u2013334, 1987.","journal-title":"Journal of Symbolic Computations"},{"key":"8_CR23","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(93)90243-M","volume":"120","author":"E. Knill","year":"1993","unstructured":"E. Knill, P.T. Cox, and T. Pietrzykowski. Equality and abductive residua for Horn clauses. Theoretical Computer Science, 120:1\u201344, 1993.","journal-title":"Theoretical Computer Science"},{"key":"8_CR24","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D. Knuth","year":"1970","unstructured":"D. Knuth and P. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263\u2013297. Pergamon Press, Oxford, 1970."},{"key":"8_CR25","volume-title":"Technical report","author":"D.S. Lankford","year":"1975","unstructured":"D.S. Lankford. Canonical inference. Technical report, Department of Mathematics, South-Western University, Georgetown, Texas, 1975."},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"J.W. Lloyd. Foundations of Logic Programming (2nd edition). Springer Verlag, 1987.","DOI":"10.1007\/978-3-642-83189-8"},{"key":"8_CR27","first-page":"264","volume":"109","author":"A. Ma\u013acev","year":"1956","unstructured":"A. Ma\u013acev. Subdirect products of models. Dokl. Akad. Nauk SSSR (in Russian), 109:264\u2013266, 1956.","journal-title":"Dokl. Akad. Nauk SSSR (in Russian)"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"R. Nieuwenhuis and A. Rubio. Basic superposition is complete. In ESOP'92, volume 582 of Lecture Notes in Computer Science, pages 371\u2013389. Springer Verlag, 1992.","DOI":"10.1007\/3-540-55253-7_22"},{"issue":"1","key":"8_CR29","first-page":"1","volume":"11","author":"R. Nieuwenhuis","year":"1995","unstructured":"R. Nieuwenhuis and A. Rubio. Theorem proving with ordering and equality constrained clauses. Journal of Symbolic Computations, 11(1):1\u201332, 1995.","journal-title":"Journal of Symbolic Computations"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"R. Nieuwenhuis. On narrowing, refutation proofs and constraints. In J. Hsiang, editor, Rewriting Techniques and Applications, volume 914 of Lecture Notes in Computer Science, pages 56\u201370, 1995.","DOI":"10.1007\/3-540-59200-8_47"},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"P. Padawitz. Computing in Horn Clause Theories, volume 16 of EATCS Monographs in Theoretical Computer Science. Springer Verlag, 1988.","DOI":"10.1007\/978-3-642-73824-1"},{"issue":"1","key":"8_CR32","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1137\/0212006","volume":"12","author":"G.E. Peterson","year":"1983","unstructured":"G.E. Peterson. A technique for establishing completeness results in theorem proving with equality. SIAM Journal of Computing, 12(1):82\u2013100, 1983.","journal-title":"SIAM Journal of Computing"},{"key":"8_CR33","first-page":"73","volume-title":"Machine Intelligence, volume 7","author":"G. Plotkin","year":"1972","unstructured":"G. Plotkin. Building-in equational theories. In Meltzer and Michie, editors, Machine Intelligence, volume 7, pages 73\u201390. Edinburgh University Press, Edinburgh, 1972."},{"key":"8_CR34","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1016\/S0747-7171(08)80131-9","volume":"11","author":"M. Rusinowitch","year":"1991","unstructured":"M. Rusinowitch. Theorem proving with resolution and superposition: an extension of the Knuth and Bendix completion procedure as a complete set of inference rules. Journal of Symbolic Computations, 11:21\u201349, 1991.","journal-title":"Journal of Symbolic Computations"},{"issue":"4","key":"8_CR35","doi-asserted-by":"crossref","first-page":"622","DOI":"10.1145\/321850.321859","volume":"21","author":"J.R. Slagle","year":"1974","unstructured":"J.R. Slagle. Automated theorem-proving for theories with simplifiers, commutativity and associativity. Journal of the Association for Computing Machinery, 21(4):622\u2013642, 1974.","journal-title":"Journal of the Association for Computing Machinery"},{"issue":"4","key":"8_CR36","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1007\/BF00244359","volume":"6","author":"S. Winker","year":"1990","unstructured":"S. Winker. Robbins algebra: Conditions that make a near-boolean algebra boolean. Journal of Automated Reasoning, 6(4):465\u2013489, 1990.","journal-title":"Journal of Automated Reasoning"},{"key":"8_CR37","doi-asserted-by":"crossref","unstructured":"H. Zhang and D. Kapur. First-order theorem proving using conditional rewrite rules. In E. Lusk and R. Overbeek, editors, 9th International Conference on Automated Deduction, volume 310 of Lecture Notes in Computer Science, pages 1\u201320, 1988.","DOI":"10.1007\/BFb0012820"},{"issue":"3","key":"8_CR38","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/BF00881872","volume":"11","author":"H. Zhang","year":"1993","unstructured":"H. Zhang. Automatic proofs of equality problems in Overbeek's competition. Journal of Automated Reasoning, 11(3):333\u2013351, 1993.","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Extensions of Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60983-0_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T17:14:26Z","timestamp":1713633266000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60983-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540609834","9783540497516"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/3-540-60983-0_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}