Transcript n07 - Computer Science at Rutgers

Propositional Logic
Reading: Ch. 7, AIMA 2nd Ed.
(skip 7.6-7.7)
Rutgers CS440, Fall 2003
Logic for knowledge representation
• Important problem:
knowledge representation = solving the problems of
– How to represent knowledge about problem domain
– How to reason using this knowledge in order to answer queries or
make decisions
• Knowledge-based agents
– Have knowledge representation in a formal language
– Can reason about world using inference in the language
– Can decide what action to take by inferring that the action is good
• Declarative agents
– Declare to agents facts about world
– Pose questions to get answers
Rutgers CS440, Fall 2003
Declarative knowledge-based agents
Rutgers CS440, Fall 2003
Wumpus world
•
Performance measure
Gold +1000, death –1000, step –1, arrow –10
•
Environment
- squares adjacent to wumpus are smelly
- squares adjacent to pits are breezy
- glitter iff gold is in the same square
- shooting kills wumpus if you are facing it
- shooting uses up the only arrow
- grabbing picks up gold if in the same square
- releasing drops the gold in same square
•
Sensors
Breeze, glitter, smell
•
Actuators
Left, right turn, forward, grab, release, shoot
Rutgers CS440, Fall 2003
Wumpus world characterization
• Observable
– No – only local perception
• Deterministic
– Yes – outcomes explicite
• Episodic
– No – sequential actions
• Discrete
– Yes
• Single-agent
– Yes
Rutgers CS440, Fall 2003
Exploring wumpus world
ok
ok
ok
A
Rutgers CS440, Fall 2003
Exploring wumpus world
P?
ok
B
P?
A
ok
ok
Rutgers CS440, Fall 2003
Exploring wumpus world
P?
ok
B
ok
P?
ok
A
Rutgers CS440, Fall 2003
Exploring wumpus world
P?
ok
ok
B
P? W?
ok
S
W?
A
Rutgers CS440, Fall 2003
Exploring wumpus world
P?
P
ok
ok
B
P? W? ok
ok
S
A
W?
W
How can we make these inferences automatically?
Rutgers CS440, Fall 2003
Logic
• Logic is a formal language for representing information such that
conclusions can be drawn
• A logic includes
– Syntax: specifies symbols in the language and how they can be
combined to form sentences
– Semantics: specifies what facts in the world a semantics refers to.
Assigns truth values to sentences based on their meaning in the
world.
– Inference procedure: mechanical method for computing (deriving)
new (true) sentences from existing sentences
entails
Representation:
Sentences
Sentences
semantics
follows
World:
Facts
Facts
Rutgers CS440, Fall 2003
Example
•
Language of arithmetic
–
–
–
–
•
4x+y > 0 is a sentence, 4x<y0 is not
4x+y > 0 is true iff number 4x+y is greater than zero
4x+y > 0 is true in a world where x=0, y = 1
4x+y > 0 is false in a world where x=0, y = 0
Hence, to build a logic-based representation:
1. Define a set of primitive symbols and the associated semantics
2. Logic defines the ways of putting there symbols together in order
to represent true facts about world
3. Logic defines ways of inferring new sentences from existing ones
Rutgers CS440, Fall 2003
Propositional (Boolean) logic
•
•
Simple language (but useful for key ideas and definitions)
Language syntax
– Atoms/Symbols: P12, B11, W33,, IS_HOT, IS_BREEZY, , …
User defines meaning of symbols.
– Connectives:  (and),  (or),  (implies),  (iff),  (not)
– Sentences or Well-formed-formulae (wff):
1. A symbol is a sentence
2. If S is a sentence, S (negation) is a sentence
3. If S and T are sentences, ST (conjunction), ST (disjunction), ST
(implication), ST (equivalence) are sentences
4. A finite number of applications of (1)-(3) is a sentence
Rutgers CS440, Fall 2003
Symbols & Sentences of Wumpus world
• Pij is “pit in (i,j)”
• Bij is “breeze in (i,j)”
• Wij is “wumpus in (i,j)”
• B11
• “Pits cause breezes in adjacent squares”
– B11  ( P12  P21 )
– B12  ( P11  P22  P13 )
– …
Rutgers CS440, Fall 2003
Semantics
• Association of elements of logical language (atoms &
sentences) with real world
• Propositional logic = associate atoms with propositions
E.g.,
–
–
–
–
P12 is associated with “pit is in cell (1,2)”
B11 is associated with “breeze is felt in cell (1,1)”
W33 is associated with “wumpus is in (3,3)”
IS_HOT is associated with “I am taking cs440”
• Association of atoms with propositions = interpretation
If atom  has value TRUE (1), then its interpretation P is true in
the world; otherwise  has value FALSE (0)
• E.g., P12 = 1 means “pit is in cell (1,2) is true”
Rutgers CS440, Fall 2003
Propositional truth tables
• Used to compute values of any sentence, given values of atoms
• Establishes meaning of propositional connectives
A
A
B
AB
AB
AB
AB
0
0
1
0
0
1
1
0
1
1
1
0
1
0
1
0
0
1
0
0
0
1
1
0
1
1
1
1
• The basic truth table can be used to evaluate any sentence by
applying the rules recursively
A  ( AB ) = 0  ( 01 ) = 1  ( 01 ) = 1  1 = 1
Rutgers CS440, Fall 2003
Models
• A model is an interpretation of a set of sentences such that each
sentence is True:
 is a model of a sentence S if S is true in 
