Inference in First Order Logic: Horn Clauses

---

Reasoning with FOL

We have talked about two kinds of logic: propositional and first-order (FOL).
Last time we sketched how the knowledge base of an intelligent agent could be expressed in terms of FOL.
Today we will discuss how we can reason using FOL.
What does it mean to reason?
One way of looking at it is to think in terms of asking and answering questions.
Suppose we have a sentence (in FOL) such as:

 Likes(Sally, Teacher)

We can think of this as the way the intelligent agent might ASK itself: "Does sally like the teacher?".
The answer could be "True", "False" or "don't know".
If the answer is "True", we would like to have an automatic procedure for inferring it from the database.
Inference just means constructing a proof.
Today we will discuss valid proof components--inference rules--and two algorithms for automatically constructing FOL proofs.
Notice that there is another type of question: "Do you know what time it is?".
This could be encoded as a sentence in FOL as follows:

 Exists t Knows(You,t) AND CurrentTime(t)

The answer to this question could still be "True", "False" or "don't know", but, if it is "True", it would be nice to know what the value of "t" (the current time) is!
Just like the previous question, this question can be answered by constructing a proof that either proves that "t1", say, is the current time, or proving that there is no current time.
To summarize then, reasoning in FOL involves finding the answers to questions by constructing proofs. If the questions have variables, then the values of the variables, not just the answer, are important.

Inference rules for FOL

Now we must look at how to do proofs using first-order logic.
A computer program, i.e. an AI agent, cannot do proofs by somehow magically "understanding" sentences and "thinking" about their meanings.
A proof must always be built from a fixed set of inference rules.



The propositional logic inference rules

Remember the inference rules for propositional logic:


1. Modus Ponens or Implication-Elimination:

   A => B, A
   ---------
       B
   

2. And-Elimination:

   A1 and A2 and ... An
   --------------------
           Ai
   

3. And-Introduction:

     A1, A2, ... An
   --------------------
   A1 and A2 and ... An
   

4. Or-Introduction:

          Ai
   ------------------
   A1 or A2 or ... An
   

5. Double-Negation Elimination:

   NOT(NOT(A))
   -----------
        A
   

6. Unit Resolution:

   A or B, NOT(B)
   ---------------
           A
   

7. Resolution:

   A or B, NOT(B) or C
   -------------------
           A or C
   
   

These rules are still valid for FOL.
A, B, and C are now atomic sentences (ie, a predicate or Term=Term, no negation).



Substitution

We need some way to deal with variables and the quantifiers "EXISTS" and "FORALL".
To describe inference rules involving variables and quantifiers, we need the notion of "substitution".
Let alpha be any sentence and let theta be a substitution list:


 theta = {x/fred, y/z, ...}

The notation SUBST(theta, alpha) will denote the result of applying the substitution theta to the sentence alpha Intuitively subst(x := g, alpha) is alpha with every appearance of x replaced by g.
Notice that this is a syntactic operation on sentences. Any operation involved in a proof has to be syntactic: it has to just manipulate and transform sentences.





Elimination and Introduction

Many inference rules tell how how to get rid of (eliminate) or introduce a connective or quantifier into a formula.
The "universal elimination" rule lets us use a universally quantified sentence to reach a specific conclusion, i.e. to obtain a concrete fact.



 
          FORALL x alpha
       ---------------------
        SUBST({x/g} alpha)

Here g may be any term, including any term that is used elsewhere in the knowledge base.
The "existential elimination" rule lets us convert an existentially quantified sentence into a form without the quantifier.



 
          EXISTS x alpha
       ---------------------
        SUBST({x/k} alpha)

Here k must be a new constant symbol that does not appear anywhere else in the database. It is serving as a new name for something we know must exist, but whose name we do not yet know.
The "existential introduction" rule lets us use a specific fact to obtain an existentially quantified sentence:



 
                   alpha
        ------------------------------
         EXISTS y SUBST({g/y}, alpha)

This rule can be viewed as "leaving out detail": it omits the name of the actual entity that satisfies the sentence alpha, and just says that some such entity exists.



Skolemization

The "existential elimination" rule is also called the Skolemization rule, after a mathematician named Thoralf Skolem.



 
          EXISTS x alpha
        --------------------
        subst({x/k}, alpha)       where k is a FRESH constant

