On Solving Equations and Disequations

Wray L. Buntine, Hans Jürgen Bürckert

Research output: Contribution to journalArticleResearchpeer-review

14 Citations (Scopus)


We are interested in the problem of solving a system[formula omitted] 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.

Original languageEnglish
Pages (from-to)591-629
Number of pages39
JournalJournal of the ACM
Issue number4
Publication statusPublished - 7 Jan 1994


  • Definite clause
  • E-disunification
  • E-unification
  • equational theory
  • inequations
  • logic programming
  • solving equations and disequations

Cite this