Menu
Home
People
Places
Arts
History
Plants & Animals
Science
Life & Culture
Technology
Reference.org
Dis-unification
open-in-new
<h2 id="publications-on-dis-unification">Publications on dis-unification</h2> <ul><li><a href="/facts/Alain_Colmerauer/HzI8opM2">Alain Colmerauer</a> (1984). "Equations and Inequations on Finite and Infinite Trees". In ICOT (ed.). <i>Proc. Int. Conf. on Fifth Generation Computer Systems</i>. pp. 85–99.</li> <li>Hubert Comon (1986). "Sufficient Completeness, Term Rewriting Systems and 'Anti-Unification'". <i>Proc. 8th International Conference on Automated Deduction</i>. <a href="/facts/LNCS/1UeA77BC">LNCS</a>. Vol. 230. Springer. pp. 128–140."Anti-Unification" here refers to inequation-solving, a naming which nowadays has become quite unusual, cf. <a href="/facts/Anti-unification_(computer_science)/cKHhbFtC">Anti-unification (computer science)</a>.</li> <li>Claude Kirchner; Pierre Lescanne (1987). "Solving Disequations". <i>Proc. <a href="/facts/Symposium_on_Logic_in_Computer_Science/j7qwgDmc">LICS</a></i>. pp. 347–352.</li> <li>Claude Kirchner and Pierre Lescanne (1987). <a href="https://hal.inria.fr/inria-00075867">Solving disequations</a> (Research Report). INRIA.</li> <li>Hubert Comon (1988). <a href="http://hal.inria.fr/docs/00/33/12/63/PDF/Comon.Hubert_1988_these.pdf"><i>Unification et disunification: Théorie et applications</i></a> (PDF) (Ph.D.). I.N.P. de Grenoble.</li> <li>Hubert Comon; Pierre Lescanne (Mar–Apr 1989). <a href="https://doi.org/10.1016%2FS0747-7171%2889%2980017-3">"Equational Problems and Disunification"</a>. <i><a href="/facts/J._Symb._Comput./hEnNr3L1">J. Symb. Comput.</a></i> 7 (3–4): 371–425. <a href="/facts/CiteSeerX_(identifier)/SceDmd3c">CiteSeerX</a> <a href="https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.139.4769">10.1.1.139.4769</a>. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1016%2FS0747-7171%2889%2980017-3">10.1016/S0747-7171(89)80017-3</a>.</li> <li>Comon, Hubert (1990). "Equational Formulas in Order-Sorted Algebras". <i>Proc. ICALP</i>.Comon shows that the <a href="/facts/First-order_logic/lcISqWIg">first-order logic</a> 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 <a href="/facts/Term_rewriting/9PHlnnnJ">term rewriting systems</a>.</li> <li>Hubert Comon (1991). <a href="http://www.lsv.ens-cachan.fr/~comon/ftp.articles/disunification.ps">"Disunification: A Survey"</a>. In Jean-Louis Lassez; <a href="/facts/Gordon_Plotkin/2CrnVkVj">Gordon Plotkin</a> (eds.). <i>Computational Logic — Essays in Honor of <a href="/facts/John_Alan_Robinson/k2acEudn">Alan Robinson</a></i>. MIT Press. pp. 322–359.</li> <li>Hubert Comon (1993). <a href="http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/comon-icalp91.pdf">"Complete Axiomatizations of some Quotient Term Algebras"</a> (PDF). <i>Proc. 18th Int. Coll. on Automata, Languages, and Programming</i>. LNCS. Vol. 510. Springer. pp. 148–164. Retrieved 29 June 2013.</li></ul> <h2 id="see-also">See also</h2> <ul><li><a href="/facts/Unification_(computer_science)/4EPHSB1T">Unification (computer science)</a>: solving equations between symbolic expressions</li> <li><a href="/facts/Constraint_logic_programming/b47VLwE9">Constraint logic programming</a>: incorporating solving algorithms for particular classes of inequalities (and other relations) into <a href="/facts/Prolog/r5h66Qh1">Prolog</a></li> <li><a href="/facts/Constraint_programming/rgkCK5bD">Constraint programming</a>: solving algorithms for particular classes of inequalities</li> <li><a href="/facts/Simplex_algorithm/9fndF6cq">Simplex algorithm</a>: solving algorithm for linear inequations</li> <li><a href="/facts/Inequation/BuBq2Bwb">Inequation</a>: kinds of inequations in mathematics in general, including a brief section on <a href="/facts/Inequation/BuBq2Bwb">solving</a></li> <li><a href="/facts/Equation_solving/2RKaXrDM">Equation solving</a>: how to solve equations in mathematics</li></ul>