Logic Programming Prolog

I am reading the book Logic, Programming and Prolog (2nd ed).  After completing the preliminaries chapter, much of the material was familiar since it was defining predicate calculus and logical inferences.  The material is mathematically rigorous by authors Ulf Nilsson and Jan Maluszynski.  They develop a series of definitions to build the language of predicate calculus and inference.  The familiarity was due to my studies from the material presented in Luger and Stubblefield (1992), and Stewart and Norvig (1995).

The authors continue with the SLD-Resolution along with Unification.  They illustrate a unification algorithm as well as proof trees.  Afterwards negation is discussed; thus  they develop the SLDNF-Resolution.  The cut and mathematics is covered.  If used improperly, cuts can make programs unsound and yield false answers.  All this tied into logic programming theory.  The theorems and propostions come from various resources.  The goal of the book is teach programmers on how to write logic programs that are sound, correct, and finite.

I found this book interesting thus far and good introduction to logic programming and prolog.

Progress Report – December 2008

The month began by reviewing my college Probability and Statistics book (Devore 1991).  I needed to review standard probability concepts mentioned in articles and the Stanford machine learning class.  For example, the article Learning with a Mixture of Trees (Meila and Jordan 2000) the authors explain the new algorithm by using Joint Probabilities and probabilistic mathematics to describe the algorithm – a similar used by Dr. Ng in his machine learning lectures.

AIMA Book

I was reading Chapters 6 and 7 of the AIMA book (Russell, Norvig 1995). They describe propositional calculus, which from their perspective is a weak form logic. The authors start with the basics and build on the fundamentals by demonstrating the language using Backus Naur Form (BNF).  They used the Wumpus World as an example and demostrated that it will take at 6400 propositional logic statements to adequately describe the 4×4 Wumpus World.

In the next Chapter, the authors discuss predicate calculus and show its BNF.  The main focus is on first order predicate calculus and then applying it to the Wumpus World example.  They discuss the frame problem and situation calculus.  They used predicate calculus to demonstrate the differences and static components between two situations, which includes the frame axioms.

The discussion was neatly tied together between a problem and predicate calculus unlike the Luger book that I read earlier.  In the Luger the frame problem was used to illustrate robotic planning in the block’s world.

My goals are to run the AIMA wumpus world lisp code and complete the predicate calculus of the Wumpus world problem.

Unification

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.