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}}
  "Anti-Unification" here refers to inequation-solving, a naming which nowadays has become quite unusual, cf. Anti-unification (computer science).
• {{cite book | author1 = Claude Kirchner | author2 = Pierre Lescanne | chapter = Solving Disequations | title = Proc. LICS | 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.| 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}}
  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.
• {{cite book| title=Computational Logic — Essays in Honor of 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}}

• 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

Category:Logic programming

Category:Theoretical computer science

Category:Unification (computer science)

{{comp-sci-theory-stub}}