Funding for 'IT Lab' Project, Phase 1: Progress of sticker sales. Purchase a sticker to help us reach our target.Updated: 2010-02-28 11:53
10.7%
Home » Volume 01 Issue 08 September 2009 » Software Dev
AI


A quick recap

After a small break in the series of AI articles with no article appearing on diGIT magazine’s August issue, here we are again exploring the area of knowledge representation and reasoning with respect to AI. Hope our readers have not forgotten all the concepts which were introduced in the last couple of articles with respect to ‘First Order Logic’ which we are going to go in depth in today’s article. Just to give you a quick glimpse of what we presented in the last article (which appeared in diGIT’s July 2009 issue), I would remind you the concepts we discussed. We learnt what ‘First Order Logic’ (FOL) also known as ‘Predicate Logic’ is in the context of representing knowledge using logical symbols. We also learnt the syntax of FOL under two sections such as logical symbols and non-logical symbols. The descriptions on connectives, punctuation and variable fell in the logical symbol section while variables, predicate symbols and function symbols belonged to the non-logical symbol section. Then we also looked at the scope of the quantifiers such as ‘For all’  and ‘Exists’ , where understanding of the scope is highly essential to construct as well as interpret FOL based statements. Next we went to understand the semantics of FOL based statements and the article consisted of various examples to give the flavor of different interpretations of the statements. The last section also consisted of a comparison between FOL and Propositional Logic so that you could understand the pros and cons of each logical representation method. I hope you would go through the previous article and refresh your memory on the above stated concepts before going through today’s article so that you could get the most out of it easily.

Today we are going to look at interpretations, models, reasoning and resolution with regard to FOL which we would be discussing in the following sections in detail.

What is an ‘Interpretation’?

An interpretation is ‘an assignment to a variable which gives some semantic meaning to the predicate, function or statement in concern’. For example let’s consider a predicate as follows.

Boy(x)

Then all the possible assignments to the variable x in the predicate Boy() are interpretations.

Further, an interpretation assigns a denotation to all non-logical constants in the FOL language. It enables each term to be assigned to a specific object that it represents and based on that each sentence is assigned a truth value which gives semantic meaning to the FOL statements. Therefore, an interpretation is extremely important with respect to understanding and interpreting the meaning or the semantics of FOL. Interpretations in general specifies exactly which objects, relations and functions are referred to by the constant, predicate and function symbols respectively. Practically, when we are defining knowledge of a certain domain using FOL, we build up a specific set of available and useful interpretations which is known as ‘intended interpretation’ when we possess a certain understanding of the domain in concern. In such as case, for example if we are dealing with a domain of a school we know that certain constants such as ‘Bill’ are the intelligent boy where as ‘Jane’ is the smart girl. We may also know that the predicates ‘teaches’ refers to the teaching relationship between subject and teacher while ‘study’ refers to studying relationship between student and subject.


‘Model’&‘Tautology’ – An overview

If an interpretation satisfies or makes a certain FOL statement true (valid) in the domain of concern, such interpretation is called a ‘Model’ of that domain.

You may also see that a certain interpretation can make the FOL statement be invalid or leading for its semantic meaning to be false. So in that case it is not a model of that domain. Let’s try to illustrate this concept with a simple example in FOL.



In the above case the domain in concern is restricted to the specific constants defined which are as follows.

  •  Bob
  • Jack

So if we assign each of the above constants which could be interpretations in the FOL statement number 4 it would result as follows.

Interpretation 1:- x=bob, y=bob




This result is false and is not valid since there is no atomic statement which says that OlderThan(bill, bill) is true. We only consider the given atomic statements as true and all the others as false when dealing with knowledgebase systems. Therefore conjunction of two true statements and one false statement leads to a false conclusion. Let’s try the next interpretation.

Interpretation 2:- x=jack, y= bob


This result is also false and is not valid since there is no atomic statement which says that OlderThan(jack, bob) is true. We only consider the given atomic statements as true and all the others as false when dealing with knowledgebase systems. Therefore conjunction of two true statements and one false statement leads to a false conclusion. Let’s try the next interpretation.

Interpretation 3:- x=bob, y= jack

This result is true because the atomic sentences Boy(bob), Boy(jack) and  OlderThan(bob, jack)are all true and defined in the domain. So the conjunction of all three true values lead to the statement ElderBrother(bob, jack) being interpreted as true. Therefore the interpretation, x=bob, y= jack is a ‘model’ for this example.

If a FOL statement is resulted as valid or gives value true under all possible interpretations applicable in that domain, then such FOL statement it is called a ‘Tautology’. So in such a case under all possible interpretations the truth value of the statement becomes true thus showing it is valid under all conditions pertaining in that domain, which shows that it is a ground truth.


Resolution based reasoning

This topic is the ultimate objective of learning all about FOL. After constructing a knowledgebase using FOL statements adhering to the required syntax and semantics taught before, the objective is to raise queries to the knowledgebase and get some answers or reasoning to arrive at certain conclusions with regard to the domain in concern.

