Transcript PPT

Knowledge Representation IV
Inference in First-Order Logic
CSE 473
Logistics
• PS2
Snapshot due today
Final version due in 1 week
• Turn lights down
© Daniel S. Weld
2
473 Topics
Perception
Inference
Logic
NLP
Robotics
Supervised
Learning
Knowledge
Representation
Multi-agent
Reinforcement
Learning
Planning
Probability
Search
Problem Spaces
Agency
© Daniel S. Weld
3
Logic-Based KR






Propositional logic
Syntax (CNF, Horn clauses, …)
Semantics (Truth Tables)
Inference (FC, Resolution, DPLL, WalkSAT)
Restricted Subsets
First-order logic
Syntax (quantifiers, skolem functions, …
Semantics (Interpretations)
Inference (FC, Resolution, Compilation)
Restricted Subsets (e.g. Frame Systems)
Representing events, action & change
© Daniel S. Weld
4
Propositional. Logic vs. First Order
Ontology
Syntax
Objects,
Facts (P, Q)
Properties,
Relations
Variables & quantification
Atomic sentences
Sentences have structure: terms
Connectives
father-of(mother-of(X)))
Semantics
Truth Tables
Interpretations
(Much more complicated)
Inference
Algorithm
DPLL, GSAT
Fast in practice
Unification
Forward, Backward chaining
Prolog, theorem proving
NP-Complete
Semi-decidable
Complexity
© Daniel S. Weld
5
Prop. Logic: Knowledge Engr
1)
2)
3)
4)
5)
One of the women is a biology major
Lisa is not next to Dave in the ranking
Dave is immediately ahead of Jim
Jim is immediately ahead of a bio major
Mary or Lisa is ranked first
1. Choose Vocabulary Universe: Lisa, Dave, Jim, Mary
LD = “Lisa is directly ahead of Dave”
D = “Dave is a Bio Major”
2. Choose initial sentences (wffs)
1)
2)
3)
4)
© Daniel S. Weld
L M
LD  DL
DJ
(JD  D)  (JL  L)  (JM  M)
Error!
6
Knowledge Engineering in FOPC
1)
2)
3)
4)
5)
1.
One of the women is a biology major
Lisa is not next to Dave in the ranking
Dave is immediately ahead of Jim
Jim is immediately ahead of a bio major
Mary or Lisa is ranked first
Choose Vocabulary
Objects, Relations
2. Choose initial sentences
© Daniel S. Weld
7
FOL Reasoning

FO Forward & Backward Chaining
FO Resolution
Many other types of theorem proving
Restricted representations
Description logics
Compilation to SAT
© Daniel S. Weld
8
Unification
• Match expressions w/ variables
Denoted ?x
• Unify(x, y) returns “mgu”
Unify(city(?a), city(kent)) returns {?a/kent}
• Substitute(expr, mapping) returns new expr
Substitute(connected(?a, ?b), {?a/kent})
returns connected(kent, ?b)
© Daniel S. Weld
9
Unification Example I
• Unify(f(g(?x, dog), ?y)),
f(g(cat, ?y), dog)
Unification ok
Returns {?x / cat, ?y / dog}
When substitute in both expressions, they match
Each is f(g(cat, dog))
© Daniel S. Weld
10
Unification Example II
• Unify(f(g(?x)), f(?x))
They don’t unify
 binding, such that substitution makes both
expressions the same.
E.g. consider: {?x / g(?x) }
We get f(g(g(?x))) and f(g(?x)) … not equal!
• A variable value may not contain itself
Directly or indirectly
© Daniel S. Weld
11
Reminder Resolution
• When trying to prove
 |= 
• Use proof by contracdiction
Show    unsatisfiable
• Resolution rule
© Daniel S. Weld
12
Propositional Resolution
[Robinson 1965]
{ (p  ), ( p    ) } |-R (    )
}
Recall Propositional Case:
•Literal in one clause
•Its negation in the other
•Result is disjunction of other literals
© Daniel S. Weld
13
First-Order Resolution
[Robinson 1965]
{ (p(?x)  a(a), ( p(q)  b(?x)  c(?y)) }
|-R
(a(a)  b(q)  c(?y))
•Literal in one clause
•The negation of something which unifies in
the other
•Result is disjunction of other literals / mgu
© Daniel S. Weld
14
First-Order Resolution
• Is it the case that  |=  ?
• Method
Let  =   
Convert  to clausal form
•
•
•
•
Standardize variables
Move quantifiers to front, skolemize to remove 
Replace  with  and 
Demorgan’s laws...
Resolve until get empty clause
© Daniel S. Weld
15
Skolemization
• Existential quantifiers aren’t necessary!
Existential variables can be replaced by
• Skolem functions (or constants)
• Args to function are all surrounding  vars
• d t has(d, t)
d has(d, f(d) )
• x y loves(y, x)
y loves(y, f() )
y loves(y, f97 )
© Daniel S. Weld
16
Example
• Given
?x man(?x) => mortal(?x)
?x woman(?x) => mortal(?x)
?x person(?x) => man(?x)  woman(?x)
person(kelly)
• Prove
mortal(kelly)
[m(?x),d(?x)] [w(?y), d(?y)] [p(?z),m(?z),w(?z)] [p (k)][d(k)]
© Daniel S. Weld
17
Example Continued
[m(?x),d(?x)] [w(?y), d(?y)] [p(?z),m(?z),w(?z)] [p (k)] [d(k)]
[m(k),w(k)]
[w(k), d(k)]
[w(k)]
[d(k)]
[]
© Daniel S. Weld
18
May not Terminate
Given
Prove
P(fred)
?p ?f P(?p) => P(?f)
P(joe)
[ (P(?p), P(F(?p)))
(P(joe))
(P(fred)) ]
(P(F(joe)))
(P(F(F(joe))))
(P(F(F(F(joe)))))
© Daniel S. Weld
…
19
Compilation to Prop. Logic I
• Typed Logic
city a,b connected(a,b)
• Universe
Cities: seattle, tacoma, enumclaw
• Equivalent propositional formula:
Cst  Cse  Cts  Cte  Ces  Cet
© Daniel S. Weld
20
Compilation to Prop. Logic II
• Typed Logic
city c biggest(c)
• Universe
Cities: seattle, tacoma, enumclaw
• Equivalent propositional formula:
Bs  Bt  Be
© Daniel S. Weld
21
Compilation to Prop. Logic III
• Universe
• Cities: seattle, tacoma, enumclaw
• Firms: IBM, Microsoft, Boeing
• First-Order formula
firm f city c
HeadQuarters(f, c)
• Equivalent propositional formula
[ (HQis  HQit  HQie) 
(HQms  HQmt  HQme) 
(HQbs  HQbt  HQbe) ]
© Daniel S. Weld
22
Hey!
• You said FO Inference is semi-decidable
• But you compiled it to SAT
Which is NP Complete
• So now we can always do the inference?!?
Tho it might take exponential time…
• Something seems wrong here….????
© Daniel S. Weld
23
Restricted Forms of FO Logic
• Known, Finite Universes
Compile to SAT
• Frame Systems
Ban certain types of expressions
• Horn Clauses
Aka Prolog
• Function-Free Horn Clauses
Aka Datalog
© Daniel S. Weld
24