L17-18-19 - BTechSpot.com

Download Report

Transcript L17-18-19 - BTechSpot.com

First Order Logic
(Syntax, Semantics and Inference)
1


Knowledge based agents can represent the world it is
in and can deduce the actions to take
In most programming languages the data and
operations are tied closely



Each update to a data structure is done via a domainspecific procedure whose details are derived by the
programmer from his own knowledge of the domain
Is there a way to say “pit is in [1,2] or [2,1]” ?
Propositional logic could represent the partial
information, with negation and disjunction
2


Propositional Logic is “compositional”
Propositional logic is less expressive when the world
consists many objects (why?)


But english/.../.. are very much expressive
Why not use engilsh for our representation?

Ambiguous & not compositional
3
First-order logic


Propositional logic assumes the world contains facts,
(ontological commitment)
First-order logic (like natural language) assumes the
world contains
– Objects: people, houses, numbers, colors, baseball
games, wars, …
– Relations: red, round, prime, brother of, bigger than,
part of, comes between, …
– Functions: father of, best friend, one more than, plus,
…
4


Ontological Commitments

Propositional Logic: facts which hold ot does not.

FOL
: Objects and relations
Epistemological Commitments (possible states of
knowledge w.r.t each facts)

Propositional Logic: true/false

FOL
: true/false
5
Syntax of FOL: Basic elements







Constants
Predicates
Functions
Variables
Connectives
Equality
Quantifiers
KingJohn, 2, ...
Brother, >,...
Sqrt, LeftLegOf,...
x, y, a, b,...
, , , , 
=
, 
6
Atomic sentences
Sentence
= AtomicSentence
| (Sentence Connective Sentence)
| Quantifier Variables,…. Sentence
| Sentence
Atomic sentence =
Term

predicate (term1,...,termn)
| term1 = term2
= function (term1,...,termn)
| constant
| variable
E.g., Brother(KingJohn,RichardTheLionheart) >
(Length(LeftLegOf(Richard)), Length(LeftLegOf(KingJohn)))
7
Truth in first-order logic



Sentences are true with respect to a model (possible world) and
an interpretation
Model contains objects (domain elements) and relations among
them
Interpretation specifies referents for
constant symbols
→ objects
predicate symbols
→ relations
function symbols → functional relations

An atomic sentence predicate(term1,...,termn) is true iff the
objects referred to by term1,...,termn are in the relation referred
to by predicate
8
Universal quantification
 <variables> <sentence>
Everyone at England is smart:
x At(x, England)  Smart(x)
 x P is true in a model m iff P is true with x being each possible object in
the model

Roughly speaking, equivalent to the conjunction of instantiations of P
At(KingJohn,England)  Smart(KingJohn)
 At(Richard, England)  Smart(Richard)
 At(England, England)  Smart(England)
 ...
9
A common mistake to avoid


Typically,  is the main connective with 
Common mistake: using  as the main connective
with :
x At(x, England)  Smart(x)
means “Everyone is at England and everyone is smart”
10
Existential quantification




<variables> <sentence>
Someone at England is smart:
x At(x, England)  Smart(x)
x P is true in a model m iff P is true with x being some possible object in
the model
Roughly speaking, equivalent to the disjunction of instantiations of P
At(KingJohn, England)  Smart(KingJohn)
 At(Richard, England)  Smart(Richard)
 At(England, England)  Smart(England)
 ...
11
Another common mistake to avoid


Typically,  is the main connective with 
Common mistake: using  as the main connective with :
x At(x,England)  Smart(x)
is true if there is anyone who is not at England!
12
Properties of quantifiers


x y is the same as y x
x y is the same as y x
13
Properties of quantifiers
x y is the same as y x
x y is the same as y x

x y is not the same as y x
x y Loves(x,y)



“There is a person who loves everyone in the world”
y x Loves(x,y)

“Everyone in the world is loved by at least one person”
14
Properties of quantifiers
x y is the same as y x
x y is the same as y x

x y is not the same as y x
x y Loves(x,y)



“There is a person who loves everyone in the world”
y x Loves(x,y)