( an interpretation of S satisfies  )
• A mathematical structure that represents the (problem in) real
world.
• Some other notions:
– Unsatisfiable: there is no interpretation that satisfies S
Rutgers CS440, Fall 2003
Models of Wumpus world
• Situation after detecting
nothing in (1,1), moving
up, breeze in (2,1)
• What are the possible
models for P?,
assuming only pits?
P?
• P12, P22, P31  {0,1}
B P?
A
• 8 possible models
P?
Rutgers CS440, Fall 2003
Models of Wumpus world
P
B
B
A
A
P
B
A
P
B
P
A
B
P
A
P
B
A
P
P
B
B
A
P
A
P
Rutgers CS440, Fall 2003
P
P
Are these the
models of Wumpus
world?
Wumpus Knowledge Base (KB)
• KB = { S1, S2, …, SN } – set of all sentences describing our
current knowledge of the world, where each sentence is in
propositional logic
• Wumpus world KB
S1: B11
S2: B21
S3: B11  ( P12  P21 )
S4: B21  ( P11  P22  P31 )
S5: P11
• Remember, models are interpretations where all Si are true
• How to find models?
Rutgers CS440, Fall 2003
Model checking: Enumeration of symbols
in sentences
• Check for valid models by enumerating all possible symbols
interpretations: KB = S1  S2  S3  S4  S5
B11
B21
P11
P12
P21
P22
P31
S1
S2
S3
S4
S5
KB
0
0
0
0
0
0
0
1
0
1
1
1
0
0
0
0
0
0
0
1
1
0
1
0
1
0
…
…
…
…
0
1
0
0
0
0
0
1
1
1
0
1
0
0
1
0
0
0
0
1
1
1
1
1
1
1
0
1
0
0
0
1
0
1
1
1
1
1
1
0
1
0
0
0
1
1
1
1
1
1
1
1
0
1
0
0
1
0
0
1
1
0
0
1
0
…
…
1
0
…
1
1
1
1
1
1
Rutgers CS440, Fall 2003
…
1
1
1
0
0
Model checking: Enumeration of symbols
in sentences
• Models are shown in red!
• How many enumerations? 27
B11
B21
P11
P12
P21
P22
P31
S1
S2
S3
S4
S5
KB
0
0
0
0
0
0
0
1
0
1
1
1
0
0
0
0
0
0
0
1
1
0
1
0
1
0
…
…
…
…
0
1
0
0
0
0
0
1
1
1
0
1
0
0
1
0
0
0
0
1
1
1
1
1
1
1
0
1
0
0
0
1
0
1
1
1
1
1
1
0
1
0
0
0
1
1
1
1
1
1
1
1
0
1
0
0
1
0
0
1
1
0
0
1
0
…
…
1
0
…
1
1
1
1
1
1
Rutgers CS440, Fall 2003
…
1
1
1
0
0
Models of Wumpus world
• Rows of the truth table where the last column (KB) is true (I.e.,
all sentences are true)
P
B
B
A
A
P
B
A
P
P
B
A
B
P
A
P
KB
B
A
P
P
B
B
A
P
P
Rutgers CS440, Fall 2003
A
P
P
Inference & entailment
• Given KB, what else can we conclude about the world?
E.g., does a goal (a.k.a. query, conclusion, theorem)
sentence G follow from KB?
• Note: we do not know semantics.
Hence: we have to determine if all models of KB are models
of G.
• I.e., KB entails G, ( KB |= G ) iff G is true whenever KB is true
• KB |= G iff KB  G is valid
(A sentence is valid iff it is true under all possible
interpretations)
• KB |= G iff KB  G is unsatisfiable
Rutgers CS440, Fall 2003
Wumpus world entailment
• G = “(1,2) is safe”
• Does KB |= G ?
P
B
B
A
A
P
B
A
P
P
B
A
B
P
A
M(KB)M(G)
P
B
KB
A
YES!
P
P
B
B
A
P
P
G
Rutgers CS440, Fall 2003
A
P
P
Wumpus world entailment (II)
• G: P12
• Column KBG is all 1, hence it is valid. Thus, KB |= G.
• Conclusion G follows from KB no matter what the
interpretations
B11
B21
P11
P12
P21
P22
P31
S1
S2
S3
S4
S5
KB
G
KBG
0
0
0
0
0
0
0
1
0
1
1
1
0
1
1
0
0
0
0
0
0
1
1
0
1
0
1
0
1
1
…
…
…
…
…
0
1
0
0
0
0
0
1
1
1
0
1
0
1
1
0
1
0
0
0
0
1
1
1
1
1
1
1
1
1
0
1
0
0
0
1
0
1
1
1
1
1
1
1
1
0
1
0
0
0
1
1
1
1
1
1
1
1
1
1
0
1
0
0
1
0
0
1
1
0
0
1
0
1
1
…
…
1
0
…
1
1
1
1
1
1
…
1
1
Rutgers CS440, Fall 2003
1
0
0
…
0
1
Inference by enumeration properties
• The truth table method of inference is complete for
Propositional Logic because we can always enumerate all 2N
rows for the N propositional symbols that occur.
• But this is exponential in N. In general, it has been shown that
the problem of checking if a set of sentences in PL is satisfiable
is NP-complete.
• Can be implemented using which search procedure?
– Depth-first search.
•
(The truth table method of inference is not complete for FirstOrder Logic.)
Rutgers CS440, Fall 2003
Inference procedures
•
Inference methods
1. Model checking
– Enumeration (seen previously)
– Improved backtracking & local search
2. Inference using sound rules of inference
•
•
•
•
•
Derive new sentences that are true in all cases where premises are true.
E.g., ( P = 1 and PQ = 1 )  Q = 1
Construct a proof that a given sentence G can be derived from KB using
a sequence of inference rules
Rules R are sound if, for a KB and sentence G, KB |- G under rules R
implies KB |= G
If when KB |= G there exists a proof of G from KB using R, then the R is
complete
If R is sound and complete we can prove entailment by searching
for a proof
Rutgers CS440, Fall 2003
(Some) Sound rules of inference
Name
Premise(s)
Derived sentence
Modus ponens
A, AB
B
And introductions
A, B
AB
And elimination
AB
A
Double negations
 A
