# Dis-unification

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Dis-unification
> Markdown URL: https://mediated.wiki/source/Dis-unification.md
> Source: https://en.wikipedia.org/wiki/Dis-unification
> Source revision: 1258126052
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

{{Short description|Solving symbolic inequations}}
{{Dicdef|date=November 2024}}
'''Dis-unification''', in [computer science](/source/computer_science) and [logic](/source/logic), is an algorithmic process of solving [inequation](/source/inequation)s between symbolic [expressions](/source/expression_(mathematics)).

==Publications on dis-unification==
* {{cite book| author=Alain Colmerauer| author-link=Alain Colmerauer| chapter=Equations and Inequations on Finite and Infinite Trees| title=Proc. Int. Conf. on Fifth Generation Computer Systems| year=1984| pages=85–99| editor=ICOT}}
* {{cite book| author=Hubert Comon| chapter=Sufficient Completeness, Term Rewriting Systems and 'Anti-Unification'| title=Proc. 8th International Conference on Automated Deduction| year=1986| volume=230| pages=128–140| publisher=Springer| series=[LNCS](/source/LNCS)}}<BR>"Anti-Unification" here refers to inequation-solving, a naming which nowadays has become quite unusual, cf. [Anti-unification (computer science)](/source/Anti-unification_(computer_science)). 
* {{cite book | author1 = Claude Kirchner | author2 = Pierre Lescanne | chapter = Solving Disequations | title = Proc. [LICS](/source/Symposium_on_Logic_in_Computer_Science) | year = 1987 | pages = 347–352}}
* {{cite report | url=https://hal.inria.fr/inria-00075867 | author=Claude Kirchner and Pierre Lescanne | title=Solving disequations | institution=INRIA | type=Research Report | number=RR-0686 | year=1987 }}
* {{cite thesis| type=Ph.D.| author=Hubert Comon| title=Unification et disunification: Théorie et applications| year=1988| publisher=I.N.P. de Grenoble|url=http://hal.inria.fr/docs/00/33/12/63/PDF/Comon.Hubert_1988_these.pdf}}
* {{cite journal | author1 = Hubert Comon | author2 = Pierre Lescanne | title = Equational Problems and Disunification | journal = [J. Symb. Comput.](/source/J._Symb._Comput.)| volume  = 7 | number = 3–4 | pages = 371–425 | date = Mar–Apr 1989 | doi = 10.1016/S0747-7171(89)80017-3 | doi-access = free | citeseerx = 10.1.1.139.4769 }}
* {{cite book| author=Comon, Hubert| chapter=Equational Formulas in Order-Sorted Algebras| title=Proc. ICALP| year=1990}}<BR>Comon shows that the [first-order logic](/source/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](/source/sufficient_completeness) of [term rewriting systems](/source/Term_rewriting).
* {{cite book|  title=Computational Logic — Essays in Honor of [Alan Robinson](/source/John_Alan_Robinson)| editor1=Jean-Louis Lassez |editor2= Gordon Plotkin| editor2-link=Gordon Plotkin| author=Hubert Comon| contribution=Disunification: A Survey| year=1991| pages=322–359| publisher=MIT Press |contribution-url=http://www.lsv.ens-cachan.fr/~comon/ftp.articles/disunification.ps}}
* {{cite book| author=Hubert Comon| chapter=Complete Axiomatizations of some Quotient Term Algebras| title=Proc. 18th Int. Coll. on Automata, Languages, and Programming| year=1993| volume=510| pages=148–164| publisher=Springer| series=LNCS| contribution-url=http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/comon-icalp91.pdf| accessdate=29 June 2013}}

==See also==
* [Unification (computer science)](/source/Unification_(computer_science)): solving equations between symbolic expressions
* [Constraint logic programming](/source/Constraint_logic_programming): incorporating solving algorithms for particular classes of inequalities (and other relations) into [Prolog](/source/Prolog)
* [Constraint programming](/source/Constraint_programming): solving algorithms for particular classes of inequalities
* [Simplex algorithm](/source/Simplex_algorithm): solving algorithm for linear inequations
* [Inequation](/source/Inequation): kinds of inequations in mathematics in general, including a brief section on [solving](/source/Inequation)
* [Equation solving](/source/Equation_solving): how to solve equations in mathematics

Category:Logic programming
Category:Theoretical computer science
Category:Unification (computer science)

{{comp-sci-theory-stub}}

---
Adapted from the Wikipedia article [Dis-unification](https://en.wikipedia.org/wiki/Dis-unification) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Dis-unification?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.