{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T13:26:54Z","timestamp":1760707614777},"publisher-location":"Berlin\/Heidelberg","reference-count":51,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354019343X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0012853","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T06:12:39Z","timestamp":1132726359000},"page":"517-526","source":"Crossref","is-referenced-by-count":9,"title":["Solving disequations in equational theories"],"prefix":"10.1007","author":[{"given":"Hans-J\u00fcrgen","family":"B\u00fcrckert","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"34_CR1","unstructured":"W. Buntine: A Theory of Equations, Inequations, and Solutions for Logic Programming. New South Wales Institute of Technology, 1986."},{"key":"34_CR2","doi-asserted-by":"crossref","unstructured":"H.-J. B\u00fcrckert: Lazy Theory Unification in PROLOG: An Extension of the Warren Abstract Machine. Proc. of 10th German Workshop on Art. Intelligence, Springer, 1986, p. 277\u2013288.","DOI":"10.1007\/978-3-642-71385-9_28"},{"key":"34_CR3","unstructured":"H.-J. B\u00fcrckert: Matching \u2014 A Special Case of Unification? SEKI-Report, Universit\u00e4t Kaiserslautern, 1987."},{"key":"34_CR4","unstructured":"H.-J. B\u00fcrckert: Solving Disequations in Equational Theories. SEKI-Report, Universit\u00e4t Kaiserslautern, 1987."},{"key":"34_CR5","doi-asserted-by":"crossref","unstructured":"H.-J. B\u00fcrckert, A. Herold & M. Schmidt-Schau\u00df: On Equational Theories, Unification, and Decidability. Proc. of 2nd Conf. on Rewriting Techniques and Applications, Springer, LNCS 256, 1987, p. 204\u2013215; to appear also in J. of Symb. Comp., Special Issue on Unification (ed. C. Kirchner), 1987.","DOI":"10.1007\/3-540-17220-3_18"},{"key":"34_CR6","doi-asserted-by":"crossref","unstructured":"H.-J. B\u00fcrckert, A. Herold, J. Siekmann, M. Stickel & M. Tepp: Opening the AC-Unification Race. In preparation, 1988","DOI":"10.1007\/BF00297251"},{"issue":"1","key":"34_CR7","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/BF00246024","volume":"2","author":"W. B\u00fcttner","year":"1986","unstructured":"W. B\u00fcttner: Unification in the Datastructure Multisets. J. of Automated Reasoning, Vol. 2, No. 1, 1986, p. 75\u201388.","journal-title":"J. of Automated Reasoning"},{"key":"34_CR8","unstructured":"S. Burris, H.P. Sankappanavar: A Course in Universal Algebra. Springer, 1979."},{"key":"34_CR9","unstructured":"C.-L. Chang & R.C.-T. Lee: Symbolic Logic and Theorem Proving. Academic Press, 1973."},{"key":"34_CR10","unstructured":"A. Colmerauer: Equations and Inequations on Finite and Infinite Trees. Proc. of Conf. on Fifth Gen. Comp. Syst., ICOT, 1984, p. 85\u201399."},{"key":"34_CR11","first-page":"128","volume":"230","author":"H. Comon","year":"1986","unstructured":"H. Comon: Sufficient Completeness, Term Rewriting Systems, and Anti-unification. Proc. of Conf. on Automated Deduction, Springer LNCS 230, 1986, p. 128\u2013140.","journal-title":"LNCS"},{"key":"34_CR12","unstructured":"H. Comon: Private communications. 1987\/88."},{"key":"34_CR13","unstructured":"H. Comon: Unification et Disunification. Th\u00e9orie et Applications. Thesis (in French), Universit\u00e9 de Grenoble, 1988."},{"key":"34_CR14","unstructured":"H. Comon & P. Lescanne: Equational Problems and Disunification. Universit\u00e9 de Grenoble and Centre de Rech.en Inform. de Nancy, 1988."},{"key":"34_CR15","first-page":"194","volume":"170","author":"F. Fages","year":"1984","unstructured":"F. Fages: Associative-Commutative Unification. Proc. of 7th Conf. on Automated Deduction, Springer, LNCS 170, 1984, p. 194\u2013208.","journal-title":"LNCS"},{"key":"34_CR16","first-page":"205","volume":"159","author":"F. Fages","year":"1983","unstructured":"F. Fages & G. Huet: Complete Sets of Unifiers and Matchers in Equational Theories. Proc. of CAAP'83, Springer, LNCS 159, 1983, p. 205\u2013220; see also J. of Theoret. Comp. Sci. 43, 1986, p. 189\u2013200.","journal-title":"LNCS"},{"key":"34_CR17","first-page":"381","volume":"202","author":"A. Fortenbacher","year":"1985","unstructured":"A. Fortenbacher: An Algebraic Approach to Unification under Associativity and Commutativity. Proc. of Conf. on Rewriting Techniques and Applications, Springer, LNCS 202, 1985, p. 381\u2013397.","journal-title":"LNCS"},{"key":"34_CR18","unstructured":"J. Gallier & S. Raatz: SLD-Resolution Methods for Horn Clauses with Equality Based on E-Unification. Proc. of Int. Symp. on Logic Programming, 1986"},{"key":"34_CR19","unstructured":"J.A. Goguen & J. Meseguer: EQLOG \u2014 Equality, Types, and Generic Modules for Logic Programming. In: Logic Programming: Functions, Relations, and Equations. Prentice Hall, 1986, p. 295\u2013363."},{"key":"34_CR20","doi-asserted-by":"crossref","unstructured":"G. Gr\u00e4tzer: Universal Algebra. Springer, 1979.","DOI":"10.1007\/978-0-387-77487-9"},{"key":"34_CR21","doi-asserted-by":"crossref","unstructured":"A. Herold: Combination of Unification Algorithms. Proc. of 8th Conf. on Automated Deduction, Springer, LNCS 230, 1986.","DOI":"10.1007\/3-540-16780-3_111"},{"key":"34_CR22","unstructured":"A. Herold: Combination of Unification Algorithms in Equational Theories. Dissertation, Universit\u00e4t Kaiserslautern, 1987."},{"key":"34_CR23","doi-asserted-by":"crossref","unstructured":"A. Herold & J.H. Siekmann: Unification in Abelian Semigroups. MEMO-SEKI, Universit\u00e4t Kaiserslautern, 1986.","DOI":"10.1007\/BF00243791"},{"key":"34_CR24","unstructured":"A. Herold, J.H. Siekmann & M.E. Stickel: Benchmarks for AC-Unification. Private communication, 1987."},{"key":"34_CR25","doi-asserted-by":"crossref","unstructured":"G. Huet & D.C. Oppen: Equations and Rewrite Rules: A Survey. In: Formal Languages: Perspectives and Open Problems. (ed. R. Book), Academic Press, 1980.","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"key":"34_CR26","unstructured":"J.M. Hullot: Compilation des Formes Canoniques dans des Th\u00e9ories Equationelles. Th\u044dse (in French), Universit\u00e9 de Paris-Sud, 1980"},{"key":"34_CR27","unstructured":"J. Jaffar, J.-L. Lassez & M. Maher: Logic Programming Language Scheme. In: Logic Programming: Functions, Relations, Equations. (eds. D. DeGroot, G. Lindstrom), Prentice Hall, 1986."},{"key":"34_CR28","doi-asserted-by":"crossref","unstructured":"J.P. Jouannaud & H. Kirchner: Completion of a Set of Rules Modulo a Set of Equations. Proc. of 11th ACM Conf. on Principles of Programming Languages, 1984.","DOI":"10.1145\/800017.800519"},{"key":"34_CR29","unstructured":"C. Kirchner: Methodes et Outils de Conception Systematique d'Algorithmes d'Unification dans les Th\u00e9ories Equationnelles. Th\u00e8se de Doctorat d'Etat (in French), Universit\u00e9 de Nancy, 1985."},{"key":"34_CR30","doi-asserted-by":"crossref","unstructured":"C. Kirchner & H. Kirchenr. Implementation of a General Completion Procedure Parametrized by Built-in Theories and Strategies. Proc. of EUROCAL Conf., 1985.","DOI":"10.1007\/3-540-15984-3_296"},{"key":"34_CR31","unstructured":"C. Kirchner & P. Lescanne: Solving Disequations. Proc. IEEE 2nd Symp. on Logic in Comp. Sci., 1987."},{"key":"34_CR32","volume-title":"Decision Procedures for Simple Equational Theories with Commutative-Associative Axioms: Complete Sets of Commutative-Associative Reductions. Internal Report","author":"D. Lankford","year":"1977","unstructured":"D. Lankford & R.M. Ballantyne: Decision Procedures for Simple Equational Theories with Commutative-Associative Axioms: Complete Sets of Commutative-Associative Reductions. Internal Report, University of Texas, Austin, 1977."},{"key":"34_CR33","doi-asserted-by":"crossref","unstructured":"J.-L. Lassez, M.J. Maher & K. Marriot: Unification Revisited. Technical Report, IBM Yorktown Heights, 1987.","DOI":"10.1016\/B978-0-934613-40-8.50019-1"},{"key":"34_CR34","unstructured":"M. Livesey & J.H. Siekmann: Unification of AC-Terms (Bags) and ACI-Terms (Sets). Int. Report, Essex University, 1975, and Universit\u00e4t Karlsruhe, 1976."},{"issue":"1","key":"34_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF00381143","volume":"3","author":"H.J. Ohlbach","year":"1987","unstructured":"H.J. Ohlbach: Link Inheritance in Abstract Clause Graphs. J. of Automated Reasoning, Vol 3, No 1, 1987, p. 1\u201334.","journal-title":"J. of Automated Reasoning"},{"issue":"2","key":"34_CR36","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1145\/322248.322251","volume":"28","author":"G.E. Peterson","year":"1981","unstructured":"G.E. Peterson & M.E. Stickel: Complete Sets of Reductions for Equational Theories with Complete Unification Algorithms. JACM, Vol 28, No 2, 1981, p. 322\u2013364.","journal-title":"JACM"},{"key":"34_CR37","first-page":"73","volume":"7","author":"G. Plotkin","year":"1972","unstructured":"G. Plotkin: Building in Equational Theories. Machine Intelligence 7, 1972, p. 73\u201390.","journal-title":"Machine Intelligence"},{"issue":"1","key":"34_CR38","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"J.A. Robinson: A Machine Oriented Logic Based on the Resolution Principle. JACM, Vol 12, No 1, 1965, p. 23\u201341.","journal-title":"JACM"},{"key":"34_CR39","unstructured":"M. Schmidt-Schau\u00df: Combination of Unification Algorithms in Arbitrary Disjoint Equational Theories. SEKI-Report, Universit\u00e4t Kaiserslautern, 1987, also in this proceedings."},{"key":"34_CR40","unstructured":"J.H. Siekmann: Unification and Matching Problems. PH.D. Thesis, Essex University, 1978."},{"key":"34_CR41","unstructured":"J.H. Siekmann: Unification Theory. A Survey. J. of Symb. Comp., Special Issue on Unification (ed. C. Kirchner), 1987."},{"key":"34_CR42","unstructured":"J.H. Siekmann & P. Szabo: The Undecidability of the DA-unification Problem. SEKI-Report SR-86-19, Universit\u00e4t Kaiserslautern, 1986."},{"key":"34_CR43","unstructured":"G. Smolka, W. Nutt, J.A. Goguen & J. Meseguer: Order-Sorted Equational Computation. SEKI-Report, Universit\u00e4t Kaiserslautern, 1987."},{"key":"34_CR44","doi-asserted-by":"crossref","unstructured":"M.E. Stickel: A Complete Unification Algorithm for Associative-Commutative Functions. Proc. of 4th Int. Joint Conf. on Art. Intelligence, Tblisi, 1975, p. 71\u201382.","DOI":"10.21236\/ADA015846"},{"key":"34_CR45","unstructured":"M.E. Stickel: Unification Algorithms for Artificial Intelligence. Ph. D. Thesis, Carnegie-Mellon University, 1976."},{"issue":"3","key":"34_CR46","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1145\/322261.322262","volume":"28","author":"M.E. Stickel","year":"1981","unstructured":"M.E. Stickel: A Unification Algorithm for Associative-Commutative Functions. JACM, Vol 28, No 3, 1981, p. 423\u2013434.","journal-title":"JACM"},{"key":"34_CR47","first-page":"248","volume":"170","author":"M.E. Stickel","year":"1984","unstructured":"M.E. Stickel: A Case Study of Theorem Proving by the Knuth-Bendix Method Discovering that X 3 = X implies Ring Commutativity. Proc. of 7th Conf. on Automated Deduction, Springer, LNCS 170, 1984, p. 248\u2013258.","journal-title":"LNCS"},{"issue":"3","key":"34_CR48","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1007\/BF00243792","volume":"3","author":"M.E. Stickel","year":"1987","unstructured":"M.E. Stickel: A Comparison of the Variable-Abstraction and Constant-Abstraction Methods for Associative-Commutative Unification. J. of Automated Reasoning, Vol 3, No 3, 1987, p. 285\u2013289.","journal-title":"J. of Automated Reasoning"},{"key":"34_CR49","unstructured":"P. Szabo: Unifikationstheorie erster Ordnung. (In German), Dissertation, Universit\u00e4t Karlsruhe, 1982."},{"key":"34_CR50","unstructured":"W. Taylor: Equational Logic. Houston Journal of Mathematics 5, 1979."},{"key":"34_CR51","unstructured":"L. Wos, R. Overbeek, E. Lusk, J. Boyle: Automated Reasoning \u2014 Introduction and Applications. Prentice Hall, 1984."}],"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\/BFb0012853","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,5]],"date-time":"2023-05-05T15:35:12Z","timestamp":1683300912000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0012853"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354019343X"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/bfb0012853","relation":{},"subject":[]}}