Transcript First Order Logic

First-Order Logic
CSE 573
573 Core Topics
Inference
Logic-Based
Supervised
Learning
Knowledge
Representation
Reinforcement
Learning
Planning
Probabilistic
Search
Problem Spaces
Agency
© Daniel S. Weld
2
Immediate Schedule
• Today
• First-Order Logic
• Thurs 10/16
• Class  3:30pm
“Intelligence in Wikipedia”
• Tues 10/21
• Jesse Davis – Machine Learning
• Thurs 10/23
• Probabilistic Reasoning
• Tues 10/28
• Jesse Davis
Learning Probabilistic Representations
CSPs will come later
© 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
FOL Definitions
• Constants: a,b, dog33.
Name a specific object.
• Variables: X, Y.
Refer to an object without naming it.
• Functions: dad-of
Mapping from objects to objects.
• Terms: dad-of(dog33)
Refer to objects
• Atomic Sentences: in(dad-of(dog33), food6)
Can be true or false
Correspond to propositional symbols P, Q
© Daniel S. Weld
6
More Definitions
• Logical connectives: and, or, not, =>
• Quantifiers:
 Forall
 There exists
• Examples
Dumbo is grey
Elephants are grey
There is a grey elephant
© Daniel S. Weld
7
Quantifier / Connective
Interaction
1. x E(x)  G(x)
E(x) == “x is an elephant”
G(x) == “x has the color grey”
2. x E(x) G(x)
3. x E(x)  G(x)
4. x E(x) G(x)
© Daniel S. Weld
8
Nested Quantifiers:
Order matters!
x y P(x,y)  y x P(x,y)
• Examples
Every dog shares a tail!
Every dog has a tail
d t has(d,t)
? t d has(d,t)
Someone is loved by everyone
x y loves(y, x)
© Daniel S. Weld
9
Semantics
• Syntax: a description of the legal
arrangements of symbols
(Def “sentences”)
• Semantics: what the arrangement of
symbols means in the world
Sentences
Models
© Daniel S. Weld
Sentences
Semantics
World
Semantics
Representation
Inference
Models
10
Propositional Logic: SEMANTICS
• “Interpretation” (or “possible world”)
• Specifically, TRUTH TABLES
Assignment to each variable either T or F
Assignment of T or F to each connective
P
Q
T F
T T F
F F F
PQ
© Daniel S. Weld
11
Models
• Depiction of one possible “real-world” model
© Daniel S. Weld
12
Interpretations=Mappings
syntactic tokens  model elements
Depiction of one possible interpretation, assuming
Constants:
Richard John
© Daniel S. Weld
Functions:
Leg(p,l)
Relations:
On(x,y) King(p)
13
Interpretations=Mappings
syntactic tokens  model elements
Another interpretation, same assumptions
Constants:
Richard John
© Daniel S. Weld
Functions:
Leg(p,l)
Relations:
On(x,y) King(p)
14
Satisfiability, Validity, & Entailment
• S is valid if it is true in all interpretations
• S is satisfiable if it is true in some interp
• S is unsatisfiable if it is false all interps
|=
• S1 entails S2 if
forall interps where S1 is true,
S2 is also true
© 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
FOL Reasoning
•
•
•
•
FO Forward & Backward Chaining
FO Resolution
Many other types of theorem proving
Restricted representations
Description logics
Horn Clauses
• Compilation to SAT
© Daniel S. Weld
17
Forward Chaining
• Given
?x lifeform(?x) => mortal(?x)
?x mammal(?x) => lifeform(?x)
?x dog(?x) => mammal(?x)
dog(fido)
• Prove
mortal(fido)
?x dog(?x) => mammal(?x)
dog(fido)
mammal(fido)
?
© Daniel S. Weld
18
Unification
• Emphasize variables with ?
• Useful for FO inference (modus ponens, …)
Also for compilation of FOPC -> propositional
• Unify(, ) 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
19
Unification Examples
• Unify( road(?a, kent), road(seattle, ?b) )
• Unify( road(?a, ?a), road(seattle, kent) )
• Unify( f(g(?x, dog), ?y), f(g(cat, ?y), dog) )
• Unify( f(g(?x)), f(?y) )
• Unify( f(g(?x)), f(?x) )
© Daniel S. Weld
20
Properties of Resolution
• Sound
• Complete
• But satisifability of FO
Logic is only semi-decidable
?x human(?x) => male(father(?x))
?y male(?y) => human(?y)
human(Fred)
Prove: male(Bob)
© Daniel S. Weld
26
Properties of Resolution
• Sound
• Complete
• But satisifability of FO
Logic is only semi-decidable
h(?x)  m(f(?x))
m(?y)  h(?y)
h(F)
Prove: m(B)
© Daniel S. Weld
27
Properties of Resolution
• Sound
• Complete
• But satisifability of FO
Logic is only semi-decidable
h(?x)  m(f(?x))
m(?y)  h(?y)
h(F)
m(B)
© Daniel S. Weld
28
Resolution Proof
{[m(?y), h(?y)], [h(?x), m(f(?x))], [h(F)], [m(B)]}
?x=F
[m(f(F))]
?y=f(F)
[h(f(F))]
?x=f(F)
[m(f(f(F)))]
...
© Daniel S. Weld
29
Compilation to Prop. Logic I
• Typed Logic
city a,b connected(a,b)
• Universe
Cities: seattle, tacoma, enumclaw
• Equivalent propositional formula:
© Daniel S. Weld
30
Compilation to Prop. Logic II
• Universe
• Cities: seattle, tacoma, enumclaw
• Firms: IBM, Microsoft, Boeing
• First-Order formula
city c firm f
hasHQ(c, f)
• Equivalent propositional formula
© Daniel S. Weld
31
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
32
Revisiting Planning as SAT
P0
Q
P2
A1
0
R0
S0
2
B1
C1
T0
Initial
State
© Daniel S. Weld
Q
R2
S2
T2
Actions
Time 2
…
33
Medic SAT Compiler
Planner
Init state
Actions
Goal
Compiler
© Daniel S. Weld
Plan
Logic
Simplification
SAT
Solver
Decoder
34
Axioms
Axiom
Description / Example
Init
The initial state holds at t=0
Goal
The goal holds at t=2n
A  P, E
Frame
Paint(A,Red,t)  Block(A, t-1)
Paint(A,Red,t)  Color(A, Red, t+1)
Classical / Explanatory
At-least-one
Act1(…, t)  Act2(…, t)  …
Exclude
Act1(…, t)  Act2(…, t)
© Daniel S. Weld
35
Revisiting Planning as SAT
P0
Q
P2
A1
0
R0
S0
2
B1
C1
T0
Initial
State
© Daniel S. Weld
Q
R2
S2
T2
Actions
Time 2
…
36
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
37
KR with Description Logics
Abox
mother(jane)
child-of(jane, bob)
…
Assertions
Tbox
person
Term Defs
father
mother
grandmother
© Daniel S. Weld
38
Tbox
• Term definitions
• FO Language + inference organized into a
taxonomy, e.g:
father(x) = person(x) male(x)  y childof(y,x)
parent(x) = person(x)  y childof(y,x)
• Complexity of classifying new terms
subsumption
person
Subsumption hierarchy 
father
mother
grandmother
© Daniel S. Weld
39
Abox
• Assertions
• Abox – separate language + inference for
“propositional” assertions using Tbox terms
e.g. person(kelley)
© Daniel S. Weld
40
Debate
• Restricted language thesis
Disjunction, negation, particularization, order…
Natural kinds
• Restricted classification thesis
Concepts using contingent information:
Treatable disease, democratic country, illegal act
• Counterargument
• Constructs: Omit vs limit
Completeness
Efficiency
© Daniel S. Weld
41