A
Unit resolutions
AB, B
A
Resolution
AB, B  C
AC
Equivalence
elimination
AB
(A  B)  (B  A)
(mode that affirms)
Rutgers CS440, Fall 2003
Using SRI in Wumpus world
1. S1: B11
S2: B21
S3: B11  ( P12  P21 )
S4: B21  ( P11  P22  P31 )
S5: P11
KB
2.
3.
4.
5.
6.
S6: (B11(P12P21))( P12P21)B11)
S7: (P12P21)B11
S8:  B11 ( P12  P21 )
S9: ( P12  P21 )
S10: P12  P21
•
Monotonicity property:
• adding new sentences to a KB does not change entailment
( KB |= G  KB  S |= G ). It can only lead to new
conclusions.
Rutgers CS440, Fall 2003
S3 & equivalence elimin.
S6 & and elimination
S7 & negation
S1, S8, & modus ponens
S9 & DeMorgan
Inference using Resolution
• A single rule sufficient for complete inference procedure, when
coupled with a complete search algorithm
( A  B, A) leads to B
( A  B, A  C) leads to B  C
Rutgers CS440, Fall 2003
Resolution in Wumpus world
• Continue from previous example by moving A into (1,2) and not
feeling breeze
2.
S1: B11, S2: B21, S3: B11  ( P12  P21 ), S4: B21  ( P11  P22  P31 ),
S5: P11
KB
S10: P12  P21
previously inferred
3.
4.
S11: B12
S12: B12  ( P11  P22  P13 )
percept
rule
5.
6.
S13:  P22
S14:  P13
S11 & S12 & equiv. elim., add elim, modus ponens
7.
8.
9.
S15: P11  P22  P31
S16: P11  P31
S17: P31
S4 & S2 & equiv. elim. & modus ponens
1.
S15, S13 & resolution
S16, S5 & resolution
Rutgers CS440, Fall 2003
Resolution algorithm & CNF
•
•
How to effectively use resolution? It only applies to disjunctions
of symbols.
CNF: conjunctive normal forms
– Every KB can be represented as a CNF
– Every sentence can be represented as a conjunction of
disjunctions of literals
•
Method:
1.
2.
3.
4.
Eliminate equivalences (conjunction of implications)
Eliminate implications (disjunctions of negation & symbols/sent)
Propagate negations to literals (DeMorgan)
Done!
Rutgers CS440, Fall 2003
CNF in Wumpus world
1.
2.
3.
4.
5.
6.
S3: B11  ( P12  P21 )
( B11  ( P12  P21 ) )  ( ( P12  P21 ) B11 )
( B11  ( P12  P21 ) )  (( P12  P21 )  B11 )
( B11  P12  P21 )  ( ( P12   P21 )  B11 )
( B11  P12  P21 )  (  P12  B11 )  (  P21  B11 )
:CNF
Rutgers CS440, Fall 2003
Resolution refutation algorithm
•
•
•
Relies on proof by contradiction (refutation):
Assume goal sentence is false, prove KB does not hold.
Remember, KB |= G iff KB  G is unsatisfiable, i.e.,
KB  G = {}
Algorithm:
1. Convert all sentences in KB to CNFs
2. Resolve all pairs of CNFs into new clauses
3. Check for contradiction
– Resolution refutation is complete
Rutgers CS440, Fall 2003
Resolution refutation in Wumpus world
KB
Rutgers CS440, Fall 2003
G
Special case: Horn clauses and forwardbackward chaining
• Restricted set of clauses: Horn clauses
disjunction of literals where at most one is positive, e.g.,
A  B  C or A  B
• Why Horn clauses?
– Every Horn clause can be written as an implication, e.g.,
A  B  C =  ( A  B )  C = ( A  B )  C
A  B =  ( A  B ) = ( A  B )  0(integrity constraint)
– Inference in Horn clauses can be done using forward-backward
(F-B) chaining in linear time
Rutgers CS440, Fall 2003
Example of FC
Rutgers CS440, Fall 2003
How good is PL as a representational
language?
• Not very expressive
– Cannot express complex environments concisely
– E.g., need to write separate rules for every square in Wumpus
world even though they do not change from square to square
Bij  ( Pi,j-1  Pi,j+1  Pi-1,j  Pi+1,j ), for all (i,j)
– E.g., to specify there is exactly one wumpus in the world, need to specify
• There is at least one: ?
• There is at most one: ?
Rutgers CS440, Fall 2003
Announcement
• New assignment type: mini project-presentations
•
•
•
•
Prepared by a team of two students
Related to a topic discussed in class
Presented in class, 15-20 mins
Will be graded, 15% of total grade
(new grade distribution: final 30%, midterm 30%, hw 25%,
presentation 15%)
• First presentation:
Oct 15, Bayesian network software
• Prepare slides and handouts (web page, pdf file is ok) for the
class
Rutgers CS440, Fall 2003