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.
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. "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.
Claude Kirchner and Pierre Lescanne (1987).
Solving disequations (Research Report). INRIA.
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.
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.
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. "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.
Claude Kirchner and Pierre Lescanne (1987).
Solving disequations (Research Report). INRIA.
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.