On solving equations and disequations

ABSTRACT

We are interested in the problem of solving a system<si=ti:1≤i≤n,pj≠qj:1≤j≤m> of equations and disequations, also known as disunification. Solutions to disunification problems are substitutions for the variables of the problem that make the two terms of each equation equal, but leave those of the disequations different. We investigate this in both algebraic and logical contexts where equality is defined by an equational theory and more generally by a definitive clause equality theory E. We show how E-disunification can be reduced to E-unification, that is, solving equations only, and give a disunification algorithm for theories given a unification algorithm. In fact, this result shows that for theories in which the solutions of all unification problems can also be represented finitely. We sketch how disunification can be applied to handle negation in logic programming with equality in a similar style to Colmerauer's logic programming with rational trees, and to represent many solutions to AC-unification problems by a few solutions to ACI-disunification problems.

REFERENCES

• 1: Franz Baader, The theory of idempotent semigroups is of unification type zero, Journal of Automated Reasoning, v.2 n.3, p.283-286, Aug. 1987 [doi>10.1007/BF02328451]
• 2: ~BIRKHOFF, G. 1935. On the structure of abstract algebra. Proc. Cambridge Phil. Soc. 31, ~433 454.
• 3: ~BUNTINE, W. 1986. A theory of equations, inequations and solutions for logic programming. ~Unpublished manuscript, New South Wales Institute of Technology, New South Wales, Aus- ~tralia.
• 4: Wray Buntine, Generalized subsumption and its applications to induction and redundancy, Artificial Intelligence, v.36 n.2, p.149-176, September 1988 [doi>10.1016/0004-3702(88)90001-X]
• 5: Hans-Jürgen Bürckert, Lazy Theory Unification inProlog: An Extension of the warren Abstract machine, GWAI-86 und 2. Österreichische Artificial-Intelligence-Tagung, p.277-288, September 22-26, 1986
• 6: Hans-Jürgen Bürckert, Solving Disequations in Equational Theories, Proceedings of the 9th International Conference on Automated Deduction, p.517-526, May 23-26, 1988
• 7: H.-J. Bürckert, Matching—A special case of unification?, Journal of Symbolic Computation, v.8 n.5, p.523-536, Nov. 1989 [doi>10.1016/S0747-7171(89)80057-4]
• 8: ~BORCKERT, H.-J. 1991. A Resolution Pnnciple for a Logic wtth restricted Quanttfiers. Lecture ~Notes in Artificial Intelligence, vol. 568. Springer-Verlag, New York.
• 9: Hans-Jürgen Bürckert, A resolution principle for constrained logics, Artificial Intelligence, v.66 n.2, p.235-271, April 1994 [doi>10.1016/0004-3702(94)90027-2]
• 10: Hans-Jürgen Bürckert , Alexander Herold , Deepak Kapur , Jórg H. Siekmann , Mark E. Stickel , Michael Tepp , Hantao Zhang, Opening the AC-unification race, Journal of Automated Reasoning, v.4 n.4, p.465-474, Dec. 1988 [doi>10.1007/BF00297251]
• 11: Hans-Jürgen Bürckert , Alexander Herolod , Manfred Schmidt-Schauss, On equational theories, unification, and (Un)decidability, Journal of Symbolic Computation, v.8 n.1-2, p.3-49, Jul./Aug. 1989 [doi>10.1016/S0747-7171(89)80021-5]
• 12: ~BORCKERT, H.-J. AND SCH1MIDT-SCHAUB, M. 1989. Some solvability results for equational prob- ~lems. SEKI-Report SR-89-07, Universit~it Kaiserslautern, Kaiserslautern, Germany.
• 13: ~BURRIS, S., AND SANKAPPANAVAR, H. P. 1979. A Course in Unicersal Algebra. Springer-Vertag, ~New York.
• 14: Wolfram Büttner, Unification in datastructure multisets, Journal of Automated Reasoning, v.2 n.1, p.75-88, 1986
• 15: Chin-Liang Chang , Richard C. Lee , Richard Char-Tung Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, Inc., Orlando, FL, 1997
• 16: ~CLARK, K. L. 1978. Negation as Failure. In Logic and Databases, H. Gallaire and J. Minker, eds. ~Plenum Press, New York, pp. 293 322.
• 17: ~COLMERAUER, A. 1984. Equations and inequations on finite and infinite trees. In Proceedings of ~the International Conference on Fifth Generation Computer Systems, ICOT, pp. 85-99.
• 18: H Comon, Sufficient completeness, term rewriting systems and “anti-unification”, Proc. of the 8th international conference on Automated deduction, p.128-140, August 1986, Oxford, United Kingdom
• 19: ~COMON, H. 1988. Unification et Disunification. Th~orie et applications. Thesis (in French). ~Universit~ de Grenoble, Grenoble, France.
• 20: ~COMON, H. 1991. Disunification: A survey. In Essays in Honour of Alan Robinson (J.-L. Lassez ~and G. Plotkin, Eds.). MIT Press, Cambridge, Mass.
• 21: Hubert Comon , Pierre Lescanne, Equational problems and disunification, Journal of Symbolic Computation, v.7 n.3-4, p.371-425, March/April 1989 [doi>10.1016/S0747-7171(89)80017-3]
• 22: ~FAGES, F. 1983. Formes Canoniques dans les Alg~bres Bool~ennes, et Application h la D~mon- ~stration Automatique en Logique de Premier Ordre. Th~se de 3~me Cycle (in French). Univ. ~Paris VL Paris, France.
• 23: FAGES, F. 1985. Associative-communicative unification. Tech. Rep., INRIA, France.
• 24: F Fages , G Huet, Complete sets of unifiers and matchers in equational theories, Theoretical Computer Science, v.43 n.2-3, p.189-200, July 1986
• 25: ~FERNANDEZ, M. 1992. Narrowing based approaches for equational disunification. App. Algebra ~ Eng. Commun. Comput.
• 26: Albrecht Fortenbacher, An algebraic approach to unification under associativity and commutativity, Proc. of the first international conference on Rewriting techniques and applications, p.381-397, December 1985, Dijon, France
• 27: Jean H. Gallier, Logic for computer science: foundations of automatic theorem proving, Harper & Row Publishers, Inc., New York, NY, 1985
• 28: ~GALLIER, J. H., AND RAATZ, S. 1986. SLD-resolution methods for Horn clauses with equality ~based on E-unification. In Proceedings of the Internattonal Sympostum on Logic Programming
• 29: Michael R. Genesereth , Nils J. Nilsson, Logical foundations of artificial intelligence, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1987
• 30: ~GOGUEN, J. A. 1989. What is unification? In Resohttzon of Equatzons tit ,4lgcbratc Stnwtures (H. ~Ait-Kaci and M. Nivat, eds.). Academic Press, Orlando, Fla. pp. 217-262.
• 31: ~GOGUEN, J. A., AND MESEGUER, J. 1984. Equality, types, modules, and generics for logic ~programming. In Proceedings of 2nd International Logic Proglummmg Confcretlce (Uppsala), pp. ~115-125.
• 32: ~GOGUEN, J. A., AND MF~SEGUUR, J. 1986. EQLOG--Equality, types, and generic modules for ~logic programming. In Logic Programming: Functions, Relations, and Equations. D. DeGroot, ~and G. Lindstrom, eds. Prentice-Hall, Englewood Cliffs, N.J., pp. 295 363. ~GR3.TZER, G. 1979. UnwersalAlgebra. Sprlnger-Verlag, New York, 1979.
• 33: A Herold, Combination of unification algorithms, Proc. of the 8th international conference on Automated deduction, p.450-469, August 1986, Oxford, United Kingdom
• 34: ~HEROLD, A. 1987. Combination of unification algorithms in equational theories. Dissertation. ~Univ. Kaiserslautern, Kaiserslautern, Germany.
• 35: ~HEROLD, m., AND SIEKMANN, J. H. 1986. Unification in abelian semigroups. MEMO-SEKI Univ. ~ Kaiserslautern, Kaiserslautern, Germany.
• 36: ~HOHFELD, M., AND SMOLKA, G. 1988. Definite relations over constraint languages. LILOG-rep. ~ 53. IBM Germany, Stuttgart, Germany.
• 37: ~HUET, G., AND OPPEN, D. C. 1980. Equations and rewrite rules: A survey. In Formal Lang,ages' ~PerspectiL,e and Open Problems. R. Book, ed. Academic Press, Orlando, Fla.
• 38: ~HULLOT, J. M. 1980. Compilation des Formes Canoniqucs dans de Thdones equationelles. ~Thase du 3ame Cycle (in French). Univ. Paris-Sud, Paris, France.
• 39: J. Jaffar , J.-L. Lassez, Constraint logic programming, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.111-119, January 21-23, 1987, Munich, West Germany [doi>10.1145/41625.41635]
• 40: ~JAFFAR, J., LASSEZ, J.-L., AND MAHER, M. 1984. A theory of complete logic programming with ~ equality. In Proceeding~ of the Confi'rence on Fifth Generation Computing &'stems. ICOT, pp. ~175 184.
• 41: ~jAFFER, J., LASSEZ, J.-L., AND MAHER, M. 1986. Logic programming language scheme. In Logic ~Programming: Functions, Relations, Equations D. Degroot and G. Lindstrom, eds. Prentice-Hall, ~Englewood Cliffs, N.J.
• 42: Joxan Jaffar , Peter J Stuckey, Logic program semantics for programming with equations, Proceedings on Third international conference on logic programming, p.313-326, September 1986, London, United Kingdom
• 43: Jean-Pierre Jouannaud , Helene Kirchner, Completion of a set of rules modulo a set of equations, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.83-92, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800519]
• 44: ~JOUANNAUD, J.-P., AND KIRCHNER, C. 1991. Solving equations in abstract algebras: A rule-based ~survey of unification. In Essm's in Honour of Alan Robinson J.-L. Lassez and G. Plotkin, eds. ~ MIT Press, Cambridge, Mass.
• 45: ~ICdRCHNER, C. 1985. Methodes et Outlls de Conception Systematique d'Algorithmes d'Unifica- ~tions dans les Theories Equationelles. Thase de Doctorat d'Etat (In French). Umv. Nancy, ~Nancy, France.
• 46: ~KIRCHNER, C., ED. 1990. Umfication. Academic Press, Orlando, Fla. (See also special issue on ~unification of J. Syrnb. Cornput. 7&8. (1989).)
• 47: ~KIP, C!4NI2R, C., AND LE~CANNE, P. 1987. Solving disequations. In Proceedbz~ of tile 2nd IEEE ~Symposium in Computer Science. IEEE, New York, pp. 347-352.
• 48: Kevin Knight, Unification: a multidisciplinary survey, ACM Computing Surveys (CSUR), v.21 n.1, p.93-124, March 1989 [doi>10.1145/62029.62030]
• 49: ~LANKFORD, D., AND BALLANTYNE, Px. M. 1977. Decision procedures for simple equational ~theories with commutative-associative axioms: Complete sets of commutative-associative reduc- ~tions. Internal Re. Univ. Texas at Austin, Austin, Tex.
• 50: J.-L. Lassez , M. J. Maher , K. Marriott, Unification revisited, Foundations of deductive databases and logic programming, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1988
• 51: ~LIVESEY, M., AND SIEKMANN, J. H. 1975/1976. Unification of AC-terms (bags) and ACI-terms ~ (sets). Internal rep. Univ. Essex, Essex, England, (1975) and Univ. Karlsruhe, Karlsruhe, ~ Germany (1976).
• 52: ~LLO'tD, J. W. 1984. Fotmdatlons of Logic Programming. SprInger-Verlag, New York.
• 53: ~LLOYD, J. W., AND TOPOR, R. 1984. Making Prolog more expressive. Tech. Rep. 84-8. Univ. ~Melbourne, Melbourne, Australia.
• 54: ~LuICiUEZ, D. 1989. A deduction procedure for first order programs. In Proceedings of the ~lntertlational ConJbrence ol~ Logic Programming.
• 55: Werner Nutt , Pierre Réty , Gert Smolka, Basic narrowing revisited, Journal of Symbolic Computation, v.7 n.3-4, p.295-317, March/April 1989 [doi>10.1016/S0747-7171(89)80014-8]
• 56: Gerald E. Peterson , Mark E. Stickel, Complete Sets of Reductions for Some Equational Theories, Journal of the ACM (JACM), v.28 n.2, p.233-264, April 1981 [doi>10.1145/322248.322251]
• 57: ~PLOTKtN, G. D. 1970. A note on inductive generalization. Mach. Int. 5, 153-163.
• 58: ~PLOTKIN, G. D. 1972. Building in equational theories. Mach. Int. 7, 73-90.
• 59: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• 60: D E Rydeheard , R M Burstall, A categorical unification algorithm, Proceedings of a tutorial and workshop on Category theory and computer programming, p.493-505, November 1986, Guildford, United Kingdom
• 61: Manfred Schmidt-Schauss, Unification under associativity and idempotence is of type nullary, Journal of Automated Reasoning, v.2 n.3, p.277-281, Aug. 1987 [doi>10.1007/BF02328450]
• 62: Manfred Schmidt-Schaub, Unification in a combination of arbitrary disjoint equational theories, Journal of Symbolic Computation, v.8 n.1-2, p.51-99, Jul./Aug. 1989 [doi>10.1016/S0747-7171(89)80022-7]
• 63: ~SHOk. NFIELD, J. R. 1967. Mathematical Logtc. Addison-Wesley, Reading Mass.
• 64: ~SIEKMANN, J, H. 1978. Unification and matching problems. Ph.D dissertation, Univ. Essex, ~Essex, England.
• 65: Jörg H. Siekmann, Unification theory, Journal of Symbolic Computation, v.7 n.3-4, p.207-274, March/April 1989 [doi>10.1016/S0747-7171(89)80012-4]
• 66: ~S1EKMANN, J. m., AND SZABO, P. 1981. Universal unification and regular ACFM theories. In ~Proceedings of IJCAI.
• 67: ~SIEKMANN, J. H., AND SZABO~ P. 1988. The undecidability of the DA-unification problem. J. ~ Symb. Logic'.
• 68: ~SMOLKA, G., NUTF, W., GOGUEN, J. A., AND MESEGUER, J. 1989. Order-Sorted equational ~ computation. In Resolution of Equattons in Algebraic Stl~tctures (H. Ait-Kaci and M. Nivat, eds.) ~ Prentice-Hall, Englewood Chffs, N.J.
• 69: ~STICKEL, M. E. 1975. A complete unification algorithm for associative-commutative functions. In ~ Proceedings of the 4th Intemattonal Joblt Conference on ArtifictaI Intelligence (Tblisi). pp. 71-82.
• 70: ~STICKEL, M. E. 1976. Unification algorithms for artificial intelligence, Ph.D dissertation. ~Carnegie-Mellon Univ., Pittsburgh, Pa.
• 71: Mark E. Stickel, A Unification Algorithm for Associative-Commutative Functions, Journal of the ACM (JACM), v.28 n.3, p.423-434, July 1981 [doi>10.1145/322261.322262]
• 72: Mark E. Stickel, A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering That x³=x Implies Ring Commutativity, Proceedings of the 7th International Conference on Automated Deduction, p.248-258, May 14-16, 1984
• 73: Mark E. Stickel, A comparison of the variable-abstraction and constant-abstraction methods for associative-commutative unification, Journal of Automated Reasoning, v.3 n.3, p.285-289, Sept. 1987
• 74: ~SZABO, P. 1982. UnJfikationstheorie erster Ordnung. Dissertation (in German). Univ. Karlsruhe, ~Karlsruhe, Germany.
• 75: ~TARSKI, A. 1946. A remark on functionally free algebras. Ann. Math. 2, 47, 163-165.
• 76: ~TAYLOR, W. 1979. Equational logic. Hou. J. Math 5,
• 77: Pascal Van Hentenryck, Constraint satisfaction in logic programming, MIT Press, Cambridge, MA, 1989
• 78: Larry Wos , Ross Overbeek , Ewing Lusk , Jim Boyle, Automated reasoning (2nd ed.): introduction and applications, McGraw-Hill, Inc., New York, NY, 1992

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Logic and constraint programming

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Computational logic

General Terms:
Languages, Theory

Keywords:
E-disunification, E-unification equational theory, definite clause, inequations, logic programming, solving equations and disequations