Transcript PowerPoint file

Explorations in Artificial Intelligence
Prof. Carla P. Gomes
[email protected]
Module 3-1-2
Logic Based Reasoning
Proof Methods
1
Proofs Methods
2
Proof methods
Proof methods divide into (roughly) two kinds:
– Application of inference rules
• Legitimate (sound) generation of new sentences from old
• Proof = a sequence of inference rule applications
Can use inference rules as operators in a standard search algorithm
• Different types of proofs
– Model checking
• truth table enumeration (always exponential in n)
Current
module
we’ve talked about this approach
• improved backtracking, e.g., Davis--Putnam-Logemann-Loveland
(DPLL)
• (including some inference rules)
• heuristic search in model space (sound but incomplete)
e.g., min-conflicts-like hill-climbing algorithms
Next
modules
Proof
The sequence of wffs (w1, w2, …, wn) is called a proof (or deduction) of wn from
a set of wffs Δ iff each wi in the sequence is either in Δ or can be inferred from a
wff (or wffs) earlier in the sequence by using a valid rule of inference.
If there is a proof of wn from Δ, we say that wn is a theorem of the set Δ.
Δ├ wn
(read: wn can be proved or inferred from Δ)
The concept of proof is relative to a particular set of inference rules used. If we
denote the set of inference rules used by R, we can write the fact that wn can be
derived from Δ using the set of inference rules in R:
Δ├ R wn
(read: wn can be proved from Δ using the inference rules in R)
Propositional logic:
Rules of Inference or Methods of Proof
How to produce additional wffs (sentences) from other ones? What steps can we
perform to show that a conclusion follows logically from a set of hypotheses?
Example
Modus Ponens
P
PQ
______________
Q
The hypotheses (premises) are written in a column and the conclusions below the bar
The symbol  denotes “therefore”. Given the hypotheses, the conclusion follows.
The basis for this rule of inference is the tautology (P  (P  Q))  Q)
[aside: check tautology with truth table to make sure]
In words: when P and P  Q are True, then Q must be True also. (meaning of
second implication)
6
Propositional logic:
Rules of Inference or Methods of Proof
Example
Modus Ponens
If you study the CS 372 material  You will pass
You study the CS372 material
______________
 you will pass
