Transcript FOL_review1
Suppose you know that you are going to fail or pass CS 205.
Further, since this is the only class you need to graduate, you
know that you are going to either not pass the class or graduate
on time.
Then you can derive the fact that you will either not pass or you
graduate on time.
Fail or Pass, not Pass or GraduateOnTime
Therefore Fail or GraduateOnTime
F
P
G
Fail
Pass
Graduate on time
FP
P G
FG
Special cases to be aware of…
F
P
Free
Parent
FP
P
F
Special cases to be aware of…
FP
P A B C
FABC
Special cases to be aware of…
FP
P (any legal sentence)
F (any legal sentence)
Logics in General
Language
Ontological
Commitment
Epistemological
Commitment
Propositional Logic
Facts
True / False /
Unknown
First-Order Logic
Fact, objects, relations True / False /
Unknown
Temporal Logic
Facts, objects,
relations, times
True / False /
Unknown
Probability Theory
Facts
Degree of belief
[0,1]
Fuzzy Logic
Degree of truth
[0,1]
Known interval value
First-Order Logic
• First-Order Logic assumes that the world
contains:
– Terms (Objects)
• E.g. people, houses, numbers, theories, colors, football
games, wars, centuries, paintings, bicycles …
– Predicates (returns true, false)
• E.g. red, round, prime, bogus, multistoried, brother of,
bigger than, inside, outside, has color, occurred after, owns,
comes between, …
– Functions (Statements that return Terms)
• E.g. fatherOf, bestfriendOf, thirdquarterOf, onemorethan,
beginningOf, …
Syntax of First-Order Logic
•
•
•
•
•
•
•
Constants
Predicates
Functions
Variables
Connectives
Equality
Quantifiers
KingJohn, 2, TRUE …
Brother, > , …
Sqrt, LeftArmOf, …
x, y, a, b, …
¬
= (may be implement as equals predicate)
$"
Components of First-Order Logic
• Term
– Constant, e.g. Blue
– Function of constant, e.g. EyeColorOf(Joe)
• Atomic Sentence
– Predicate relating objects (no variable)
• Brother (John, Richard)
• Married (Mother(John), Father(John))
• Complex Sentences
– Atomic sentences with logical connectives
• Brother (John, Richard) Brother (John, Father(John))
Components of First-Order Logic
• Quantifiers
– Each quantifier defines a variable for the duration of
the following expression, and indicates the truth of
the expression…
• Universal quantifier “for all” "
– The expression is true for every possible value of the
variable
• Existential quantifier “there exists” $
– The expression is true for at least one value of the
variable
Universal Quantification
• " <variables> <sentence>
• "X At(X, UCR) Smart(X)
Everyone at UCR is smart
• Equivalent to the conjunction of all instantiations of P
– At(Mike, UCR) Smart(Mike)
– At(Laurie, UCR) Smart(Laurie)
– At(Sarah, UCR) Smart(Sarah)
–…
A Common Mistake to Avoid
• Typically is the main connective with "
• Common mistake: using as the main
connective with "
• "x At(x, UCR) Smart(x)
• Means “Everyone is at UCR and everyone is smart”!
Existential Quantification
• $ <variables> <sentence>
• $X At(X, UCR) Smart(X)
Someone at UCR is smart
• Equivalent to the disjunction of instantiations of P
–
–
–
–
At(Mike, UCR) Smart(Mike)
At(Laurie, UCR) Smart(Laurie)
At(Sarah, UCR) Smart(Sarah)
…
Another Common Mistake to Avoid
• Typically, is the main connective with $
• Common mistake: using as the main
connective with $
• $ x At(x, UCR) Smart(x)
• Is true if there is anyone who is not at UCR!
Examples
• Everyone likes McDonalds
–
"x likes(x, McDonalds)
• Someone likes McDonalds
–
$x likes(x, McDonalds)
• All children like McDonalds
–
"x child(x) likes(x, McDonalds)
• Everyone likes McDonalds unless they are allergic to it
–
–
"x likes(x, McDonalds) allergic(x, McDonalds)
"x allergic (x, McDonalds) likes(x, McDonalds)
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”
Nesting Quantifiers
• Everyone likes some kind of food
"y $x food(x) likes(y, x)
• There is a kind of food that everyone likes
$x "y food(x) likes(y, x)
• Someone likes all kinds of food
$y "x food(x) likes(y, x)
• Every food has someone who likes it
"x $y food(x) likes(y, x)
Examples
• Quantifier Duality
– Not everyone like McDonalds
("x likes(x, McDonalds))
$x likes(x, McDonalds)
– No one likes McDonalds
($x likes(x, McDonalds))
"x likes(x, McDonalds)
More Sentences
• Brothers are siblings
"x,y Brother(x,y) Sibling(x, y)
• Sibling is “symmetric”
"x,y Sibling(x,y) Sibling(y, x)
Even More Sentences
• One’s mother is one’s female parent
"x,y Mother(x,y) (Female(x) Parent(x,y))
• A first cousin is a child of a parent’s sibling
"x,y FirstCousin(x,y) $p,ps Parent(p,x)
Sibling(ps,p) (Parent(ps,y)
Comments About Quantification
• To say “everyone likes McDonalds”, the following is too
broad!
– "x, likes(x, McDonalds)
– For example: likes (myBicycle, McDonalds)
• We mean: Every one (who is a human) likes McDonalds
– "x, person(x) likes(x, McDonalds)
• Essentially, the left side of the rule declares the class of the
variable x. Constraints like this are often called “domain
constraints”
• Or, we can simply state that our KB is only about (i.e. its
domain is) humans.
Equality
• We allow the usual infix = operator
– Father(John) = Henry
– "x,y sibling(x, y) (x=y)
• Or we can use
– equals(Father(John) , Henry)
– "x,y sibling(x, y) equals(x,y)
• Example: (Sibling in terms of Parent)
"x,y Sibling(x,y) [….
• Example: (Sibling in terms of Parent)
"x,y Sibling(x,y) [….
I am going to need
four variables…
m
x
f
y
• Example: (Sibling in terms of Parent)
"x,y Sibling(x,y) [¬(x=y)
m
x
¬(x=y)
f
y
• Example: (Sibling in terms of Parent)
"x,y Sibling(x,y) [¬(x=y) $m,f ¬(m=f)
¬(m=f)
m
x
¬(x=y)
f
y
• Example: (Sibling in terms of Parent)
"x,y Sibling(x,y) [¬(x=y) $m,f ¬(m=f) Parent(m,x)
Parent(f,x)
¬(m=f)
m
f
Parent(m,x) Parent(f,x)
x
¬(x=y)
y
• Example: (Sibling in terms of Parent)
"x,y Sibling(x,y) [¬(x=y) $m,f ¬(m=f) Parent(m,x)
Parent(f,x) Parent(m,y) Parent (f,y)]
¬(m=f)
m
Parent(m,x) Parent(f,x)
x
f
Parent(m,y) Parent (f,y)
¬(x=y)
y
Knowledge engineering in FOL
1. Identify the task
2. Assemble the relevant knowledge
3. Decide on a vocabulary of predicates,
functions, and constants
4. Encode general knowledge about the domain
5. Encode a description of the specific problem
instance
6. Pose queries to the inference procedure and
get answers
7. Debug the knowledge base
Resolution
• Resolution allows a complete inference mechanism
(search-based) using only one rule of inference
• Work by proof by contradiction
• Resolution rule:
– Given: P1 P2 P3 … Pn, and P1 Q1 … Qm
– Conclude: P2 P3 … Pn Q1 … Qm
Complementary literals P1 and P1 “cancel out”
• To prove a proposition F by resolution,
–
–
–
–
Start with F
Resolve with a rule from the knowledge base (that contains F)
Repeat until all propositions have been eliminated
If this can be done, a contradiction has been derived and the
original proposition F must be true.
Propositional Resolution Example
• Rules
– If it is cold and there is precipitation, it will be snow
– If it is January, it will be cold
– If you see clouds, there will be precipitation
• Facts
– It is January
– There are clouds
KB
• Prove
– snow
ASK(KB |-
snow )
¬cold ¬precipitation snow
¬January cold
¬clouds precipitation
January
clouds
We want to prove snow
KB |- snow
So we assume the opposite of
snow and add it to our
knowledge base
TELL(KB, ¬snow)
And we look for a contradiction…
¬cold ¬precipitation snow
¬January cold
¬clouds precipitation
January
clouds
¬cold ¬precipitation snow
¬January cold
¬clouds precipitation
January
Clouds
¬snow
¬snow
¬cold ¬precipitation snow
¬January cold
¬clouds precipitation
January
(¬cold ¬precipitation) snow
clouds
¬snow
¬cold ¬precipitation
¬cold ¬precipitation
¬cold ¬precipitation ¬January cold
¬January ¬precipitation
¬cold ¬precipitation snow
¬January cold
¬clouds precipitation
January
clouds
¬snow
¬cold ¬precipitation
¬January ¬precipitation
¬cold ¬precipitation snow
¬January cold
¬clouds precipitation
January
clouds
¬snow
¬cold ¬precipitation
¬January ¬precipitation
¬January ¬clouds
¬January ¬precipitation
¬clouds precipitation
¬January ¬clouds
¬cold ¬precipitation snow
¬January cold
¬clouds precipitation
January
clouds
¬snow
¬cold ¬precipitation
¬January ¬precipitation
¬January ¬clouds
¬clouds
Contradiction!
January
¬January ¬clouds
¬clouds
So ASK(KB |-
snow )
is true
But what about FOL?
Two problems:
We cannot resolve ¬J(y) c(y) with ¬c(x) ¬p(x) because
one fact is about y and the other fact is about x.
Second, maybe our knowledge base is not in the right format
to allow resolution. Resolution only works if the knowledge
base is in conjunctive normal form (CNF).
CNF means a list (really a conjunction) of disjunctions
"x cat(x) likes(x, Fish)
"x "y (cat(x) likes(x,y)) eats(x,y)
cat(Ziggy)
¬c(x) ¬p(x)
¬J(y) c(y)
¬c(z) p(z)
In CNF
In CNF
We have seen that we can do resolution when the KB is in CNF.
But most KB are not is that format.
Theorem: We can convert any KB to CNF
•
•
•
•
•
•
•
Eliminate Implications
Move inwards
Standardize Variables
Move Quantifiers left
Skolemize {Eliminate Existential Quantifiers, Drop Universal Quantifiers }
Distribute over
Flatten nested conjunctions and disjunctions.
Note that we must do the steps in order!
The process is called Skolemization
We can always make something like this…. into something like this
"x cat(x) likes(x, Fish)
"x "y (cat(x) likes(x,y)) eats(x,y)
cat(Ziggy)
¬c(x) ¬p(x)
¬J(y) c(y)
¬c(z) p(z)
We cannot resolve ¬J(y) c(y) with ¬c(x) ¬p(x) because
one fact is about y and the other fact is about x.
We can solve this problem with Substitution (Binding,
Instantiation)
Example: SUBST{x/y} is a substitution indicating that y should
be substituted for x.
So we have
¬J(y) c(y)
¬c(x) ¬p(x)
We do a substitution SUBST{x/y} to get
¬J(y) c(y)
¬c(y) ¬p(y)
We can now resolve these
¬J(y) c(y)
¬c(y) ¬p(y)
¬J(y) ¬p(y)
¬c(x) ¬p(x)
¬J(y) c(y)
¬c(z) p(z)
Bad News
• Even with heuristics search resolution is exponential in
general.
• Resolution is complete, but only semidecidable.
If our KB implies A (or it implies A), resolution will find
the proof in finite time. But if the KB does not implies A
(or A), resolution will simply run forever.