{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T12:36:43Z","timestamp":1752669403724},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540542339"},{"type":"electronic","value":"9783540475163"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54233-7_140","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:37:18Z","timestamp":1330209438000},"page":"267-278","source":"Crossref","is-referenced-by-count":7,"title":["Canonical sets of horn clauses"],"prefix":"10.1007","author":[{"given":"Nachum","family":"Dershowitz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/S0747-7171(86)80017-7","volume":"2","author":"J. Avenhaus","year":"1986","unstructured":"J\u00fcrgen Avenhaus. On the descriptive power of term rewriting systems. J. Symbolic Computation, 2:109\u2013122, 1986.","journal-title":"J. Symbolic Computation"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Leo Bachmair and Nachum Dershowitz. Equational inference, canonical proofs, and proof orderings. J. of the Association for Computing Machinery, to appear.","DOI":"10.1145\/174652.174655"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Leo Bachmair and Harald Ganzinger. Completion of first-order clauses with equality. In M. Okada, editor, Proceedings of the Second International Workshop on Conditional and Typed Rewriting Systems, Montreal, Canada, June 1990. Lecture Notes in Computer Science, Springer, Berlin.","DOI":"10.1007\/3-540-54317-1_89"},{"key":"20_CR4","unstructured":"Leo Bachmair, Nachum Dershowitz, and Jieh Hsiang. Orderings for equational proofs. In Proceedings of the IEEE Symposium on Logic in Computer Science, pages 346\u2013357, Cambridge, MA, June 1986."},{"key":"20_CR5","first-page":"1","volume-title":"Resolution of Equations in Algebraic Structures 2: Rewriting Techniques","author":"L. Bachmair","year":"1989","unstructured":"Leo Bachmair, Nachum Dershowitz, and David A. Plaisted. Completion without failure. In H. A\u00eft-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures 2: Rewriting Techniques, chapter 1, pages 1\u201330. Academic Press, New York, 1989."},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Hubert Bertling. Knuth-Bendix completion of Horn clause programs for restricted linear resolution and paramodulation. In S. Kaplan and M. Okada, editors, Extended Abstracts of the Second International Workshop on Conditional and Typed Rewriting Systems, pages 89\u201395, Montreal, Canada, June 1990. Revised version to appear in Lecture Notes in Computer Science, Springer, Berlin.","DOI":"10.1007\/3-540-54317-1_90"},{"key":"20_CR7","volume-title":"Experiments with computer implementations of procedures which often derive decision algorithms for the word problem in abstract algebras","author":"G. Butler","year":"1980","unstructured":"George Butler and Dallas S. Lankford. Experiments with computer implementations of procedures which often derive decision algorithms for the word problem in abstract algebras. Memo MTP-7, Department of Mathematics, Louisiana Tech. University, Ruston, LA, August 1980."},{"key":"20_CR8","first-page":"243","volume-title":"Handbook of Theoretical Computer Science B: Formal Methods and Semantics","author":"N. Dershowitz","year":"1990","unstructured":"Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science B: Formal Methods and Semantics, chapter 6, pages 243\u2013320. North-Holland, Amsterdam, 1990."},{"issue":"8","key":"20_CR9","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N. Dershowitz","year":"1979","unstructured":"Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465\u2013476, August 1979.","journal-title":"Communications of the ACM"},{"key":"20_CR10","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1016\/0304-3975(90)90064-O","volume":"75","author":"N. Dershowitz","year":"1990","unstructured":"Nachum Dershowitz and Mitsuhiro Okada. A rationale for conditional equational programming. Theoretical Computer Science, 75:111\u2013138, 1990.","journal-title":"Theoretical Computer Science"},{"key":"20_CR11","first-page":"31","volume-title":"Proceedings of the First International Workshop on Conditional Term Rewriting Systems","author":"N. Dershowitz","year":"1987","unstructured":"Nachum Dershowitz, Mitsuhiro Okada, and G. Sivakumar. Confluence of conditional rewrite systems. In S. Kaplan and J.-P. Jouannaud, editors, Proceedings of the First International Workshop on Conditional Term Rewriting Systems, pages 31\u201344, Orsay, France, July 1987. Vol. 308 of Lecture Notes in Computer Science, Springer, Berlin (1988)."},{"issue":"3","key":"20_CR12","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"Nachum Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17(3):279\u2013301, March 1982.","journal-title":"Theoretical Computer Science"},{"issue":"1&2","key":"20_CR13","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"Nachum Dershowitz. Termination of rewriting. J. of Symbolic Computation, 3(1&2):69\u2013115, February\/April 1987. Corrigendum: 4, 3 (December 1987), 409\u2013410.","journal-title":"J. of Symbolic Computation"},{"key":"20_CR14","first-page":"31","volume-title":"Resolution of Equations in Algebraic Structures 2: Rewriting Techniques","author":"N. Dershowitz","year":"1989","unstructured":"Nachum Dershowitz. Completion and its applications. In H. A\u00eft-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures 2: Rewriting Techniques, chapter 2, pages 31\u201386. Academic Press, New York, 1989."},{"key":"20_CR15","unstructured":"Nachum Dershowitz. Ordering-based strategies for Horn clauses. In Proceedings of the 12th International Joint Conference on Artificial Intelligence, Sydney, Australia, August 1991. To appear."},{"issue":"3","key":"20_CR16","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"1","author":"W. F. Dowling","year":"1984","unstructured":"William F. Dowling and Jean H. Gallier. Linear-time algorithms for testing the satisfiability of propositional Horn formulae. J. of Logic Programming, 1(3):267\u2013284, 1984.","journal-title":"J. of Logic Programming"},{"key":"20_CR17","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1007\/BFb0012832","volume-title":"Proceedings of the Ninth International Conference on Automated Deduction","author":"J. Gallier","year":"1988","unstructured":"Jean Gallier, Paliath Narendran, David Plaisted, Stan Raatz, and Wayne Snyder. Finding canonical rewriting systems equivalent to a finite set of ground equations in polynomial time. In E. Lusk and R. Overbeek, editors, Proceedings of the Ninth International Conference on Automated Deduction, pages 182\u2013196, Argonne, Illinois, May 1988. Vol. 310 of Lecture Notes in Computer Science, Springer, Berlin."},{"key":"20_CR18","first-page":"62","volume-title":"Proceedings of the First International Workshop on Conditional Term Rewriting Systems","author":"H. Ganzinger","year":"1987","unstructured":"Harald Ganzinger. A completion procedure for conditional equations. In S. Kaplan and J.-P. Jouannaud, editors, Proceedings of the First International Workshop on Conditional Term Rewriting Systems, pages 62\u201383, Orsay, France, July 1987. Vol. 308 of Lecture Notes in Computer Science, Springer, Berlin (1988)."},{"key":"20_CR19","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/3-540-16780-3_86","volume-title":"Proceedings of the Eighth International Conference on Automated Deduction","author":"J. Hsiang","year":"1986","unstructured":"Jieh Hsiang and Micha\u00ebl Rusinowitch. A new method for establishing refutational completeness in theorem proving. In J. H. Siekmann, editor, Proceedings of the Eighth International Conference on Automated Deduction, pages 141\u2013152, Oxford, England, July 1986. Vol. 230 of Lecture Notes in Computer Science, Springer, Berlin."},{"key":"20_CR20","first-page":"54","volume-title":"Proceedings of the Fourteenth EATCS International Conference on Automata, Languages and Programming","author":"J. Hsiang","year":"1987","unstructured":"Jieh Hsiang and Micha\u00ebl Rusinowitch. On word problems in equational theories. In T. Ottmann, editor, Proceedings of the Fourteenth EATCS International Conference on Automata, Languages and Programming, pages 54\u201371, Karlsruhe, West Germany, July 1987. Vol. 267 of Lecture Notes in Computer Science, Springer, Berlin."},{"key":"20_CR21","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1016\/B978-0-12-115350-2.50017-8","volume-title":"Formal Language Theory: Perspectives and Open Problems","author":"G. Huet","year":"1980","unstructured":"G\u00e9rard Huet and Derek C. Oppen. Equations and rewrite rules: A survey. In R. Book, editor, Formal Language Theory: Perspectives and Open Problems, pages 349\u2013405. Academic Press, New York, 1980."},{"issue":"1","key":"20_CR22","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1016\/0022-0000(81)90002-7","volume":"23","author":"G. Huet","year":"1981","unstructured":"G\u00e9rard Huet. A complete proof of correctness of the Knuth-Bendix completion algorithm. J. Computer and System Sciences, 23(1):11\u201321, 1981.","journal-title":"J. Computer and System Sciences"},{"key":"20_CR23","volume-title":"Proceedings of the Third IFIP Working Conference on Formal Description of Programming Concepts","author":"J. Jouannaud","year":"1986","unstructured":"Jean-Pierre Jouannaud and Bernard Waldmann. Reductive conditional term rewriting systems. In Proceedings of the Third IFIP Working Conference on Formal Description of Programming Concepts, Ebberup, Denmark, 1986."},{"key":"20_CR24","volume-title":"Two generalizations of the recursive path ordering","author":"S. Kamin","year":"1980","unstructured":"Sam Kamin and Jean-Jacques L\u00e9vy. Two generalizations of the recursive path ordering. Unpublished note, Department of Computer Science, University of Illinois, Urbana, IL, February 1980."},{"issue":"3","key":"20_CR25","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1016\/S0747-7171(87)80010-X","volume":"4","author":"S. Kaplan","year":"1987","unstructured":"St\u00e9phane Kaplan. Simplifying conditional term rewriting systems: Unification, termination and confluence. J. Symbolic Computation, 4(3):295\u2013334, December 1987.","journal-title":"J. Symbolic Computation"},{"key":"20_CR26","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D. E. Knuth","year":"1970","unstructured":"Donald E. Knuth and P. B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263\u2013297. Pergamon Press, Oxford, U. K., 1970. Reprinted in Automation of Reasoning 2, Springer, Berlin, pp. 342\u2013376 (1983)."},{"key":"20_CR27","first-page":"144","volume-title":"Proceedings of the First International Workshop on Conditional Term Rewriting Systems","author":"E. Kounalis","year":"1987","unstructured":"Emmanuel Kounalis and Micha\u00ebl Rusinowitch. On word problems in Horn theories. In S. Kaplan and J.-P. Jouannaud, editors, Proceedings of the First International Workshop on Conditional Term Rewriting Systems, pages 144\u2013160, Orsay, France, July 1987. Vol. 308 of Lecture Notes in Computer Science, Springer, Berlin (1988)."},{"key":"20_CR28","volume-title":"On the uniqueness of term rewriting systems","author":"D. S. Lankford","year":"1983","unstructured":"Dallas S. Lankford and A. Michael Ballantyne. On the uniqueness of term rewriting systems. Unpublished note, Department of Mathematics, Louisiana Tech. University, Ruston, LA, December 1983."},{"key":"20_CR29","volume-title":"Canonical inference","author":"D. S. Lankford","year":"1975","unstructured":"Dallas S. Lankford. Canonical inference. Memo ATP-32, Automatic Theorem Proving Project, University of Texas, Austin, TX, December 1975."},{"key":"20_CR30","doi-asserted-by":"crossref","first-page":"374","DOI":"10.1007\/3-540-15198-2_24","volume-title":"Mathematical Foundations of Software Development","author":"J. A. Makowsky","year":"1985","unstructured":"J. A. Makowsky. Why Horn formulas matter in computer science: Initial structures and generic examples. In Mathematical Foundations of Software Development, pages 374\u2013385, 1985. Vol. 185 of Lecture Notes in Computer Science, Springer, Berlin."},{"issue":"1","key":"20_CR31","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/0020-0190(83)90009-1","volume":"16","author":"Y. M\u00e9tivier","year":"1983","unstructured":"Yuves M\u00e9tivier. About the rewriting systems produced by the Knuth-Bendix completion algorithm. Information Processing Letters, 16(1):31\u201334, January 1983.","journal-title":"Information Processing Letters"},{"key":"20_CR32","first-page":"81","volume-title":"Extended Abstracts of the Second International Workshop on Conditional and Typed Rewriting Systems","author":"R. Nieuwenhuis","year":"1990","unstructured":"Robert Nieuwenhuis and Fernando Orejas. Clausal rewriting. In S. Kaplan and M. Okada, editors, Extended Abstracts of the Second International Workshop on Conditional and Typed Rewriting Systems, pages 81\u201388, Montreal, Canada, June 1990. Concordia University. Revised version to appear in Lecture Notes in Computer Science, Springer, Berlin."},{"key":"20_CR33","unstructured":"Jean-Luc R\u00e9my and Hantao Zhang. REVEUR4: A system for validating conditional algebraic specifications of abstract data types. In Proceedings of the Sixth European Conference on Artificial Intelligence, pages 563\u2013572, Pisa, Italy, 1984."},{"key":"20_CR34","first-page":"135","volume-title":"Machine Intelligence 4","author":"G. Robinson","year":"1969","unstructured":"G. Robinson and L. Wos. Paramodulation and theorem-proving in first order theories with equality. In B. Meltzer and D. Michie, editors, Machine Intelligence 4, pages 135\u2013150. Edinburgh University Press, Edinburgh, Scotland, 1969."},{"key":"20_CR35","volume-title":"D\u00e9monstration Automatique: Techniques de r\u00e9\u00e9criture","author":"M. Rusinowitch","year":"1989","unstructured":"Micha\u00ebl Rusinowitch. D\u00e9monstration Automatique: Techniques de r\u00e9\u00e9criture. InterEditions, Paris, France, 1989."},{"key":"20_CR36","first-page":"1","volume-title":"Proceedings of the Ninth International Conference on Automated Deduction","author":"H. Zhang","year":"1988","unstructured":"Hantao Zhang and Deepak Kapur. First-order theorem proving using conditional equations. In E. Lusk and R. Overbeek, editors, Proceedings of the Ninth International Conference on Automated Deduction, pages 1\u201320, Argonne, Illinois, May 1988. Vol. 310 of Lecture Notes in Computer Science, Springer, Berlin."},{"key":"20_CR37","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1007\/3-540-15976-2_2","volume-title":"Proceedings of the First International Conference on Rewriting Techniques and Applications","author":"H. Zhang","year":"1985","unstructured":"Hantao Zhang and Jean-Luc R\u00e9my. Contextual rewriting. In Proceedings of the First International Conference on Rewriting Techniques and Applications, pages 46\u201362, Dijon, France, May 1985. Vol. 202 of Lecture Notes in Computer Science, Springer, Berlin (September 1985)."}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54233-7_140.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:53:12Z","timestamp":1605646392000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54233-7_140"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540542339","9783540475163"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/3-540-54233-7_140","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}