Recently reviewing a blog on knowledge representation and predicate calculus, I noticed the blog writer handled poorly the topic of unification and resolution theorem proving. The writer stated that unification had to with matching Prolog data structures – that is true for the Prolog programming language since unification and resolution are built into the language. At first I thought and understood unification algorithm provided by Luger (1993). Nevertheless, upon reviewing the Unification section, I realized that I missed some the critical points and updated my OneNote Notebook by adding a new page discussing the Unification topic and extracting the important concepts. In addition, I added details to the Unification algorithm.
Before we can be begin the the Unification topic, please review the recommended websites in Wikipedea for the subjects of propositional calculus and predicate calculus. The links are excellent.
Unification and resolution principle was developed and published in 1965 by John Alan Robinson when he was visiting researcher at the Argonne National Laboratory’s Mathematics Division. His paper A machine-oriented logic based on the resolution principle is the basis for all theorem provers and eventually lead to the development of the Prolog programming language.
Basically unification is ability of an inference system to match two expressions. In propositional calculus this task is very trival. However, in predicate calculus, the task is more involved since a number of issues require resolution. Basically, the existential variables require to be set to constants in the logical database. Next, the universal quantifier variables can be computed, if possible. The next issue is if variable is itself in a function, which could lead to infinite assignment – thus the occurs check is required to test this condition. Once a variable is bound, then that assignment must consistent, otherwise, it leads to less generality. Also, there is the issue of composition of variables. Finally, the concept of the most general unifier (mgu).
At last the introduction to the unification algorithm pseudo code. Basically the unify functions requires the two expression be in the form of s-expressions. For example,
p(X) becomes (p X), p(a, f(b, c)) becomes (p a (f b c)).
The above format makes it easier to work with a functional language such as LISP. I enclosed my version of the unify pseudo code:
function unify(s1, s2) returns either { fail, {}, {Unification} }
begin
he1 <- first element of s1
he2 <- first element of s2
if both he1 and he2 are constants and if he1 = he2,
then return {} else return fail.
if he1 is a variable and is present in he2,
then return fail else return {he2/he1}
if he2 is a variable and is repsent in he1,
then return fail else return {he1/he2}
result1 <- unify(he1, he2)
if result1 is fail, then return fail.
apply substitutions from result to rest of s1 and to rest of s2
result2 <- unify(rest s1, rest s2)
return compose result1 result2
end
I have presented the pseudo code for a version of the unify function, which is a generalized symbolic matching algorithm, and have seen various versions of the unify function in the Internet, in Luger(1993), and in Winston and Horn (1989). Finally, much research has been done to make the unification algorithm as linear as possible.
Read More »
