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:
“The definition of good prose is proper words in their proper places; of good verse, the most proper words in their proper places. The propriety is in either case relative. The words in prose ought to express the intended meaning, and no more; if they attract attention to themselves, it is, in general, a fault.”
—Samuel Taylor Coleridge (1772–1834)
“No man, not even a doctor, ever gives any other definition of what a nurse should be than this—”devoted and obedient.” This definition would do just as well for a porter. It might even do for a horse. It would not do for a policeman.”
—Florence Nightingale (1820–1910)
“Though living is a dreadful thing
And a dreadful thing is it
Life the niggard will not thank,
She will not teach who will not sing,
And what serves, on the final bank,
Our logic and our wit?”
—Philip Larkin (1922–1986)