Transcript Resources - CSE, IIT Bombay

CS344 : Introduction to Artificial
Intelligence
Pushpak Bhattacharyya
CSE Dept.,
IIT Bombay
Lecture 9,10,11- Logic; Deduction
Theorem
23/1/09 to 30/1/09
Logic and inferencing
Vision
NLP
Search
 Reasoning
 Learning
 Knowledge

Robotics
Expert
Systems
Planning
Obtaining implication of given facts and rules -- Hallmark of
intelligence
Propositions
Stand for facts/assertions
− Declarative statements
− As opposed to interrogative statements (questions) or imperative
statements (request, order)
−
Operators
AND
(

),
OR
(

),
NOT
(~),
IMPLIC
N
(

)
=> and ¬ form a minimal set (can express other operations)
- Prove it.
Tautologies are formulae whose truth value is always T, whatever the
assignment is
Model
In propositional calculus any formula with n propositions has 2n models
(assignments)
- Tautologies evaluate to T in all models.
Examples:
1)
P  P
2)
( P  Q)  (P  Q)
e Morgan with AND
-
Formal Systems
Rule governed
 Strict description of structure and rule application


Constituents


Symbols
Well formed formulae

Inference rules

Assignment of semantics

Notion of proof

Notion of soundness, completeness, consistency,
decidability etc.
Hilbert's formalization of propositional calculus
1. Elements are propositions : Capital letters
2. Operator is only one :

