Definition of Unification For First-order Logic
Let p and q be sentences in first-order logic.
- UNIFY(p,q) = U where subst(U,p) = subst(U,q)
Where subst(U,p) means the result of applying substitution U on the sentence p. Then U is called a unifier for p and q. The unification of p and q is the result of applying U to both of them.
Let L be a set of sentences, for example, L = {p,q}. A unifier U is called a most general unifier for L if, for all unifiers U' of L, there exists a substitution s such that applying s to the result of applying U to L gives the same result as applying U' to L:
- subst(U',L) = subst(s,subst(U,L)).
Read more about this topic: Unification (computer Science)
Famous quotes containing the words definition of, definition and/or logic:
“... we all know the wag’s definition of a philanthropist: a man whose charity increases directly as the square of the distance.”
—George Eliot [Mary Ann (or Marian)
“... we all know the wag’s definition of a philanthropist: a man whose charity increases directly as the square of the distance.”
—George Eliot [Mary Ann (or Marian)
“The logic of worldly success rests on a fallacy: the strange error that our perfection depends on the thoughts and opinions and applause of other men! A weird life it is, indeed, to be living always in somebody else’s imagination, as if that were the only place in which one could at last become real!”
—Thomas Merton (1915–1968)