Dis-unification, in
computer science
Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to Applied science, practical discipli ...
and
logic
Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premises ...
, is an algorithmic process of solving
inequation
In mathematics, an inequation is a statement that an inequality holds between two values. It is usually written in the form of a pair of expressions denoting the values in question, with a relational sign between them indicating the specific ine ...
s between symbolic
expressions.
Publications on dis-unification
*
*
"Anti-Unification" here refers to inequation-solving, a naming which nowadays has become quite unusual, cf.
Anti-unification (computer science).
*
*
*
*
*
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.
*
*
See also
*
Unification (computer science) In logic and computer science, unification is an algorithmic process of solving equations between symbolic expressions.
Depending on which expressions (also called ''terms'') are allowed to occur in an equation set (also called ''unification prob ...
: solving equations between symbolic expressions
*
Constraint logic programming
Constraint logic programming is a form of constraint programming, in which logic programming is extended to include concepts from constraint satisfaction. A constraint logic program is a logic program that contains constraints in the body of clau ...
: 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
In mathematics, an inequation is a statement that an inequality holds between two values. It is usually written in the form of a pair of expressions denoting the values in question, with a relational sign between them indicating the specific ine ...
: kinds of inequations in mathematics in general, including a brief section on
solving
*
Equation solving: how to solve equations in mathematics
Logic programming
Theoretical computer science
Unification (computer science)
{{comp-sci-theory-stub