Transcript presentation source

Encoding Knowledge with
First Order Predicate Logic
Outline:
Motivation
Predicate calculus terminology
Expressing knowledge in logic
An example proof by resolution
Formal interpretations and satisfiability
CSE 415 -- (c) S. Tanimoto, 2004
Predicate Logic
1
Motivation: More Accurate and
General Representations of
Knowledge
“If Willy is a bird, then Willie can fly.”
Propositional calculus:
P: Willy is a bird
Q: Willy can fly
P -> Q
“Any bird can fly.”
Predicate calculus
Forall x (Bird(x) -> CanFly(x) )
CSE 415 -- (c) S. Tanimoto, 2004
Predicate Logic
2
Another Example
“John’s grandfather was a blacksmith, and his mother
was a seamstress.”
Propositional calculus:
P1: John’s grandfather was a blacksmith.
P2: John’s grandmother was a seamstress.
P&Q
Predicate calculus:
Q1(x): x is a blacksmith.
Q2(x): x is a seamstress.
f(x): grandfather of x.
Q1(f(x)) & Q2(m(x))
CSE 415 -- (c) S. Tanimoto, 2004
Predicate Logic
3
Terminology of the Predicate
Calculus
Predicate symbols:
P, Q, R, P1, P2, ... , Q1, Q2, ..., R1, R2, ...
If P takes n arguments, we call P an n-ary predicate
P( term1, term2, . . . , termn)
n >= 0
Function symbols:
f, g, h, f1, f2, . . . , g1, g2, . . . , h1, h2, . . .
A term is either:
a constant: e.g., a, b, c, a1, a2, . . . , b1, b2, . . . , c1, c2, . . .
a variable: e.g., x, y, z, x1, x2, . . . , y1, y2, . . . , z1, z2, . . .
an n-ary function symbol, followed by n terms in parentheses.
Examples of terms: x, a, f(x), g1(a, y), h(f(x), g(y, b))
CSE 415 -- (c) S. Tanimoto, 2004
Predicate Logic
4
Well-Formed Formulas
Atomic formula: an n-ary predicate symbol followed by n terms in
parentheses:
e.g., P(x, f(x, a, y))
If F is an atomic formula, then it is a well-formed formula (WFF).
Compound formula: a statement formed from one or more WFFs
using logical connectives.
If F is a compound formula, then it is a WFF.
e.g., P(x, f(x, a, y)) v (Q -> R(x))
Quantified formula: a statement formed from a WFFs by prefixing it
with a quantifier and a variable.
e.g., (Forall x) (P(x, f(x, a, y)) v (Q -> R(x)))
(Exists y) Q(y)
If F is a quantified formula, then it is a WFF.
CSE 415 -- (c) S. Tanimoto, 2004
Predicate Logic
5
A Syllogism for
Predicate Logic
Coloured flowers are always scented.
I dislike flowers that are not grown in the open air.
No flowers grown in the open air are colourless.
Lewis Carroll
Therefore, I dislike all flowers that are not scented.
CSE 415 -- (c) S. Tanimoto, 2004
Predicate Logic
6
Encoding the Syllogism
Predicate symbols:
C(x)
S(x)
D(x)
A(x)
= x is coloured.
= x is scented.
= I dislike x.
= x is grown in the open air.
CSE 415 -- (c) S. Tanimoto, 2004
Predicate Logic
7
Encoding the Syllogism
Coloured flowers are always scented.
(forall x) ( C(x) -> S(x) )
I dislike flowers that are not grown in the open air.
(forall x) ( ~A(x) -> D(x) )
No flowers grown in the open air are colourless.
(forall x) ( A(x) -> ~~C(x) )
Therefore, I dislike all flowers that are not scented.
(forall x) (~S(x) -> D(x) )
CSE 415 -- (c) S. Tanimoto, 2004
Predicate Logic
8
Proof by Resolution:
(1) Negate the conclusion
Coloured flowers are always scented.
(forall x) ( C(x) -> S(x) )
I dislike flowers that are not grown in the open air.
(forall x) ( ~A(x) -> D(x) )
No flowers grown in the open air are colourless.
(forall x) ( A(x) -> ~~C(x) )
It is not the case that I dislike all flowers that are not scented.
~(forall x) (~S(x) -> D(x) )
CSE 415 -- (c) S. Tanimoto, 2004
Predicate Logic
9
Proof by Resolution:
(2) Obtain Clause Form
Coloured flowers are always scented.
(forall x) ( C(x) -> S(x) )
(forall x) (~C(x) v S(x) ) Rewrite -> using ~ and v.
~C(x) v S(x)
Drop leading universal quantifier.
The other clauses are:
A(x) v D(x)
~A(x) v C(x)
(exists x) ~(~S(x) -> D(x) ) Move negation inward
(exists x) (~S(x) & ~D(x) ) DeMorgan’s law
~S(a) & ~D(a)
Introduce Skolem constant
~S(a), ~D(a)
Break into 2 clauses.
CSE 415 -- (c) S. Tanimoto, 2004
Predicate Logic
10
Proof by Resolution:
(3) Resolve
P1: ~C(x) v S(x)
P2: A(y) v D(y)
P3: ~A(z) v C(z)
P4: ~S(a)
P5: ~D(a)
P6: A(a)
P7: C(a)
P8: S(a)
P9: []
P2, P5
P3, P6
P1, P7
P4, P8
variables are standardized apart.
{ a/y }
{ a/z }
{ a/x }
{}
CSE 415 -- (c) S. Tanimoto, 2004
Predicate Logic
11
Formal Interpretations
An interpretation for a given formula W consists of
the following:
A domain D of elements that can be referred to by terms. E.g.,
D = (0, 1, 2, . . . }
An assignment that maps each constant symbol of W to an
element of D.
For each n-ary function symbol of W a mapping from n-tuples
of elements of D to single elements of D.
For each n-ary predicate symbol of W a mapping from ntuples of elements of D to {T, F}.
CSE 415 -- (c) S. Tanimoto, 2004
Predicate Logic
12
Example of Interpretation
Let W = (forall x) (P(a) & Q(x, a) )
An interpretation for W:
D = { apple, peach }
{ a = apple }
mapping for constants
{}
mappings for functions
{ P(apple) = T, P(peach) = T; mappings for predicates
Q(apple,apple) = T, Q(apple, peach) = T,
Q(peach,apple) = T, Q(peach, peach) = T }
CSE 415 -- (c) S. Tanimoto, 2004
Predicate Logic
13
Satisfiability
A formula W is satisfiable iff there exists some
interpretation of W that make W true.
A formula W is unsatisfiable iff there does NOT
exist any interpretation of W that make W true.
Then W is inconsistent. W is a contradiction.
If every interpretation of W satisfies W (makes W
true), then W is a tautology.
If I is an interpretation for W that satisfies W , then I
is a model for W.
CSE 415 -- (c) S. Tanimoto, 2004
Predicate Logic
14
Another Interpretation
Let W = (forall x) (P(a) & Q(x, a) )
An interpretation for W:
D = { 0, 1, 2, . . . }
{a=0}
{}
{ P(n) iff n = 0;
Q(m,n) iff n > m. }
mapping for constants
mappings for functions
mappings for predicates
Note that ~Q(x, x).
This interpretation fails to satisfy W. It’s not a model for W.
CSE 415 -- (c) S. Tanimoto, 2004
Predicate Logic
15
The Basis of Proof by
Resolution
Resolution is used to prove that a given set of
clauses is inconsistent. (i.e., it cannot have a
model).
Each time a resolvent is formed, it is added to the
set of clauses. This does not change the
consistency of the set.
However, if the null clause is ever added to the set,
then it becomes very obvious that the set is
inconsistent.
CSE 415 -- (c) S. Tanimoto, 2004
Predicate Logic
16