Inference in First-order Logic

While defining inference, we mean to define effective procedures for answering questions in FOPL.

FOPL offers the following inference rules:

·         Inference rules for quantifiers

·         Universal Instantiation (UI): In this, we can infer any sentence by substituting a ground term (a term without variables) for the variables. In short, when we create the FOPL of the given statement, we can easily infer any other statement using that FOPL

Notation: Let, SUBST( θ , α ) be the result of the given sentence α , and its substitute is θ.

       where v is the variable and g is the ground term.

       For example: Every man is mortal.

        It is represented as ∀ x: man(x)  →   mortal(x).

In UI, we can infer different sentences as:

man(John) →   mortal(John)

man(Aakash) →  mortal(Aakash), etc.

·         Existential Instantiation(EI): In EI, the variable is substituted by a single new constant symbol.

Notation: Let, the variable be v which is replaced by a constant symbol k for any sentence α  The value of k is unique as it does not appear for any other sentence in the knowledge base. Such type of constant symbols are known as Skolem constant. As a result, EI is a special case of Skolemization process.

Note: UI can be applied several times to produce many sentences, whereas EI can be applied once, and then the existentially quantified sentences can be discarded.

      For example: ∃x:steal(x, Money).

 We can infer from this: steal(Thief, Money)

·         Generalized Modus Ponen: It is a lifted version of Modus Ponen as it uplifts the Modus Ponens from ground propositions to FOPL. Generalized Modus Ponen is more generalized than Modus Ponen. It is because, in generailzed, the known facts and the premise of the implication are matched only upto a substitution, instead of its exact match.

Notation: For atomic sentences like pi.pi’ and q where we have a substitute
θ that SUBST( θ, pi)  for each i.

For example: p1’ is Thief(Charlie)                                p1 is Thief(x)

                                    p2’ is Silent(y)                                         p2 is Silent(y)

                                    θ will be {x/Charlie, y/Charlie}               q is evil(x)

                                     SUBST(θ,q ) is evil(Charlie).

·         Unification: It is the key component of First-order inference algorithms. Unification is the process used by the lifted inference rules to find substituents that could give identical but different logical expressions. It means the meaning of the sentence should not be changed, but it should be expressed in multiple ways. The UNIFY algorithm in unification takes two sentences as input and then returns a unifier if one exists:

              UNIFY(p,q)= θ where SUBST( θ , p) = SUBST( θ, q).

              Let see how UNIFY works with the help of the below example:

              Given: Knows(Ram,x). The question is- Whom does Ram knows?

 The UNIFY algorithm will search all the related sentences in the knowledge base, which could unify with Knows(Ram,x).

UNIFY (Knows(Ram, x), Knows(Ram, Shyam))≡{x/Shyam}

UNIFY (Knows{Ram,x}, Knows{y, Aakash})≡{x/Aakash, y/Ram}

UNIFY (Knows{Ram,x}, Knows{x, Raman})≡fails.

The last one failed because we have used the same variable for two persons at the same time.

Unification Algorithm

Earlier, we have studied TELL and ASK functions which are used to inform and interrogate a knowledge base. These are the primitive functions of STORE and FETCH functions. STORE function is used to store a sentence s into the knowledge base and FETCH function is used  to return all the unifiers with some sentences.

Note: In the above example: Knows(Ram, x) →  It is an instance of FETCH function.

·         Forward Chaining:  In forward chaining, we start with the atomic sentences in the knowledge base and apply Modus Ponen in forward direction. Also adding new sentences until any inference is not made.