(called implies)
3. Special symbol F (called 'false')
4. Two other symbols : '(' and ')'
5. Well formed formula is constructed according to the grammar
WFF P|F|WFFWFF
6. Inference rule : only one
AB and
Given
A
write B
known as MODUS PONENS
7. Axioms : Starting structures
( A  ( B  A))
A1:
A2:
(( A  ( B  C ))  (( A  B)  ( A  C )))
A3
((( A  F )  F )  A)
This formal system defines the propositional calculus
Notion of proof
1. Sequence of well formed formulae
2. Start with a set of hypotheses
3. The expression to be proved should be the last line in the
sequence
4. Each intermediate expression is either one of the hypotheses
or one of the axioms or the result of modus ponens
5. An expression which is proved only from the axioms and
inference rules is called a THEOREM within the system
Example of proof
From P and P  Q
and Q  R prove R
H1: P
H2: P  Q
H3: Q  R
i) P
H1
ii) P  Q
H2
iii) Q
MP, (i), (ii)
iv) Q  R
H3
v) R
MP, (iii), (iv)
Prove that ( P  P) is a THEOREM
i) P  ( P  P)
A1 : P for A and B
ii) P  (( P  P)  P)
A1: P for A and ( P  P) for B
iii) [( P  (( P  P)  P))  (( P  ( P  P))  ( P  P))]
A2: with P for A,
( P for
P ) B and P for C
iv)( P  ( P  P)  ( P  P))
MP, (ii), (iii)
v) ( P  P )
MP, (i), (iv)
Formalization of propositional logic (review)
Axioms :
A1
( A  ( B  A))
(( A  ( B  C ))  (( A  B)  ( A  C )))
A2
((( A  F )  F )  A)
A3
Inference rule:
Given ( A  B) and A, write B
A Proof is:
A sequence of
i) Hypotheses
ii) Axioms
iii) Results of MP
A Theorem is an
Expression proved from axioms and inference rules
Example: To prove ( P  P)
i) P  ( P  P)
A1 : P for A and B
ii) P  (( P  P)  P)
A1: P for A and ( P  P) for B
iii) [( P  (( P  P)  P))  (( P  ( P  P))  ( P  P))]
A2: with P for A,
( P for
P ) B and P for C
iv)( P  ( P  P)  ( P  P))
MP, (ii), (iii)
v) ( P  P )
MP, (i), (iv)
Shorthand
1. ¬ P
2.
is written as
(( P  F )  Q)
PF
and called 'NOT P'
is written as ( P  Q) and called
'P OR Q’
3.
(( P  (Q  F ))  F ) is
written as
'P AND Q'
Exercise: (Challenge)
- Prove that
A  (( A))
( P  Q)
and called
A very useful theorem (Actually a meta
theorem, called deduction theorem)
Statement
If
A1, A2, A3 ............. An ├ B
then
A1, A2, A3, ...............An-1├
An  B
├ is read as 'derives'
Given
A1
A2
A3
.
.
.
.
An
B
A1
A2
A3
.
.
.
.
An-1
Picture 1
An  B
Picture 2
Use of Deduction Theorem
Prove
A  (( A))
i.e.,
A  (( A  F )  F )
A, A ├FF
A├ ( A  F )  F
├
A  (( A  F )  F )
(M.P)
(D.T)
(D.T)
Very difficult to prove from first principles, i.e., using axioms and
inference rules only
Prove P  ( P  Q )
i.e. P  (( P  F )  Q)
P , P  F , Q  F├ F
P, P ├F
├Q
P├
├
(Q  F )(D.T)
F
(M.P with A3)
(P  F )  Q
P  (( P  F )  Q)
Formalization of propositional logic (review)
Axioms :
A1
( A  ( B  A))
(( A  ( B  C ))  (( A  B)  ( A  C )))
A2
((( A  F )  F )  A)
A3
Inference rule:
Given ( A  B) and A, write B
A Proof is:
A sequence of
i) Hypotheses
ii) Axioms
iii) Results of MP
A Theorem is an
Expression proved from axioms and inference rules
Example: To prove ( P  P)
i) P  ( P  P)
A1 : P for A and B
ii) P  (( P  P)  P)
A1: P for A and ( P  P) for B
iii) [( P  (( P  P)  P))  (( P  ( P  P))  ( P  P))]
A2: with P for A,
( P for
P ) B and P for C
iv)( P  ( P  P)  ( P  P))
MP, (ii), (iii)
v) ( P  P )
MP, (i), (iv)
Shorthand
1. ¬ P
2.
is written as
(( P  F )  Q)
PF
and called 'NOT P'
is written as ( P  Q) and called
'P OR Q’
3.
(( P  (Q  F ))  F ) is
written as
'P AND Q'
Exercise: (Challenge)
- Prove that
A  (( A))
( P  Q)
and called
A very useful theorem (Actually a meta
theorem, called deduction theorem)
Statement
If
A1, A2, A3 ............. An ├ B
then
A1, A2, A3, ...............An-1├
An  B
├ is read as 'derives'
Given
A1
A2
A3
.
.
.
.
An
B
A1
A2
A3
.
.
.
.
An-1
Picture 1
An  B
Picture 2
Use of Deduction Theorem
Prove
A  (( A))
i.e.,
A  (( A  F )  F )
A, A ├FF
A├ ( A  F )  F
├
A  (( A  F )  F )
(M.P)
(D.T)
(D.T)
Very difficult to prove from first principles, i.e., using axioms and
inference rules only
Prove P  ( P  Q )
i.e. P  (( P  F )  Q)
P , P  F , Q  F├ F
P, P ├F
├Q
P├
├
(Q  F )(D.T)
F
(M.P with A3)
(P  F )  Q
P  (( P  F )  Q)
More proofs
1. ( P  Q )  ( P  Q )
2. ( P  Q )  (  Q   P )
3. ( P  Q )  ((Q  P )  Q )
Proof Sketch of the Deduction
Theorem
To show that
If
A1, A2, A3,… An |- B
Then
A1, A2, A3,… An-1 |- An B
Case-1: B is an axiom
One is allowed to write
A1, A2, A3,… An-1 |- B
|- B(AnB)
|- (AnB); mp-rule
Case-2: B is An
AnAn is a theorem (already proved)
One is allowed to write
A1, A2, A3,… An-1 |- (AnAn)
i.e. |- (AnB)
Case-3: B is Ai
where (i <>n)
Since Ai is one of the hypotheses
One is allowed to write
A1, A2, A3,… An-1 |- B
|- B(AnB)
|- (AnB); mp-rule
Case-4: B is result of MP
Suppose
B comes from applying MP on
Ei and Ej
Where, Ei and Ej come before B in
A1, A2, A3,… An |- B
B is result of MP (contd)
If it can be shown that
A1, A2, A3,… An-1 |- An Ei
and
A1, A2, A3,… An-1 |- (An (EiB))
Then by applying MP twice
A1, A2, A3,… An-1 |- An B
B is result of MP (contd)
This involves showing that
If
A1, A2, A3,… An |- Ei
Then
A1, A2, A3,… An-1 |- An Ei
(similarly for AnEj)
B is result of MP (contd)
Adopting a case by case analysis as
before,
We come to shorter and shorter length
proof segments eating into the body of
A1, A2, A3,… An |- B
Which is finite. This process has to
terminate. QED
Important to note





Deduction Theorem is a meta-theorem
(statement about the system)
PP is a theorem (statement
belonging to the system)
The distinction is crucial in AI
Self reference, diagonalization
Foundation of Halting Theorem, Godel
Theorem etc.
Example of ‘of-about’
confusion

“This statement is false”

Truth of falsity cannot be decided