Transcript Outline for 4/2

Outline
• Recap
• Knowledge Representation I
• Textbook: Chapters 6, 7, 9 and 10
Some KR Languages
•
•
•
•
•
•
•
•
•
Propositional Logic
Predicate Calculus
Frame Systems
Rules with Certainty Factors
Bayesian Belief Networks
Influence Diagrams
Semantic Networks
Concept Description Languages
Nonmonotonic Logic
In Fact…
• All popular knowledge representation systems are
equivalent to (or a subset of)
– Logic (Propositional Logic or Predicate Calculus)
– Probability Theory
Propositional Logic
• Syntax
– Atomic sentences: P, Q, …
– Connectives:  , , , 
• Semantics
– Truth Tables
• Inference
–
–
–
–
–
Modus Ponens
Resolution
DPLL
GSAT
Resolution
• Complexity
4
Notation




=
}
Implication (syntactic symbol)
Inference
Entailment
• Sound
• Complete

=
implies =
implies 
5
Propositional Logic: SEMANTICS
• Multiple interpretations
– Assignment to each variable either T or F
– Assignment of T or F to each connective via defns
P
Q
T F
T T F
F F F
PQ
P
Q
T F
T T T
F T F
PQ
P
Q
T F
T T F
F T T
PQ
Note: (P  Q) equivalent to  P  Q
P
T F
F T
P
FOL Definitions
• Constants: a,b, dog33.
– Name a specific object.
• Variables: X, Y.
– Refer to an object without naming it.
• Functions: father-of
– Mapping from objects to objects.
• Terms: father-of(father-of(dog33))
– Refer to objects
• Atomic Sentences: in(father-of(dog33), food6)
– Can be true or false
– Correspond to propositional symbols P, Q
7
Terminology
•
•
•
•
Literal u or u, where u is a variable
Clause disjunction of literals
Formula, , conjunction of clauses
(u) take  and set all instances of u true; simplify
– e.g. =((P, Q)(R, Q)) then (Q)=P
• Pure literal var appearing in a formula either as a
negative literal or a positive literal (but not both)
• Unit clause clause with only one literal
Definitions
• valid = tautology = always true
• satisfiable = sometimes true
• unsatisfiable = never true
1)
2)
3)
4)
smoke  smoke
smoke  smoke
smoke  fire
 smoke  fire
valid
satisfiable
(smoke  fire)  (smoke  fire)

( smoke
 fire)
(smoke
(smoke
 fire)
 smoke
 firefire) valid
smoke  fire  fire
valid
9
Inference
• Backward Chaining (Goal Reduction)
– Based on rule of modus ponens
– If know P1 ...  Pn and know (P1 ...  Pn )=> Q
– Then can conclude Q
• Resolution (Proof by Contradiction)
• GSAT
Student-Prof Example
• Some students like all professors. No student likes
any tough professors. Thus, no professor is tough.
Unification and Substitution
• Substitution
– a set of pairs s={x=a, y=b}
– Instance of a substitution
• F=p(x,y,f(a)), Fs=applying s on F={p(a,b,f(a)}
• Replacement is simultaneous t={x=a,y=x}
– Composition of Substitutions st=?
• Unifier: a substitution that makes two expressions the same
– Most General Unifier: MGU is a smallest unifier;
– Example: unify p(f(x), h(y), a) and p(f(x), z, a)
Normal Forms (Chapter 9, page
281)
• 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)
Removing Existential
• Skolem Constants (page 281)
• Skolem Functions (page 282)
Conversion to Normal Form
•
•
•
•
•
•
•
Remove implications
Move negation inwards
Standardize variables
Move quantifiers left
Skolemization (every body has a heart)
Distribute and, or’s
Clausal Form
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!
Resolution Refutation Procedure
• Page 281 of text
–
–
–
–
Negating theorem
Normal Form Conversion
Derive an empty clause
Answer Extraction
Student-Prof Example
• FOL sentences
• Conclusion clause: negate
• Use refutation to prove.
Finding Answers
•
•
•
•
Father’s father is a grandfarther
John is Ken’s father
Larry is Joh’s father
Question: who is Ken’s grandfather?
Application: Logic Programming
• Prolog (page 304)
–
–
–
–
–
–
–
Sequence of sentences
Horn clauses
Queries
Negation as failure
Distinct names = distinct objects
Built-in predicates for math, etc.
Example: membership function
Logic Programming (page 304)
• Defining membership
– member(X, [X|L]).
– member(X, [Y|L]) :- member(X,L).
• How does Logic Programming Systems find
answers?
Semantic Networks (page 317)
• Graphically represent the
following
–
–
–
–
–
–
Birds are animals
Mammals are animals
Penguins are birds
Cats are mammals
Birds fly
Penguins don’t fly
–
–
–
–
Animals are alive
Animals don’t fly
Birds have two legs
Mammals have 4 legs
• Semantic Networks have
– Properties
– Subset links
– Member links
GSAT
[1992]
Procedure GSAT (CNF formula: , max-restarts, max-climbs)
For i := 1 to max-restarts do
A := randomly generated truth assignment
for j := 1 to max-climbs do
if A satisfies  then return yes
A := random choice of one of best successors to A
;; successor means only 1 (var,val) changes from A
;; best means making the most clauses true