Nothing “deep”, but again remember the formal reason is that
((P ^ (P  Q))  Q is a tautology.
7
Propositional logic:
Rules of Inference or Method of Proof
Rule of Inference
Tautology (Deduction Theorem)
Name
P
PQ
P  (P  Q)
Addition
PQ
P
(P  Q)  P
Simplification
P
Q
PQ
[(P)  (Q)]  (P  Q)
Conjunction
P
PQ
Q
[(P)  (P Q)]  (P  Q)
Modus Ponens
Q
PQ
 P
[(Q)  (P Q)]  P
Modus Tollens
PQ
QR
 P R
[(PQ)  (Q  R)]  (PR)
Hypothetical Syllogism
(“chaining”)
PQ
P
Q
[(P  Q)  (P)]  Q
Disjunctive syllogism
PQ
P  R
QR
[(P  Q)  (P  R)]  (Q  R)
Resolution
Valid Arguments
An argument is a sequence of propositions. The final proposition is called the
conclusion of the argument while the other proposition are called the
premises or hypotheses of the argument.
An argument is valid whenever the truth of all its premises implies the truth of
its conclusion.
How to show that q logically follows from the hypotheses (p1  p2  …pn)?
Show that
(p1  p2  …pn)  q is a tautology
One can use the rules of inference to show the validity of an argument.
9
Proof Tree
Proofs can also be based on partial orders – we can represent them using a
tree structure:
– Each node in the proof tree is labeled by a wff, corresponding to a wff in
the original set of hypotheses or be inferable from its parents in the tree
using one of the rules of inference;
– The labeled tree is a proof of the label of the root node.
Example:
Given the set of wffs:
P, R, PQ
Give a proof of Q  R
10
Tree Proof
P, P Q, Q, R, Q  R
P
PQ
R
MP
Q
Conj.
QR
What rules of inference
did we use?
11
Length of Proofs
Why bother with inference rules? We could always use a truth table
to check the validity of a conclusion from a set of premises.
But, resulting proof can be much shorter than truth table method.
Consider premises:
p_1, p_1  p_2, p_2  p_3 … p_(n-1)  p_n
To prove conclusion: p_n
Inference rules: n-1 MP steps Truth table:
2n
Key open question: Is there always a short proof for any valid
conclusion? Probably not. The NP vs. co-NP question.
Beyond Propositional Logic:
Predicates and Quantifiers
13
Predicates
Propositional logic assumes the world contains facts that are true or false.
But let’s consider a statement containing a variable:
x > 3 since we don’t know the value of x we cannot say whether the
expression is true or false
x > 3 which corresponds to “x is greater than 3”
Predicate, i.e. a property of x
14
“x is greater than 3” can be represented as P(x), where P denotes
“greater than 3”
In general a statement involving n variables x1, x2, … xn can be
denoted by
P(x1, x2, … xn )
P is called a predicate or the propositional function P at the n-tuple
(x1, x2, … xn ).
15
When all the variables in a predicate are assigned values 
Proposition, with a certain truth value.
Predicate: On(x,y)
Propositions:
ON(A,B) is False (in figure)
ON(B,A) is True
Clear(B) is True
16
Variables and Quantification
How would we say that every block in the world has a property – say “clear”  We would have to say:
 Clear(A); Clear(B); … for all the blocks… (it may be long or worse we may have an infinite number of
blocks…)
What we need is:
Quantifiers:
 Universal quantifier
x P(x)
- P(x) is true for all the values x in the universe of discourse
 Existential quantifier
x P(x)
- there exists an element x in the universe of discourse
such that P(x) is true.
Universal quantification
Everyone at Cornell is smart:
x At(x,Cornell)  Smart(x)
Implicity equivalent to the conjunction of instantiations of P


…
At(Mary,Cornell)  Smart(Mary)
At(Richard,Cornell)  Smart(Richard)
At(John,Cornell)  Smart(John)
A common mistake to avoid
Typically,  is the main connective with 
Common mistake: using  as the main connective with :
x At(x,Cornell)  Smart(x)
means “Everyone is at Cornell and everyone is smart”
Existential quantification
Someone at Cornell is smart:
x (At(x,Cornell)  Smart(x))
x P(x) “ There exists an element x in the universe of discourse such that
P(x) is true”
Equivalent to the disjunction of instantiations of P
(At(John,Cornell)  Smart(John))
 (At(Mary,Cornell)  Smart(Mary))
 (At(Richard,Cornell)  Smart(Richard))
 ...
Another common mistake to avoid
Typically,  is the main connective with
Common mistake: using  as the main connective with :
x At(x,Cornell)  Smart(x)
when is this true?
is true if there is anyone who is not at Cornell!
Quantified formulas
If ω is a wff and x is a variable symbol, then both x ω and x ω are
wffs.
x is the variable quantified over
ω is said to be within the scope of the quantifier
if all the variables in ω are quantified over in ω, we say that we have
a closed wff or closed sentence.
Examples:
x [P(x)  R(x)]
x [P(x)(y [R(x,y)  S(x))]]
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)
– “Everyone in the world loves at least one person”
y x Loves(x,y)
– “There is a person who is loved by everyone in the world” 
Quantifier duality: each can be expressed using the other
x Likes(x,IceCream)
x Likes(x,IceCream)
x Likes(x,Broccoli)
x Likes(x,Broccoli)
Statement
When True
When False
x y P(x,y)
y x P(x,y)
P(x,y) is true for
every pair
There is a pair for
which P(x.y) is
false
x y P(x,y)
For every x there is There is an x such
a y for which P(x,y) that P(x,y) is false
is true
for every y.
x y P(x,y)
There is an x such
that P(x,y) is true
for every y.
For every x there is
a y for which P(x,y)
is false
x  y P(x,y)
y  x P(x,y)
There is a pair x, y
for which P(x,y) is
true
P(x,y) is false for
every pair x,y.
Negation
Negation
Equivalent When is
Statement the
negation
True
When is
False
x P(x)
x P(x)
For every x,
P(x) is false
There is an x
for which P(x)
is true.
 x P(x)
