Dis-unification explained

Dis-unification, in computer science and logic, is an algorithmic process of solving inequations between symbolic expressions.

Publications on dis-unification

• Book: Alain Colmerauer. Alain Colmerauer. Equations and Inequations on Finite and Infinite Trees. Proc. Int. Conf. on Fifth Generation Computer Systems. 1984. 85–99. ICOT.
• Book: Hubert Comon. Sufficient Completeness, Term Rewriting Systems and 'Anti-Unification'. Proc. 8th International Conference on Automated Deduction. 1986. 230. 128–140. Springer. LNCS.
  "Anti-Unification" here refers to inequation-solving, a naming which nowadays has become quite unusual, cf. Anti-unification (computer science).
• Book: Claude Kirchner . Pierre Lescanne . Solving Disequations . . 1987 . 347–352.
• Solving disequations . Claude Kirchner and Pierre Lescanne . INRIA . Research Report . RR-0686 . 1987 .
• Ph.D.. Hubert Comon. Unification et disunification: Théorie et applications. 1988. I.N.P. de Grenoble.
• Hubert Comon . Pierre Lescanne . Equational Problems and Disunification . J. Symb. Comput.. 7 . 3–4 . 371–425 . Mar–Apr 1989 . 10.1016/S0747-7171(89)80017-3 . free . 10.1.1.139.4769 .
• Book: Comon, Hubert. Equational Formulas in Order-Sorted Algebras. Proc. ICALP. 1990.
  Comon shows that the first-order logic theory of equality and sort membership is decidable, that is, each first-order logic formula built from arbitrary function symbols, "=" and "∈", but no other predicates, can effectively be proven or disproven. Using the logical negation (¬), non-equality (≠) can be expressed in formulas, but order relations (<) cannot. As an application, he proves sufficient completeness of term rewriting systems.
• Book: Computational Logic — Essays in Honor of Alan Robinson. Jean-Louis Lassez . Gordon Plotkin. Gordon Plotkin. Hubert Comon. Disunification: A Survey. 1991. 322–359. MIT Press . http://www.lsv.ens-cachan.fr/~comon/ftp.articles/disunification.ps.
• Book: Hubert Comon. Complete Axiomatizations of some Quotient Term Algebras. Proc. 18th Int. Coll. on Automata, Languages, and Programming. 1993. 510. 148–164. Springer. LNCS. http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/comon-icalp91.pdf. 29 June 2013.

See also

• Unification (computer science): solving equations between symbolic expressions
• Constraint logic programming: incorporating solving algorithms for particular classes of inequalities (and other relations) into Prolog
• Constraint programming: solving algorithms for particular classes of inequalities
• Simplex algorithm: solving algorithm for linear inequations
• Inequation: kinds of inequations in mathematics in general, including a brief section on solving
• Equation solving: how to solve equations in mathematics