“Everyone in the world is loved by at least one person”
Quantifier duality: each can be expressed using the other
x Likes(x,IceCream)
x Likes(x,IceCream)
x Likes(x,Broccoli)
x Likes(x,Broccoli)

15
Interacting with FOL KBs

Suppose a wumpus-world agent is using an FOL KB and
perceives a smell and a breeze (but no glitter) at t=5:
Tell(KB,Percept([Smell,Breeze,None],5))
Ask(KB,a BestAction(a,5))




i.e., does the KB entail some best action at t=5?
Answer: Yes, {a/Shoot}
← substitution (binding list)
Given a sentence S and a substitution σ,
Sσ denotes the result of plugging σ into S; e.g.,
S = Smarter(x,y)
σ = {x/Hillary,y/Bill}
Sσ = Smarter(Hillary,Bill)
• Ask(KB,S) returns some/all σ such that KB╞ Sσ
16
Universal instantiation (UI)

Every instantiation of a universally quantified sentence is entailed by it:
v α
Subst({v/g}, α)
for any variable v and ground term g

E.g.,
x King(x)  Greedy(x)  Evil(x) yields:
King(John)  Greedy(John)  Evil(John)
King(Richard)  Greedy(Richard)  Evil(Richard)
King(Father(John))  Greedy(Father(John))  Evil(Father(John))
.
.

… substitutions are {x/Richard} , {x/John}, {x/ Father(John)}
We can infer any sentence by replacing the variable with the ground term
17
Existential instantiation (EI)

For any sentence α, variable v, and constant symbol k that does
not appear elsewhere in the knowledge base:
v α
Subst({v/k}, α)

E.g., x Crown(x)  OnHead(x,John) yields:
Crown(C1)  OnHead(C1,John)
provided C1 is a new constant symbol, called a Skolem constant
18
Reduction to propositional inference
Suppose the KB contains just the following:
x King(x)  Greedy(x)  Evil(x)
King(John)
Greedy(John)
Brother(Richard,John)

Instantiating the universal sentence in all possible ways, we have:
King(John)  Greedy(John)  Evil(John)
King(Richard)  Greedy(Richard)  Evil(Richard)
King(John)
Greedy(John)
Brother(Richard,John)

The new KB is propositionalized: proposition symbols are
King(John), Greedy(John), Evil(John), King(Richard), etc.
19
Reduction contd.
• Idea: propositionalize KB and query, apply resolution, return
result
• Problem: with function symbols, there are infinitely many ground
terms,

e.g., Father(Father(Father(John)))
• Theorem: Herbrand (1930). If a sentence α is entailed by an FOL
KB, it is entailed by a finite subset of the propositionalized KB
• Idea: For n = 0 to ∞ do


Create a propositional KB by instantiating with depth-n terms
See if α is entailed by this KB.
20
Reduction contd.
• Problem: Works if α is entailed, loops if α is not
entailed
• Theorem:


Turing (1936), Church (1936)
Entailment for FOL is semidecidable

algorithms exist that say yes to every entailed sentence, but
no algorithm exists that also says no to every nonentailed
sentence.
21
Problems with Propositionalization

Propositionalization seems to generate lots of irrelevant sentences.