x P(x)
There is an x For every x,
for which P(x) P(x) is true.
is false.
Love Affairs
Loves(x,y) x loves y
Everybody loves Jerry
x Loves (x, Jerry)
Everybody loves somebody
x y Loves (x, y)
There is somebody whom somebody loves
y x Loves (x, y)
Nobody loves everybody
 x y Loves (x, y) ≡ x y Loves (x, y)
There is somebody whom Lydia doesn’t love
y Loves (Lydia, y)
Note: flipping quantifiers when ¬ moves in.
Love Affairs
continued…
There is somebody whom no one loves
y x Loves (x, y)
There is exactly one person whom everybody loves
(uniqueness)
y(x Loves(x,y)  z((w Loves (w ,z) z=y))
There are exactly two people whom Lynn Loves
x y ((xy)  Loves(Lynn,x) Loves(Lynn,y) 
z( Loves (Lynn ,z) (z=x  z=y)))
Everybody loves himself or herself
x Loves(x,x)
There is someone who loves no one besides herself or himself
x y Loves(x,y) (x=y)
(note biconditional )
Let Q(x,y) denote “xy =0”; consider the domain of discourse the real
numbers
What is the truth value of
a) y x Q(x,y)?
b) x y Q(x,y)?
False
True (additive inverse)
The kinship domain:
Brothers are siblings
x,y Brother(x,y)  Sibling(x,y)
One's mother is one's female parent
m,c Mother(c) = m  (Female(m)  Parent(m,c))
“Sibling” is symmetric
x,y Sibling(x,y)  Sibling(y,x)
The set domain:
Sets are empty sets or those made by adjoining something to a set
s Set(s)  (s = {} )  (x,s2 Set(s2)  s = {x|s2})
The empty set has no element adjoined to it
x,s {x|s} = {}
Adjoining an element already in the set has no effect
x,s x  s  s = {x|s}
Only elements have been adjoined to it
x,s x  s  [ y,s2 (s = {y|s2}  (x = y  x  s2))]
Subset
s1,s2 s1  s2  (x x  s1  x  s2)
Equality of sets
s ,s (s = s )  (s  s  s  s )
Rules of Inference for Quantified
Statements
(x) P(x)
P(c)

Universal Instantiation
P(c) for an arbitrary c
(x) P(x)
Universal Generalization
(x) P(x)
Existential Instantiation
 P(c) for some element c
P(c) for some element c
 (x) P(x)
Existential Generalization
Example:
Let CS372(x) denote: x is taking CS372 class
Let CS(x) denote: x has taken a course in CS
Consider the premises x (CS372(x)  CS(x))
CS372(Ron)
We can conclude CS(Ron)
Arguments
Argument (formal):
Step
1 x (CS372(x)  CS(x))
2 CS372(Ron)  CS(Ron)
3 CS372(Ron)
4 CS(Ron)
Reason
premise
Universal Instantiation
Premise
Modus Ponens (2 and 3)
Example
Show that the premises:
1- A student in this class has not read the textbook;
2- Everyone in this class passed the first homework
Imply
Someone who has passed the first homework has not read the textbook
Example
Solution:
Let C(x) x is in this class;
T(x) x has read the textbook;
P(x) x passed the first homework
Premises:
x (Cx  T(x))
x (C(x)  P(x))
Conclusion: we want to show x (P(x)  T(x))
Step
1
2
3
4
5
6
7
8
9
x (Cx T(x))
C(a)  T(a)
C(a)
x (C(x)P(x))
C(a)  P(a)
P(a)
T(a)
P(a)  T(a)
x P(x) T(x)
Reason
premise
Existential Instantiation from 1
Simplification 2
Premise
Universal Instantiation from 4
Modus ponens from 3 and 5
Simplification from 2
Conjunction from 6 and 7
Existential generalization from 8
Resolution in Propositional Logic
Resolution
(for CNF)
Very important inference rule – several other inference rules
can be seen as special cases of resolution.
PQ
P  R
 QR
