Transcript lecture

Chapter 6
Logical Reasoning
Xiu-jun GONG (Ph. D)
School of Computer Science and Technology, Tianjin
University
[email protected]
http://cs.tju.edu.cn/faculties/gongxj/course/ai/
Outline
Intro to logic reasoning
 Preparation for resolution








Stand form clauses (9 steps)
Substitution and unify
Control strategies
The central role of logic in
Resolution reasoning

Logic is the Calculus of
Computer Science
computer science is
comparable to the role of
differential equations in the
natural sciences
In propositional logic
In Predicate logic
In particular interrogative sentence
Summary
Intro to logic




Logic is the study of the principles of valid
demonstration and inference.
Consistency, which means that none of the
theorems of the system contradict one another.
Soundness, which means that the system's
rules of proof will never allow a false inference
from a true premise. If a system is sound and its
axioms are true then its theorems are also
guaranteed to be true.
Completeness, which means that there are no
true sentences in the system that cannot, at least
in principle, be proved in the system.
Classifications of logic
Informal logic is the study of natural
language arguments.
 Formal logic is the study of inference
with purely formal content
 Symbolic logic is the study of symbolic
abstractions that capture the formal
features of logical inference
 Mathematical logic is an extension of
symbolic logic into other areas(model
theory, proof theory, set theory, and
recursion theory)

Symbolic logic

Two languages



Propositional logic
Predicate logic
Components



Syntax
Rules
Semantic
Syntax

Elements




Atoms: {A,B, …, T,F}
Literal: atoms and a  sign in front of them
Connectives: , , , and 
Sentences: Syntax of well-formed formula (wff),





Any atom is a wff.
If w1 and w2 are wffs, so are w1  w2, w1  w2, w1  w2,  w1.
There are no other wffs.
Universal sign: x
Quantifier sign: x
Inference
Reasoning is the cognitive process of
looking for reasons for beliefs,
conclusions, actions or feelings.
 Inference is the act or process of deriving
a conclusion based solely on what one
knows.
 Logic reasoning




Deduction: determining the conclusion
Induction: determining the rule.
Abduction: determining the precondition.
Semantics

Semantics


Interpretation


associating elements of a logical language with elements of
a domain of discourse
the proposition associated with an atom (value)
Propositional Truth Table

Given the values of atoms under some interpretation, use a
truth table to compute a value for any wff under that same
interpretation.
Standard Form Clauses (1)

Clause: a disjunction of literals.
~ abd e

Conjunctive Normal Form: CNF
(a  ~ b  c)  (~ a  b  d  e)  (~ f  b)

Disjunctive Normal Form: DNF

CNFDNF
Standard Form Clauses (2)

Prenex Normal Form: A wff of predicate
logic is in prenex normal form, iff





all its quantifiers are clustered at the left
no quantifier is negated
the scope of each quantifier extends to the end
of the wff
no two quantifiers quantify the same variable
every quantified variable occurs in the matrix
of the wff
Standard Form Clauses (3)

Skolem Standard Form:



A formula is in SSF if it is in conjunctive
prenex normal form with only universal firstorder quantifiers
Removing existential quantifiers from formal
logic statements
Standard Form Clauses:

Clauses in SSF
P(c)
Convert WFF to SFCs (1)
1.
Eliminate implication signs,  >
p  q ~ p  q
2.
Reduce the scopes of ～
double negative law : ~ (~ P)  P
~ ( P  Q)  ~ P ~ Q
De Morgan' s laws 
~ ( P  Q)  ~ P  ~ Q
~ (X ) P( X )  (X ) ~ P( X )
Quantifies conversion law
~ (X ) P( X )  (X ) ~ P( X )
3.
Rename variables
(X)(( Y) ~ p(X, Y)  (Y)(q(X, Y) ~ r(X, Y)))
 (X)(( Y) ~ p(X, Y)  (Z)(q(X, Z) ~ r(X, Z)))
Convert WFF to SFC (2)
4.
Forward quantifiers
(X )(( Y ) ~ p( X , Y )  (Z )( q( X , Z ) ~ r ( X , Z )))
 (X)(Y)(Z)(~ p(X, Y)  (q(X, Z) ~ r(X, Z)))
5.
Skolem transfer

Eliminate existential quantifiers
(X)president(X)  president(c)
(X )(Y )(Z ) p( X )  q(Y )  r (Z )
 (X ) p( X )  q( f ( X ))  r ( g ( X ))