E.g., from:
x King(x)  Greedy(x)  Evil(x)
King(John)
y Greedy(y)
Brother(Richard,John)
22
Forward Chaining
23
Unification
We can get the inference immediately if we can find a substitution θ such
that King(x) and Greedy(x) match King(John) and Greedy(y)
θ = {x/John,y/John} works
Unify(α,β) = θ if αθ = βθ
p
q
θ
Knows(John,x) Knows(John,Jane)
{x/Jane}
Knows(John,x)
Knows(y,OJ)
{x/OJ, y/John}
Knows(John,x) Knows(y,Mother(y)) {y/Jane, x/Mother(y)}
Knows(John,x)
Knows(x,OJ)
{Fail}
Standardizing apart eliminates overlap of variables, e.g., Knows(z17,OJ)
Unification
To unify Knows(John,x) and Knows(y,z),
θ = {y/John, x/z } or θ = {y/John, x/John, z/John}
The first unifier is more general than the second, places
fewer restriction on the values of the variables
There is a single most general unifier (MGU) that is
unique up to renaming of variables.
MGU = { y/John, x/z }
First Order Definite Clauses
Exactly one positive literal
Atomic literal
Implication whose antecedent is conjunction of positive
literal and a single positive literal as consequent
Examples
King(x) Λ Greedy(x) Evil(x)
King(John)
Greedy(y)
Generalized Modus Ponens
p1', p2', … , pn', ( p1  p2  …  pn q)
qθ
p1' is King(John)
p1 is King(x)
p2' is Greedy(y)
p2 is Greedy(x)
θ is {x/John,y/John} q is Evil(x)
q θ is Evil(John)
Lifted version of modus ponens
GMP used with KB of definite clauses
All variables assumed universally quantified
An Example KB
Consider the passage
The law says that it is a crime for an American to sell
weapons to hostile nations. The country Nono, an enemy of
America, has some missiles, and all of its missiles were sold
to it by Colonel West, who is American.
The KB should answer the query
Is Col. West a criminal?
An Example KB (contd…)
... it is a crime for an American to sell weapons to hostile nations:
American(x)  Weapon(y)  Sells(x,y,z)  Hostile(z)  Criminal(x)
Nono … has some missiles, i.e., x Owns(Nono,x)  Missile(x):
Owns(Nono,M1) and Missile(M1)
… all of its missiles were sold to it by Colonel West
Missile(x)  Owns(Nono,x)  Sells(West,x,Nono)
Missiles are weapons:
Missile(x)  Weapon(x)
An enemy of America counts as "hostile“:
Enemy(x,America)  Hostile(x)
No Function Symbols in the KB
>> Datalog KB
West, who is American …
American(West)
The country Nono, an enemy of America …
Enemy(Nono,America)
Forward Chaining Algorithm
Forward chaining - Example
Forward chaining - Example
Forward chaining - Example
Forward Chaining Algorithm - discussion
No new sentences can be added to the KB after it has
generated criminal(west)
Fixed point of inference process
Sound
Complete (?)
Datalog KB
• k- maximum arity of predicates, n – constant symbols, ppredicates  pnk distinct ground facts
KB with function symbols
• Use Herbrand’s theorem, if the query has answer.
Remember, entailment with FOL is semidecidable
Forward Chaining Algorithm - discussion
Efficiency concerns
Notice the inner-loop generate all possible θ
• Expensive pattern matching
Algorithm rechecks every rule in every iteration to see if the
premises are satisfied
Generates many facts which are irrelevant to the goal
Addressing Efficiency Concerns
Matching against known rules only
To apply the rule, Missile(x)  Weapon (x)
Look for the rules that unify only with Missile(x)
Use Indexed KB
Missile(x) Λ Owns(Nono,x)  Sells(West, x, Nono)
Owns(Nono,x)Nono may own thousands of objects
Find all missiles first, then see if these missiles are owned by
Nono : conjunct ordering
Remember heuristic : Most constrained variable
Addressing Efficiency Concerns
Matching against known rules only
Diff(wa,nt)  Diff(wa,sa)  Diff(nt,q) 
Diff(nt,sa)  Diff(q,nsw)  Diff(q,sa) 
Diff(nsw,v)  Diff(nsw,sa)  Diff(v,sa) 
Colorable()
Diff(Red,Blue) Diff (Red,Green)
Diff(Green,Red) Diff(Green,Blue)
Diff(Blue,Red) Diff(Blue,Green)
Colorable() is inferred iff the CSP has a solution
CSPs include 3SAT as a special case, hence matching is NP-hard
Forward chaining has an NP Hard Matching Problem in its inner loop 
Addressing Efficiency Concerns
Matching against known rules only
> Most Rules in real world are small and simple, upper
bounds on the rule size and arity.
> Data complexity
> Consider only subclasses of databases for which matching
is efficient  datalog KB
Use better algorithm that avoids redundant matchings
Addressing Efficiency Concerns
Incremental Forward Chaining
Every fact inferred at iteration t will use at least one fact
derived at iteration t-1
At iteration t, consider only rules whose premise include
conjuncts which unifies with a fact derived at iteration t-1
With indexing, we may find out all rules which may trigger at
iteration t
Rete Algorithm
Backward Chaining
40
Backward chaining algorithm
SUBST(COMPOSE(θ1, θ2), p) = SUBST(θ2, SUBST(θ1, p))
Backward chaining example
Backward chaining example
Backward chaining example
Backward chaining example
Backward chaining example
Backward chaining example
Backward chaining example
Backward chaining example
Properties of backward chaining
Depth-first recursive proof search: space is linear in size
of proof
Incomplete due to infinite loops
 fix by checking current goal against every goal on stack
