| 释义 |
- Publications on dis-unification
- See also
Dis-unification, in computer science and logic, is an algorithmic process of solving inequations between symbolic expressions. Publications on dis-unification- {{cite book| author=Alain Colmerauer| authorlink=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 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 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| editor2link=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| editor=| series=LNCS| contributionurl=http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/comon-icalp91.pdf| accessdate=29 June 2013}}
See also- 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
{{comp-sci-theory-stub}} 3 : Logic programming|Theoretical computer science|Unification (computer science) |