Resolution is a form of ‘rule of inference’ which define the statements of what formulas could be inferred from a set of other formulas. In other terms, the formulas or statements that we raise as queries to the knowledgebase should be inferred using the formulas or statements belonging to (residing in) the knowledgebase as a rule of inference. Such process is called ‘Resolution’. For one to go ahead with this reasoning process, it is first required to pre-process the statements appearing in the knowledgebase and convert them to a form known as Conjunctive Normal Form also known as CNF for short. CNF converts each statement to be a ‘conjunction of disjunction of literals’. Every propositional formula can be converted into an equivalent formula in CNF based on rules about logical equivalences such as the double negation law , the De Morgan's law and the distributive laws of logic which are shown in detail as follows.

We have looked at converting propositional logic statements to CNF form and performing resolution on propositional logic based systems in the previous article published in May 2009 issue of diGIT. You can have a look at it to refresh your memory again since it is somewhat similar to the resolution used here in FOL, only difference being we are now dealing with predicates and functions in contrast to simple propositions in propositional logic.

Following are the steps of converting a FOL based statement/formula to CNF form.

  1. Eliminate implication by replacing it with negation and disjunction.

    Example:- P(x) à Q(y) ≡ ~P(x) V Q(y)

  2. Move negation inwards so that it appears only in front of an atomic sentence.

    Example:- ~(P(x) V Q(x))  ≡ ~P(x) ^ ~Q(x)

    Also when quantifiers are present follow the following rules when moving negation inwards.

  3. Standardize variables - This ensures that each quantifier is over a distinct variable by renaming the variables as required. For sentences which has the same variable name appearing twice or multiple times, change the name of such variables to be unique in order to avoid confusions later. 
                       

    4.      Skolemization - Eliminate all remaining existential quantifiers Process:- For variables within existential quantifiers rename each variable with a                      distinct constant.

                       

    5.      Move universal quantifiers outside the scope of conjunction and disjunction and drop the universal quantifiers – At this point, all                          remaining variables must be universally quantified and the sentence is equivalent to one which all the universal quantifiers are moved to             the     utmost left. Therefore, we can drop the universal quantifiers now.


    6.       Distribute conjunction over disjunction

             Process:- Which requires De Morgan’s law and/or distributive law stated above.


             Example:- P(x) V (Q(x) ^ R(x)) ≡ (P(x) V Q(x)) ^ (P(x) V R(x))

   

    7.     Write resulting statement which is now in CNF form which is logically equivalent to the original statement.


   

After converting the statements in FOL which were residing in the knowledgebase in to CNF form following the above stated steps, we have to now consider how to use that to come up with resolution. If we are given a query or another statement to check the answer or check whether it is consistent with the knowledgebase respectively, we have to use the resolution as follows.

First we have to take the negation of the query to be answered or the statement to be checked for consistency.

“Why do we take the negation of this?” may be a question that might be lingering in your mind now. Let’s see the why it is required. Resolution proof is a method which is ‘refutation complete’. This means by taking the negation of the statement to be proved or answered we show that using that and the converted knowledgebase statements into CNF when unified would result in a null value (refutation) if the statement is true or false otherwise. This is a very simple concept. Consider that we have to prove that ‘A’ is true. We know certain facts related to ‘A’. If we show that using the related facts and the negation of ‘A’ leads to a refutation or a null statement we can show that ‘A’ is indeed true. This is somewhat similar to the ‘proof by contradiction’ approach used on logical and mathematical theorem proving which some of you may have heard when doing Mathematical subjects in school.

Now let’s go through a simple example where reasoning is done through resolution method mentioned above.

Example 1:-

Now let’s follow the unification procedure of resolution.

  •  Write each statement separated by the conjunctions in the resulting CNF form separately. Also write the negated to be proven statement alongside of them.
  • Then check whether we can unify a pair of statements by assigning a value for each variable inside the predicate symbols if required. Unification works such that if you find the negation and non-negated form of the same predicate/function with the same variable value you can cancel them out and write the rest of the statement. This is because the conjunction of negated and non-negated statement which is similar yield to null. For example you can see A ^ ~A = Null. Therefore, if we have predicates initialized with the same variable as P(a) ^ ~P(a) then it results in null and can be cancelled off.

 

Therefore, it is a contradiction (refutation).

Therefore, we can show that if we did not take the negation of Q(a) it would have been proven by the available statement in the knowledgebase. Thus we can conclude using resolution by refutation that; “Q(a) is inferred by (x) P(x)  ^  (P(a) à Q(a))”.

Example 2:-

Let’s consider another small example with respect to placement of boxes.

On(x,y) – Predicate to show that box ‘x’ is on box ‘y’

Red(x) – Predicate to show that the color of box ‘x’ is red




The known facts which are in the knowledgebase are as follows.

All of the above statements are atomic sentences which are already in CNF form so no need of conversion.

We have to show that:-

There exists a box which is red in color and on top of that lies a box which is not red in color. This statement can be written in FOL as follows



So to use with resolution method let’s take the negation of the above statement and unify with the known facts from the knowledgebase and see whether it results in a refutation.

Take Negation and follow steps of converting to CNF as follows. 


Now let’s do the resolution process as illustrated as below.


So this ultimately leads to a refutation showing that the statement:-