Inefficient due to repeated subgoals (both success and
failure)
 fix using caching of previous results (extra space)
Widely used for logic programming
Resolution
Converting sentences to CNF
1. Eliminate all ↔ connectives
(P ↔ Q)  ((P  Q) ^ (Q  P))
2. Eliminate all  connectives
(P  Q)  (P  Q)
3. Reduce the scope of each negation symbol to a single predicate
P  P
(P  Q)  P  Q
(P  Q)  P  Q
(x)P  (x)P
(x)P  (x)P
4. Standardize variables: rename all variables so that each quantifier has its own
unique variable name
Converting sentences to clausal form
5. Eliminate existential quantification by introducing Skolem
constants/functions
(x)P(x)  P(c)
c is a Skolem constant (a brand-new constant symbol that is not
used in any other sentence)
(x)(y)P(x,y)  (x)P(x, f(x))
since  is within the scope of a universally quantified variable, use a
Skolem function f to construct a new value that depends on the
universally quantified variable
f must be a brand-new function name not occurring in any other
sentence in the KB.
E.g., (x)(y)loves(x,y)  (x)loves(x,f(x))
In this case, f(x) specifies the person that x loves
Converting sentences to clausal form
6. Remove universal quantifiers by (1) moving them all to the left end;
(2) making the scope of each the entire sentence; and (3) dropping
the “prefix” part
Ex: (x)P(x)  P(x)
7. Put into conjunctive normal form (conjunction of disjunctions) using
distributive and associative laws
(P  Q)  R  (P  R)  (Q  R)
(P  Q)  R  (P  Q  R)
8. Split conjuncts into separate clauses
9. Standardize variables so each clause contains only variable names
that do not occur in any other clause
An example
(x)(P(x)  ((y)(P(y)  P(f(x,y)))  (y)(Q(x,y)  P(y))))
2. Eliminate 
(x)(P(x)  ((y)(P(y)  P(f(x,y)))  (y)(Q(x,y)  P(y))))
3. Reduce scope of negation
(x)(P(x)  ((y)(P(y)  P(f(x,y))) (y)(Q(x,y)  P(y))))
4. Standardize variables
(x)(P(x)  ((y)(P(y)  P(f(x,y))) (z)(Q(x,z)  P(z))))
5. Eliminate existential quantification
(x)(P(x) ((y)(P(y)  P(f(x,y))) (Q(x,g(x))  P(g(x)))))
6. Drop universal quantification symbols
(P(x)  ((P(y)  P(f(x,y))) (Q(x,g(x))  P(g(x)))))
Example
7. Convert to conjunction of disjunctions
(P(x)  P(y)  P(f(x,y)))  (P(x)  Q(x,g(x))) 
(P(x)  P(g(x)))
8. Create separate clauses
P(x)  P(y)  P(f(x,y))
P(x)  Q(x,g(x))
P(x)  P(g(x))
9. Standardize variables
P(x)  P(y)  P(f(x,y))
P(z)  Q(z,g(z))
P(w)  P(g(w))
Resolution: brief summary
Full first-order version:
l1  ···  lk,
m1  ···  mn
(l1  ···  li-1  li+1  ···  lk  m1  ···  mj-1  mj+1  ···  mn)θ
where Unify(li, mj) = θ.
The two clauses are assumed to be standardized apart so that they share
no variables.
For example,
Rich(x)  Unhappy(x) , Rich(Ken)
Unhappy(Ken)
with θ = {x/Ken}
Apply resolution steps to CNF(KB  α); complete for FOL
Resolution proof: definite clauses