AI | Rules for First Order Inference

The inference that John is evil—that is, that  answers the query  —works as follows: using the rule that Greedy Kings Are Evil, find some  that is both a king and greedy, and infer that this  is evil. More generally, we can claim the conclusion of the implication after applying if there is some replacement that makes each of the conjuncts in the premise of the implication similar to sentences already in the knowledge base. The substitution  =  achieves that goal in this situation.

We can really increase the amount of work done by the inference phase. Assume we don’t know, but we do know that everyone is greedy: 

Because we already know that John is a king (given) and that John is greedy (because everyone is greedy), we’d like to be able to conclude that \operatorname{Evil}(J o h n) exists. To make this work, we’ll need to discover a replacement for both the variables in the implication sentence and the variables in the knowledge base statements. In this situation, making the implication premises   and the knowledge-base sentences  and  equivalent by substituting . As a result, we can deduce the implication’s conclusion.

We call this inference process Generalized Modus Ponens because it can be summed up in a single inference rule:

For any  for atomic sentences p, p, and q, when there is a substitution  such that  for all .

The  atomic phrases  and the one implication are the  premises of this rule. The result of applying the substitution  to the consequent  is the conclusion. As an illustration, consider the following:

It’s simple to demonstrate that Generalized Modus Ponens is a reliable inference rule. First, we see that Universal Instantiation holds for any sentence  (whose variables are supposed to be universally quantified) and any substitution \theta, 

It holds in particular for a that satisfies the Generalized Modus Ponens rule’s criteria. Thus, we may infer 

and we can infer \operatorname{SUBST}\left(\theta, p_{1}\right) \wedge \ldots \wedge \operatorname{SUBST}\left(\theta, p_{n}\right) \Rightarrow \operatorname{SUBST}(\theta, q)

from the implication 

As the first of these two phrases perfectly supports the premise of the second,  in Generalized Modus Ponens is  for all  so, . As a result,  follows Modus Ponens.

Modus Ponens is a lifted version of Modus Ponens, elevating it from ground (variable-free) propositional logic to first-order logic. We’ll learn how to create lifted versions of the forward chaining, backward chaining, and resolution algorithms discussed in Chapter 7 throughout the rest of this chapter. Lifted inference rules have the benefit of propositionalization in that they only make the replacements that are required to allow certain inferences to occur.