unification
In plain wordsFinding values for the blanks in two logical patterns so that they become identical, for example matching 'parent(X, bob)' with 'parent(alice, Y)' by setting X to alice and Y to bob.
An algorithm that, given two terms or atomic formulas containing variables, finds a substitution — an assignment of terms to variables — that makes them syntactically identical, or reports that none exists. Whenever two expressions are unifiable they have a most general unifier (MGU), from which every other unifier can be obtained by further substitution. Unification is the matching step in resolutionresolution, n.: A mechanical step of logical reasoning: from 'A or B' and 'not A or C', conclude 'B or C'. Repeating it can demonstrate any conclusion that genuinely follows from what is known. theorem proving and in PrologProlog, prop. n.: A programming language from 1972 in which you state facts and rules in logic and then ask questions; the computer finds answers by searching for proofs. execution, and it is central to type inference in programming languages (the Hindley–Milner system) and to term rewriting. The occurs check, which forbids binding a variable to a term that contains it (X = f(X)), prevents infinite structures; Prolog omits it by default for speed. Robinson's original algorithm takes exponential time in the worst case, but later algorithms run in linear or near-linear time.
Origin
Jacques Herbrand sketched a unification procedure in his 1930 thesis. J. Alan Robinson introduced the modern algorithm and the most general unifier as the core of resolution in 1965.
Usage note
Grammar formalisms such as HPSG apply the same operation to feature structures (unification-based grammar). Unrelated to unification in physics or to 'unified' multimodal models.
Related
- resolutionresolution, n.: A mechanical step of logical reasoning: from 'A or B' and 'not A or C', conclude 'B or C'. Repeating it can demonstrate any conclusion that genuinely follows from what is known.
- PrologProlog, prop. n.: A programming language from 1972 in which you state facts and rules in logic and then ask questions; the computer finds answers by searching for proofs.
- logic programminglogic programming, n.: A style of programming in which you write down facts and rules in logic and then ask questions; the computer works out the answers itself by logical deduction.
- first-order logicfirst-order logic, n.: A precise formal language for statements about objects and their relations, using 'for all' and 'there exists', such as 'every person has a mother'. It is the standard logic of mathematics and of classic AI.
- automated theorem provingautomated theorem proving, n.: Getting computers to prove mathematical or logical statements by themselves, by searching for a chain of valid steps that leads from basic assumptions to the statement.
Sources
- Robinson, J. A. (1965). A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM 12(1), 23–41.
Mentioned in
backward chainingbackward chaining, n.: A way of reasoning that starts from the question ('is this true?') and works backward, looking for rules that would prove it and then checking whether their conditions hold., first-order logicfirst-order logic, n.: A precise formal language for statements about objects and their relations, using 'for all' and 'there exists', such as 'every person has a mother'. It is the standard logic of mathematics and of classic AI., logic programminglogic programming, n.: A style of programming in which you write down facts and rules in logic and then ask questions; the computer works out the answers itself by logical deduction., resolutionresolution, n.: A mechanical step of logical reasoning: from 'A or B' and 'not A or C', conclude 'B or C'. Repeating it can demonstrate any conclusion that genuinely follows from what is known.