Soundness of rule (validity of rule):
[(P  Q)  (P  R)]  (Q  R)
Resolution for CNF – applied to a special type of wffs: conjunction of clauses.
Literal – either an atom (e.g., P) or its negation (P).
Clause – disjunction of of literals (e.g., (P  Q  R)).
Note: Sometimes we use the notation of a set for a clause: e.g. {P,Q,R} corresponds
to the clause (PQ R); the empty clause (sometimes written as Nil or {}) is equivalent
to False;
CNF
Conjunctive Normal Form (CNF)
A wff is in CNF format when it is a conjunction of disjunctions of literals.
(P  Q  R) (S  P  T R) (Q  S)
Resolution for CNF – applied to wffs in CNF format.
Resolution
{λ}  Σ1
{ λ}  Σ2
 Σ1  Σ2
Resolvent of the
two clauses
Σi- sets of literals
i =1 ,2
λ – atom;
atom resolved upon
Resolution:
Notes
1 – Rule of Inference: Chaining
RP
P  Q
 RQ
R  P
PQ
 R Q
can be re-written
Rule of Inference Chaining
2 – Rule of Inference: Modus Ponens
P
P  Q
 Q
can be re-written
P
PQ
 Q
Rule of Inference: Modus Ponens
Resolution:
Notes
3 – Unit Resolution
P
P Q
 Q
P
P  Q
 Q
Resolution:
Notes
4 – No duplications in the resolvent set
only one instance of Q
appears in the resolvent,
which is a set!
PQRS
P  Q  W
 QRSW
5 – Resolving one pair at a time
Resolving
on Q

P  Q  R
P  W  Q  R
P  R  R  W
P  Q  R
P  W  Q  R
 P  Q  Q  W
DO NOT Resolve
on Q and R
Resolving
on R
True

P  Q  R
P  W  Q  R
PW
Resolution:
Notes
6 – Same atom with opposite signs
{P}
{P}
 {}
False – any set of wffs containing two contradictory
clauses is unsatisfiable. However, a clause {P, P}
is True.
Soundness of Resolution:
Validity of the Resolution Inference Rule
PQ
P  R
 QR
resolving on P
Validity (Tautology): (P  Q) (P  R)
P
Q
R
(PQ)
(PR)
(PQ)(PR)
(QR)
(P  Q) (P  R)  (Q  R)
0
0
0
0
1
0
0
1
0
0
1
0
1
0
1
1
0
1
0
1
1
1
1
1
1
0
0
1
0
0
0
1
1
1
0
1
0
0
1
1
1
0
1
1
1
1
1
1
0
1
1
1
1
1
1
1
0
0
0
0
1
0
0
1

(Q  R)
;
Conversion to CNF
P  (Q  R)
1.Eliminate , replacing α  β with (α  β)(β  α).
(P  (Q  R))  ((Q R)  P)
2. Eliminate , replacing α  β with α β.
(P  Q  R)  ((Q R)  P)
3. Move  inwards using de Morgan's rules and doublenegation:
(P Q R)  ((Q R)  P)
4. Apply distributivity law ( over ) and flatten:
(P  Q  R)  (Q P)  (R  P)
Converting DNF (Disjunctions of
conjunctions) into CNF
1 – create a table – each row
corresponds to the literals in each
conjunct;
2 - Select a literal in each row and
make a disjunction of these literals;
Example:
(PQ R ) (S R P) (Q S  P)
P
Q
R
S
R
P
Q
S
P
(P  S  Q)  (P  R  Q) (P  P  Q) (P  S  S)
(P  R  S) (P  P  S) (P  P  Q)…
How many clauses?
Resolution:
Wumpus World
P31  P2,2,
P2,2
 P31
