Dis-unification, in
computer science
Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied science, ...
and
logic
Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the study of deductively valid inferences or logical truths. It examines how conclusions follow from premises based on the structure o ...
, is an algorithmic process of solving
inequation
In mathematics, an inequation is a statement that either an ''inequality'' (relations "greater than" and "less than", ) or a relation "not equal to" (≠) holds between two values. It is usually written in the form of a pair of expressions den ...
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
First-order logic, also called predicate logic, predicate calculus, or quantificational logic, is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over ...
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, specifically automated reasoning, unification is an algorithmic process of solving equations between symbolic expression (mathematics), expressions, each of the form ''Left-hand side = Right-hand side''. For example, ...
: 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 claus ...
: incorporating solving algorithms for particular classes of inequalities (and other relations) into
Prolog
Prolog is a logic programming language that has its origins in artificial intelligence, automated theorem proving, and computational linguistics.
Prolog has its roots in first-order logic, a formal logic. Unlike many other programming language ...
*
Constraint programming
Constraint programming (CP) is a paradigm for solving combinatorial problems that draws on a wide range of techniques from artificial intelligence, computer science, and operations research. In constraint programming, users declaratively state t ...
: solving algorithms for particular classes of inequalities
*
Simplex algorithm
In mathematical optimization, Dantzig's simplex algorithm (or simplex method) is a popular algorithm for linear programming.
The name of the algorithm is derived from the concept of a simplex and was suggested by T. S. Motzkin. Simplices are ...
: solving algorithm for linear inequations
*
Inequation
In mathematics, an inequation is a statement that either an ''inequality'' (relations "greater than" and "less than", ) or a relation "not equal to" (≠) holds between two values. It is usually written in the form of a pair of expressions den ...
: kinds of inequations in mathematics in general, including a brief section on
solving
*
Equation solving
In mathematics, to solve an equation is to find its solutions, which are the values (numbers, functions, sets, etc.) that fulfill the condition stated by the equation, consisting generally of two expressions related by an equals sign. When s ...
: how to solve equations in mathematics
Logic programming
Theoretical computer science
Unification (computer science)
{{comp-sci-theory-stub