Saying that k is a "fresh" constant means that k is not used anywhere else in the knowledge base.
This means that k can be the name of a new entity that is not named and therefore not referred to anywhere else in the knowledge base.
Example: consider the fact


 
        exists z brotherof(Harry,z)

It would not be correct to directly deduce

 
        brotherof(Harry,William)

However it is correct to deduce

 
        brotherof(Harry,personA)

and then later we might deduce that

 personA = William.

Generalized Modus Ponens

This is a complex inference rule that captures a common pattern of reasoning.



 
        p1  p2  ...  pn   (q1 AND q2 AND ... AND qn -> r)
        -------------------------------------------
                      SUBST(theta, r)

where for each i SUBST(theta,pi) = SUBST(theta,qi).
Intuitively this is modus ponens with multiple antecedents on the left hand side of the -> connective.
Theta is a SET of individual substitutions of the form x/g where x is a variable and g is a ground term.
The equation SUBST(theta,pi) = SUBST(theta,qi) says that applying theta makes pi and q1 identical.
Terminology: theta UNIFIES pi and qi, theta is a unifying substitution.

The unification algorithm

There is a standard algorithm that given two sentences, finds their unique most general unifying substitution.
Here are some examples of unification.



 Knows(John, x) = Likes(John, x)

 Knows(John, Jane)
 Knows(y, Leonid)
 Knows(y, Mother(y))

The unification algorithm whould give the following results:



 UNIFY(Knows(John,x), Knows(John,Jane)) = {x/Jane}
 UNIFY(Knows(John,x), Knows(y,Leonid)) = {x/Leonid, y/John}

The substitution makes the two sentences identical.



 UNIFY(Knows(John,x), Knows(y,Mother(y))) = {x/John, x/Mother(John)}

Notice that the substitutions always involve a variable and a ground term.



 UNIFY(Knows(John,x), Knows(x,Elizabeth)) = fail

The variable x cannot have two values at the same time, so this last example fails.
Another example that would always fail is



 UNIFY(x, F(x)) = fail

This fails because a the variable may never occur in the term it is being unified with.

Horn clauses

Generalized modus ponens requires sentences to be in a standard form, called Horn clauses after the mathematician Alfred Horn.
A Horn clause is a sentence of the form



        q1 AND q2 AND ... AND qn -> r

where each qi and r is an atomic sentence and all variables are universally quantified.
Recall that an atomic sentence is a just single predicate and does not allow negation.
Normally the universal quantifiers are implicit (not written explicitly).
To refresh your memory, here is the syntax of FOL in Backus-Naur form.



        Sentence        -> AtomicSentence
                        | Sentence Connective Sentence
                        | Quantifier Variable,... Sentence
                        | NOT Sentence
                        | (Sentence)

        AtomicSentence  -> Predicate(Term, ...) | Term = Term

        Term            -> Constant
                        | Variable
                        | Function(Term,...)

        Connective      -> AND | OR | => | <=>

        Quantifier      -> FORALL | EXISTS

        Constant        -> A | X_1 | John | ...

        Variable        -> a | x | s ...

        Predicate       -> Before | HasColor | Raining | ...

        Function        -> Smelly | LeftLegOf | Plus | ...

In order to obtain Horn clauses, existential quantifiers must be eliminated using Skolemization.
Example:


 EXISTS x Loves(John,x) AND Loves(x,John) 

becomes

 
        Loves(John,personx)
        Loves(personx,John)

Note that above we have two Horn clauses, which share a Skolem constant.

Backward chaining

The backward chaining algorithm can answer questions in Horn clause knowledge bases.
It works by taking the goal and checking to see if it unifies directly with a sentence in the database.
If so, it returns the substitution list that makes the query equal the known sentence.
Otherwise, backward chaining finds all the implications whose conclusions unify with the query and then tries to establish their premises.
Consider a knowledge base that says it is illegal to sell weapons to hostile nations. It also says that Colonel West sold all of country Nono's missiles to it. And missiles are weapons.



 American(x) AND Weapon(y) AND Nation(z) AND Hostile(z)
  AND Sells(x,y,z) => Criminal(x)

 Owns(Nono, x) AND Missile(x) => Sells(West,Nono,x)

 Missile(x) => Weapon(x)

 Enemy(x,America) => Hostile(x)

We add to it the following facts:


 American(West)

 Nation(Nono)

 Enemy(Nono, America)

 Missile(M1)

We want to solve the crime: Is West a criminal?