P?
P?
Resolution Refutation
Resolution is sound – but resolution is not complete – e.g., (P R) ╞ (P  R) but
we cannot infer (P  R) using resolution 
we cannot use resolution directly to decide all logical entailments.
Resolution is Refutation Complete:
We can show that a particular wff W is entailed from a given KB how?
Proof by contradiction:
Write the negation of what we are trying to prove (W) as a conjunction of clauses;
Add those clauses (W) to the KB (also a set of clauses), obtaining KB’; prove
inconsistency for KB’, i.e.,
Apply resolution to the KB’ until:
•
•
No more resolvents can be added
Empty clause is obtained
To show that (P  R) ╞Res (P  R) do: (1) negate (P  R), i.e.: (P) (R) ; (2) prove that
(P  R)  (P) (R) is inconsistent
!
!
Propositional Logic:
Proof by refutation or contradiction:
Satisfiability is connected to inference via the
following:
KB ╞ α if and only if (KB α) is unsatisfiable
One assumes α and shows that this leads to a
contradiction with the facts in KB
Resolution:
Robot Domain
Example:
BatIsOk
RobotMoves
BatIsOk  BlockLiftable RobotMoves
Show that KB ╞ BlockLiftable
KB
BatIsOk  BlockLiftable  RobotMoves
BlockLiftable
BatIsOk
RobotMoves
BatIsOk  BlockLiftable  RobotMoves
BlockLiftable
KB’
RobotMoves
BatIsOk  RobotMoves
BatIsOk
Nil
BatIsOk
Resolution
Resolution is refutation complete (Completeness of resolution refutation):
If KB ╞ W, the resolution refutation procedure, i.e., applying
resolution on KB’, will produce the empty clause.
Decidability of propositional calculus by resolution refutation:
If KB is a set of finite clauses and if KB ╞ W, then the resolution
refutation procedure will terminate without producing the empty
clause.
Ground Resolution Theorem
– If a set of clauses is not satisfiable, then resolution closure of those
clauses contains the empty clause.
In general, resolution for propositional logic
is exponential !
The resolution closure of a set of clauses W in CNF, RC(W), is the set of all clauses derivable by repeated application
of the resolution rule to clauses in W or their derivatives.
Resolution algorithm
Proof by contradiction, i.e., show KBα unsatisfiable
Any complete search algorithm applying only the resolution rule, can derive any
conclusion entailed by any knowledge base in propositional logic – resolution can
always be used to either confirm or refute a sentence – refutation completeness (Given
A, it’s true we cannot use resolution to derive A OR B; but
we can use resolution to answer the question of whether A OR B is true.)
Resolution example:
Wumpus World
KB = (B1,1  (P1,2 P2,1))  B1,1
α = P1,2
Resolution example:
Wumpus World
KB = (B1,1  (P1,2 P2,1))  B1,1
α = P1,2
KB = (B11  (P1,2 P2,1)) ^ ((P1,2 P2,1)  B11)  B1,1
=(B11  P1,2 P2,1) ^ ((P1,2 P2,1)  B11)  B1,1
=(B11  P1,2 P2,1) ^(( P1,2 ^  P2,1)  B11))  B1,1
=(B11  P1,2 P2,1) ^( P1,2  B11) ^ ( P2,1  B11)  B1,1
Resolution Refutation –
Ordering Search Strategies
Original clauses – 0th level resolvents
– Depth first strategy 
• Produce a 1st level resolvent;
• Resolve the 1st level resolvent with a
0th level resolvent to produce a 2nd
level resolvent, etc.
• With a depth bound, we can use a
backtrack search strategy;
– Breadth first strategy 
• Generate all 1st level resolvents, then
all 2nd level resolvents, etc.
0th level resolvents
BatIsOk
RobotMoves
BatIsOk  BlockLiftable  RobotMoves
BlockLiftable
BatIsOk  BlockLiftable  RobotMoves
BlockLiftable
RobotMoves
BatIsOk  RobotMoves
BatIsOk
BatIsOk
Nil
Depth first strategy
Refinement Resolution Strategies
Set-of-support Resolution Strategy
Definitions:
A clause γ2 is a descendant of a clause γ1 iif:
–
–
Is a resolvent of γ1 with some other clause
Or is a resolvent of a descendant of γ1 with some
other clause;
BatIsOk  BlockLiftable  RobotMoves
BlockLiftable
If γ2 is a descendant of γ1, γ1 is an ancestor of γ2;
Set-of-support – set of clauses that are either clauses
coming from the negation of the theorem to be
proved or descendants of those clauses.
Set-of-support Strategy – it allows only refutations
in which one of the clauses being resolved is in
the set of support.
Set-of-support Strategy is refutation complete.
RobotMoves
BatIsOk  RobotMoves
BatIsOk
BatIsOk
Nil
Set-of-support Strategy
Refinement Strategies
Ancestry-filtered strategy – allows only resolutions in which at least one
member of the clauses being resolved either is a member of the
original set of clauses or is an ancestor of the other clause being
resolved;
The ancestry-filtered strategy is refutation complete.
Refinement Strategies
Linear Input Resolution Strategy – at least one of the clauses being
resolved is a member of the original set of clauses (including the
theorem being proved).
Linear Input Resolution Strategy is not refutation complete.
Example:
(P Q)
(P Q)
(P Q) (P Q) (P  Q) (P  Q)
Q
Q
This set of clauses is inconsistent; but there is
no linear-input
refutation strategy; but there is a resolution
refutation strategy;
(P  Q) (P  Q)
Nil
This is NOT
Linear Input
Resolution Strategy
Horn Clauses
Horn Clauses
Definition:
A Horn clause is a clause that has at most one positive literal.
Examples:
P; P  Q;  P  Q;  P  Q  R;
Types of Horn Clauses:
Fact – single atom – e.g., P;
Rule – implication, whose antecendent is a conjunction
of positive literals and whose consequent consists of a single
positive literal – e.g., PQ  R; Head is R; Tail is (PQ )
Set of negative literals - in implication form, the antecedent is
a conjunction of positive literals and the consequent is empty.
e.g., PQ  ; equivalent to  P  Q.
Inference with propositional Horn clauses can be done in linear time !
Forward chaining
HORN (Expert Systems and Logic Programming)
Horn Form (restricted)
KB = conjunction of Horn clauses
– Horn clause =
• proposition symbol; or
• (conjunction of symbols)  symbol
– E.g., C  (B  A)  (C  D  B)
–
Modus Ponens (for Horn Form): complete for Horn KBs
α1, … ,αn,
α1  …  αn  β
Deciding entailment with Horn clauses
can be done in linear time,
β
in the size of the KB
!
Can be used with forward chaining 
Forward Chaining:
Diagnosis systems
Example: diagnostic system
IF the engine is getting gas and the engine turns over
THEN the problem is spark plugs
IF the engine does not turn over and the lights do not come on
THEN the problem is battery or cables
IF the engine does not turn over and the lights come on
THEN the problem is starter motor
IF there is gas in the fuel tank and there is gas in the
carburator
THEN the engine is getting gas
Forward chaining
(Data driven reasoning)
Idea: fire any rule whose premises are satisfied in the KB,
– add its conclusion to the KB, until query is found
AND-OR graph
Forward chaining algorithm
Forward chaining is sound and complete for Horn KB
Count
P => Q
L and M => P
B and L => M
A and P => L
A and B => L
Agenda
Inferred
1
2
2
2
2
P
L
M
B
A
F
F
F
F
F
A
B
Forward chaining example
Forward chaining example
Forward chaining example
Forward chaining example
Forward chaining example
Forward chaining example
Forward chaining example
Forward chaining example
Backward chaining
Idea: work backwards from the query q:
to prove q by BC,
check if q is known already, or
prove by BC all premises of some rule concluding q
Avoid loops: check if new subgoal is already on the goal stack
Avoid repeated work: check if new subgoal
1. has already been proved true, or
2. has already failed
Backward chaining example
Backward chaining example
Backward chaining example
Backward chaining example
Backward chaining example
Backward chaining example
Backward chaining example
Backward chaining example
Backward chaining example
Backward chaining example
Forward vs. backward chaining
FC is data-driven, automatic, unconscious processing,
– e.g., object recognition, routine decisions
May do lots of work that is irrelevant to the goal
BC is goal-driven, appropriate for problem-solving,
– e.g., Where are my keys? How do I get into a PhD program?
Complexity of BC can be much less than linear in size of KB