Transcript Inference in First Order Logic

Inference in First Order Logic
CS 171/271
(Chapter 9)
Some text and images in these slides were drawn from
Russel & Norvig’s published material
1
Inference Algorithms




Reduction to Propositional Inference
Lifting and Unification
Chaining
Resolution
2
Propositionalization



Strategy: convert KB to propositional
logic and then use PL inference
Ground atomic sentences become
propositional symbols
What about the quantifiers?
3
Example

KB in FOL:






x King(x)  Greedy(x)  Evil(x)
King(John)
Greedy(John)
Brother(Richard,John)
The last 3 sentences can be symbols in PL
Apply Universal Instantiation to the first
sentence
4
Universal Instantiation


UI says that from a universally quantified
sentence, we can infer any sentence obtained
by substituting a ground term for the variable
Back to Example


From: x King(x)  Greedy(x)  Evil(x)
To:



King(John)  Greedy(John)  Evil(John)
King(Richard)  Greedy(Richard)  Evil(Richard)
…
5
Issue with UI


Ground terms: all symbols that refer to
objects as well as function applications (recall
that function applications return objects)
For example, suppose Father is a function:



Father(John) and Father(Richard) are also
objects/ground terms
But so are Father(Father(John)) and
Father(Father(Father(John)))
Infinitely many ground terms/instantiations
6
Existential Instantiation


Whenever there is a sentence, x P, introduce
a new object symbol called the skolem
constant and then add the unquantified
sentence P, substituting the variable with that
constant
Example:


From: x Crown(x)  OnHead(x, John)
To: Crown(Cnew)  OnHead(Cnew, John)
7
Substitution


UI and EI apply substitutions
A substitution is represented by a variable v
and a ground term g; {v/g}



Can have sets of these pairs if there are more
variables involved
Let  be a sentence (possibly containing v)
SUBST( {v/g},  ) stands for the sentence
that applies the substitution to 
8
UI and EI Defined

UI:
v α ___ for any ground term g
SUBST({v/g}, α)

EI:
v α ___ for some constant symbol k not
SUBST({v/k}, α) yet in the knowledge base
9
Back to Propositionalization
Given a KB in FOL, convert KB to PL by

1.
2.
If there are no functions (Datalog KB), UI
application does not result in infinitely many
sentences



applying UI and EI to quantified sentences
converting atomic sentences to symbols
Regular PL Inference can now be carried out
without problems
What if there are functions?
10
Dealing with Infinitely Many
Ground Terms

Can set a depth-limit for ground terms




Depth specifies levels of function nesting allowed
Carry out reduction and inference process for
depth 1, then 2, then 3, …
Stop when entailment can be concluded
This works if there is such a proof, but goes
into an endless loop if there is not


The strategy is complete
The entailment problem in this sense is
semidecidable
11
Inefficiencies in
Propositionalization


An inordinate number of irrelevant
sentences may be generated, resulting
from UI
This motivates generating only those
sentences that are important in
entailment
12
Example

Suppose KB contains:





x King(x)  Greedy(x)  Evil(x)
y Greedy(y)
King(John)
Suppose we want to conclude Evil(John)
Because of the existence of objects other
than John (such as Richard) and the
existence of functions, UI will generate many
sentences
13
Example, continued

It is sufficient to generate:



Which is just:



King(John)  Greedy(John)  Evil(John)
Greedy(John)
SUBST( {x/John}, King(x)  Greedy(x)  Evil(x) )
SUBST( {y/John}, Greedy(y) )
Applying the substitution matches the


Premises: King(x)  Greedy(x)
With other sentences in the KB:
Greedy(y), King(John)
14
Lifted Modus Ponens


Lifting: Raising propositional inference rules
to first order logic
Example: Generalized Modus Ponens
If there is a substitution θ, such that
SUBST(θ, pi) = SUBST(θ, pi’) for all i, then
p1', p2', … , pn’, ( p1  p2  …  pn  q)
_______________________________________________________________________________
SUBST(θ,q)

In our example,  = {x/John, y/John}
15
Unification



Process that makes logical expressions
identical
Goal: match the premises of
implications so that conclusions can be
derived
UNIFY algorithm takes two sentences
and returns a unifier (substitution) if it
exists
16
Unification Algorithm
17
Unification Algorithm
18
About UNIFY




UNIFY returns a Most General Unifier
(MGU)
There are efficiency issues with
OCCUR-CHECK function
May need to standardize apart:
rename variables to avoid name clashes
Unification is a key component of all
first-order algorithms
19
What’s Next?


Forward and backward chaining
algorithms for FOL that use unification
Resolution-based theorem proving
systems
20