Transcript a,b

Soundness and Completeness
KB |- S: S is provable from KB.
A proof procedure is sound if:
If KB |- S, then KB |= S.
That is, the procedure produces only correct
consequences.
A proof procedure is complete if:
If KB |= S, then KB |- S.
That is, the procedure produces all the
consequences.
Ideally, the procedure should be sound and
complete. (Ideals are nice in theory).
1
Knock Knock Logic
Who’s there?
Joe

Mike, Sally
Background knowledge:
Mike => Sally
Sally  Rita
Hence?
2
Modus Ponens
From A and A  B, infer B.
A and B can be any sentence.
Modus ponens with a few axiom schemas is
sound and complete:

A  (B  A)
A  (B  C)  ((A B)  (A  C))
( A   B)  (B  A)
More in the book.
3
Some Useful Equivalences
 Q is equivalent to: P  Q
(P  Q) is equivalent to: P  Q
(P  Q) is equivalent to: P  Q
P
4
Normal Forms
CNF = Conjunctive Normal Form
Conjunction of disjuncts (each disjunct =
“clause”)
(P  Q)  R
(P  Q)  R
(P  Q)  R
(P  Q)  R
P  Q  R
(P  R)  (Q  R)
5
Resolution
A  B  C,
C  D  E
A  B  D  E
Refutation Complete
Given an unsatisfiable KB in CNF,
Resolution will eventually deduce the empty clause
Proof by Contradiction
To show  = Q
Show   {Q} is unsatisfiable!
6
Knock Knock Resolution
Joe

Mike,
Sally,
 Mike  Sally,
Sally  Rita
7
Resolution Example prove P
(A B C) (B) (B D)
(C A D)
(D P Q) (Q)
8
Computational Complexity
Determining satisfiability is NP-complete.
Even when all clauses have at most 3 literals.
Hence, also validity and entailment testing are
NP-complete.
But, some recent progress is encouraging!
If all clauses have at most 2 literals, it is
polynomial.
But if the KB is in DNF, satisfiability is
polynomial.
What does this tell us about transforming a CNF
9
into a DNF knowledge base?
Horn Clauses
If every sentence in KB is of the form:
A  B  C  ...  F  Z
equivalently A  B  C  ...  F  Z
• Then Modus Ponens is
– Polynomial time, and
– Complete!
10
Horn Rule Inference
Backward or forward chaining.
P  Q  S
P1  Q  S1
R1  R2  Q
R1, R2, P.
11
Limitations of Prop. Logic
Cumbersome for large domains:
Man-Abraham, Man-Isaac, Man-Jacob
Woman-Sara, Woman-Rachel, Woman-Leah
Man-Abraham  Human-Abraham
Woman-Sara  Human-Sara
Cannot deal with infinite domains.
We’d like to say:
Abraham, Sara etc. are objects.
for all X, Man(X)  Human(X)
for all n, Integer(n)  Integer(n+1).
12
First Order Logic (FOPC)
We identify the objects in our domain.
Abraham, Sara, Isaac, Rachel,
Father-of(Isaac), Mother-of(Isaac).
Predicates specify properties of objects, and
tuples of objects:
Man(Abraham), Woman(Sara),
Married(Abraham, Sara).
Quantified formulas:
 X Man(X)  Human(X)
 X  Y Loves(Y,X).
13
FOL Definitions
Constants: a,b, dog33, Abraham.
Name a specific object.
Variables: X, Y.
Refer to an object without naming it.
Functions: dad-of
Mapping from objects to objects.
Terms: father-of(mother-of(dog33))
Refer to objects
Atomic Sentences: in(father-of(dog33), h1)
Can be true or false
Correspond to propositional symbols P, Q
14
More Definitions
Logical connectives:
Quantifiers:
, ,  
 Forall
 There exists
Examples
Abraham is a man.
All professors wear glasses.
Every person is loved by someone who isn’t
their mother.
15
Quantifier / Connective
Interaction
E(x) == “x is an elephant”
G(x) == “x has the color grey”
x E(x)  G(x)
equivalent to x E(x)  x G(x)?
x E(x)  G(x)
equivalent to x E(x)  x G(x)?
x E(x) G(x)
x E(x)  G(x)
x E(x) G(x)
16
Nested Quantifiers:
Order matters!
x y P(x,y)  y x P(x,y)
Examples
Every dog has a tail
Someone is loved by everyone
17
If your thesis is entirely vacuous,
add a few formulas in predicate
calculus.
- famous disgruntled advisor
18
FOPC Semantics
An interpretation includes:
A non-empty universe of discourse, O
A mapping from the constants to elements of O.
For every function symbol of arity n, a mapping
from O n to O.
For every predicate symbol of arity n, a subset of
O n.
We can now define the truth value of every
well formed formula.
19
Unification
Useful for first order inference
a,b city(a)  city(b)  connected(a,b)
city(kent)
city(seattle)
Also for compilation
Emphasize variables with ?
Unify(x, y) return mgu
Unify(city(?a), city(kent)) returns ?a/kent
20
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(?x))
21
Skolemization
 d t
dog(d)  connected(d, t)
x y person(y)  loves(y, x)
22