Convert WFF to SFC (3)
6.
Get CNF with Skolem standard form
(X ) ( p( X )  q( f ( X ))  r ( g ( X ))
 (X ) ( p( X )  r ( g ( X )))  (q( f ( X ))  r ( g ( X )))
7.
Eliminate universal quantifiers
 ( p( X )  r ( g ( X )))  (q( f ( X ))  r ( g ( X )))
Convert WFF to SFC (4)
8.
Get clauses
( p( X )  r ( g ( X )))  (q( f ( X ))  r ( g ( X )))
 { p( X )  r ( g ( X )), q( f ( X ))  r ( g ( X ))}
9.
Rename variables again
{ p( X )  r ( g ( X )), q( f ( y ))  r ( g ( y ))}
An example
(X)(( Y)p(X, Y) ~ (Y)(q(X, Y)  r(X, Y)))
 (X)(~ (Y)p(X, Y) ~ (Y)(~ q(X, Y)  r(X, Y)))
 (X)(( Y) ~ p(X, Y)  (Y)(q(X, Y) ~ r(X, Y)))
 (X)(( Y) ~ p(X, Y)  (Z)(q(X, Z) ~ r(X, Z)))
 (X)(Y)(Z)(~ p(X, Y)  (q(X, Z) ~ r(X, Z)))
 (X)
 (X)
(Z)(~ p(X, f (X))  (q(X, Z) ~ r(X, Z)))
(~ p(X, f (X))  (q(X, g(X))  ~ r(X, g(X)))
 (X)((~ p(X, f (X))  q(X, g(X)))  (~ p(X, f (X)) ~ r(X, g(X))))
 (~ p(X, f (X))  q(X, g(X)))  (~ p(X, f (X)) ~ r(X, g(X)))
 {~ p(Y , f (Y )) ~ r (Y , g (Y )), p(Y , f (Y )) ~ r (Y , g (Y ))}
Resolution reasoning of propositional
logic
Resolution is a rule of inference leading
to a refutation theorem-proving technique
for sentences in propositional logic and
first-order logic.
 Procedure



Choose two clauses that have exactly one pair
of literals that are complementary
Produce a new clause by deleting the
complementary literals and combining the
remaining literals
A B
B C
A C
General form of resolution
C1  P  C1'
C2 ~ P  C'2
R (C1 , C2 )  C1'  C'2
(P  C1' )  (~ P  C'2 )  C1'  C'2
Proof: Show that if C1 and C2 are true for explanation I, then R is
true for I.
1. Under I, if P=false, then C1’ =true, so R=C1’VC2’=true
2. Under I, if P=true, then C2’ =true, so R=C1’VC2’=true
Resolution on propositional logic

Convert all the expressions (facts, rules
and the negation of conclusion) into
standard form clauses

Resolve on all the clauses until reaches
contradict (nil)
resolution refutation
Example
Conditions:
P,
Conclusion:
R
P  Q  R,
S  T  Q,
T
(1) P
( 2) ~ P  ~ Q  R
(~ S  ~ T )  Q  (~ S  Q)  (~ T  Q)
(3) ~ S  Q
(4) ~ T  Q
(6)
(5) T
~ P ~ Q
( 6) ~ R
(7) ~ P  ~ Q
(8) ~ Q
(9) ~ T
(10) NIL
(6) (2)
(7) (1)
(8) (4)
(9) (5)
(2)
(1)
(4)
~Q
~T
NIL
(5)
Example cont.
(1) P
( 2) ~ P  ~ Q  R
(3) ~ S  Q
(4) ~ T  Q
(5) T
(6) ~ Q  R
(1)( 2)
(7 ) Q
(4)(5)
(8) R
(6)(7)
Lucky enough
Substitution and Unify

Preparing for predicate logic resolution

Universal quantifications for all variables.
Clause
(1 ,,  n )(1    k )

literal
1   k
If two clauses have matching but
complementary literals, it is possible to
resolve them
f ( y) / x
Substitution

Any substitution can be represented by a
set of ordered pairs
  {t1 / x1 , t2 / x2 ,....tn / xn }
Where xi is a variable
yi ( xi ) may be a variable, constant or function
ti / xi means that term xi is substitute d for every occurrence of
the variable ti throughout the scope of the substituti on.
F is the results of substituti on of  on predicate F
Example
  a x , f (b) y, u z
F1  P( x , y, z)
F2  g ( x , y)
F1  P(a , f (b), u )
F2   g(a , f (b))
Unify

F1 and F2 are predicate formula ,θ is a
substitution. if F1θ=F2θ,then θ is the
Unifier of F1 and F2




P(c,y,b)and P(x,a,b), θ={c/x,a/y}
P(x,y,b)and P(z,u,b) θ={z/x,u/y} other else?
P(f(y),a)and P(x,a) θ={f(y)/x}
Three types of unifier



Constant/variable ——变量实例化
Variable/variable ——变量一致化
Function/variable ——变量函数化
Most General Unifier: MGU
σ is a MGU between F1 and F2 if for any θ
be one of unifiers between F1 and F2, there
exists a λ such that θ=σ·λ
 i.e. F1 =P(x), F2 =P(f(y))




θ1 ={f(a)/x,a/y},θ2 ={f(b)/x,b/y}
θ1 ,θ2 are unifiers , but not MGUs
σ = {f(y)/x}is a MGU, where


θ1=σ· {a/y}, λ= {a/y}
θ2=σ· {b/y}, λ= {b/y}
Algorithms looking for a MGU

Steps



Ex1. F1= P(x,y,z) F2= P(x,f(a),h(b))



Find out the difference sets of variables
between two clauses
Identify the substitutions for each set
Difference set: D1={y,f(a)}, D2={z,h(b)}
MGU= {f(a)/ y, h(b)/z}
Ex2. F1= P(x), F2= P(y)


Difference set: D={x,y}
MGU={x/y} or {y/x}
Resolution Reasoning of Predicate Logic

F1 and F2 are clauses, P1 in F1 and ～ P2 in F2 are
literals such that P1 and P2 have a MGU μ, then



These two clauses have a resolvent ρ.
The resolvent is obtained by applying the substitution μ to
the union of F1 and F2, leaving out the complementary
literals.
Ρ=[(F1-{P1}) ∨(F1-{～ P2}) ] μ
Example

Problem





Marcus is a man
Show that
Caesar is a ruler
Marcus is not
A person trying to assassinate its ruler is not loyal loyal to Caesar
Marcus want to assassinate Caesar
Step1 Convert to logic expression
man (marcus)
 ruler (caesar)
 person(X)∧rule(Y)∧tryassassinate(X,Y)
→～loyalto(X,Y)
 tryassassinate (marcus, caesar)
 man(X) → person(X)

～loyalto(marcus,caesar)
Example cont.
 Step2, build standard form clauses
(1) man(m)
(2) ruler(c)
(3) ～person(X)∨～ruler(Y)∨～trya (X,Y)∨～loyalto(X,Y)
(4) trya (m,c)
(5) ～man (Z) ∨person(Z)
(6) loyalto(m,c)
 Step3, resolution reasoning
(7) ～person(m)∨～ruler(c)∨～trya (m,c) (6) (3) {m/X, c/Y}
(8) ～person(m)∨～ruler(c) (7) (4)
(9) ～person(m)
(8) (2)
(10) ～man (m)
(9) (5) {m/Z}
(11) NIL
(10)(1)
Example cont.
6 
3
m X, c Y
~ person (m) ~ ruler (c) ~ trya(m, c) 4 
~ person (m) ~ ruler (c)
5 
2 
~ person (m)
m Z
1
~ man (m)
NIL
Control Strategy (1)

Problem



How to pick up clauses to resolve?
Quick and completeness
Strategies
1.
2.
3.
Breadth-first resolution: completeness, timeconsuming
Unit resolution: with priority with literals
Input resolution: each resolvent at lease
involves a input clause
Control strategies (2)
4.
Linear resolution: Start from an initiate clause, then
resolve continue linearly.
(1) ~P ∨S
(2) P ∨Q
(3)~P ∨R
(4)~Q ∨R
(5)~R
(6)Q ∨R (2)(3)
(7)R
(6)(4)
(8)NIL
(7)(5)
The point is how to choose the initiate clause
Control strategies (3)
5.
Supported set resolution: for each resolvent, one of
clause must be in “supported set”

The supported set includes negation of the conclusion and
its resolvents
~ R ~ PR
(1) ~P ∨S
(2) P ∨Q
(3)~P ∨R
~P
PQ
Q
~ Q R
(4)~Q ∨R
(5)~R
R
~R
NIL
Control strategies (4)
6.
One occurrence literal deletion
(1) ~P ∨S
(2) P ∨Q
(3)~P ∨R
(4)~Q ∨R
(5)~R
Resolution for Particular Interrogative
Sentence

Answers for who，what，when，where，how
Known as: pompeian(x)->died(x,70)
pompeian(marcus)
Ask: died(marcus,?)
Clause set:
(1) ~pompeian(x) ∨ died(x,70)
(2) pompeian(marcus)
(3) ~died(marcus,t) ∨died(marus,t)
(ever-true expression is added for conclusion)
Example cont.
(1) ~pompeian(x) ∨ died(x,70)
(2) pompeian(marcus)
(3) ~died(marcus,t) ∨died(marus,t)
3
1
marcus
x,79 / t
~ pompeian (marcus )  died(marcus ,79)
2 
died(marcus ,79)
Summary

Preparation for resolution




Stand form clauses (9 steps)
Substitution and unify
Control strategies
Resolution reasoning



In propositional logic
In Predicate logic
In particular interrogative sentence