This article appears to be a dictionary definition. (November 2024) |
Dis-unification, in computer science and logic, is an algorithmic process of solving inequations between symbolic expressions.
Publications on dis-unification
edit- Alain Colmerauer (1984). "Equations and Inequations on Finite and Infinite Trees". In ICOT (ed.). Proc. Int. Conf. on Fifth Generation Computer Systems. pp. 85–99.85-99&rft.date=1984&rft.au=Alain Colmerauer&rfr_id=info:sid/en.wikipedia.org:Dis-unification" class="Z3988">
- Hubert Comon (1986). "Sufficient Completeness, Term Rewriting Systems and 'Anti-Unification'". Proc. 8th International Conference on Automated Deduction. LNCS. Vol. 230. Springer. pp. 128–140.128-140&rft.pub=Springer&rft.date=1986&rft.au=Hubert Comon&rfr_id=info:sid/en.wikipedia.org:Dis-unification" class="Z3988">
"Anti-Unification" here refers to inequation-solving, a naming which nowadays has become quite unusual, cf. Anti-unification (computer science). - Claude Kirchner; Pierre Lescanne (1987). "Solving Disequations". Proc. LICS. pp. 347–352.347-352&rft.date=1987&rft.au=Claude Kirchner&rft.au=Pierre Lescanne&rfr_id=info:sid/en.wikipedia.org:Dis-unification" class="Z3988">
- Claude Kirchner and Pierre Lescanne (1987). Solving disequations (Research Report). INRIA.
- Hubert Comon (1988). Unification et disunification: Théorie et applications (PDF) (Ph.D.). I.N.P. de Grenoble.
- Hubert Comon; Pierre Lescanne (Mar–Apr 1989). "Equational Problems and Disunification". J. Symb. Comput. 7 (3–4): 371–425. CiteSeerX 10.1.1.139.4769. doi:10.1016/S0747-7171(89)80017-3.3–4&rft.pages=371-425&rft.date=1989-03/1989-04&rft_id=https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.139.4769#id-name=CiteSeerX&rft_id=info:doi/10.1016/S0747-7171(89)80017-3&rft.au=Hubert Comon&rft.au=Pierre Lescanne&rft_id=https://doi.org/10.1016%2FS0747-7171%2889%2980017-3&rfr_id=info:sid/en.wikipedia.org:Dis-unification" class="Z3988">
- Comon, Hubert (1990). "Equational Formulas in Order-Sorted Algebras". Proc. ICALP.
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. - Hubert Comon (1991). "Disunification: A Survey". In Jean-Louis Lassez; Gordon Plotkin (eds.). Computational Logic — Essays in Honor of Alan Robinson. MIT Press. pp. 322–359.322-359&rft.pub=MIT Press&rft.date=1991&rft.au=Hubert Comon&rft_id=http://www.lsv.ens-cachan.fr/~comon/ftp.articles/disunification.ps&rfr_id=info:sid/en.wikipedia.org:Dis-unification" class="Z3988">
- Hubert Comon (1993). "Complete Axiomatizations of some Quotient Term Algebras" (PDF). Proc. 18th Int. Coll. on Automata, Languages, and Programming. LNCS. Vol. 510. Springer. pp. 148–164. Retrieved 29 June 2013.148-164&rft.pub=Springer&rft.date=1993&rft.au=Hubert Comon&rft_id=http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/comon-icalp91.pdf&rfr_id=info:sid/en.wikipedia.org:Dis-unification" class="Z3988">
See also
edit- 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