Understanding Normal Forms in Propositional Logic

 
1
Department of Computer Science,
Faculty of Electrical Engineering and Computer Science,
VSB - Technical University of Ostrava
Propositiponal logic
2
 
To each formula of propositional logic there is just one truth-value function, i.e.,
mapping 
{
p, q, r…
} 
 {0, 1} (the truth-value table).
On the other hand, to each such function there are 
infinitely many formulas,
which are 
mutually equivalent
.
Definition
: 
Formulas A, B are 
equivalent
, notation A 
 B, if A, B have exactly
the same models, i.e., A and B express the same truth-value function. In other
words, 
A entails B, and vice versa
:
A 
 B iff A |= B a B |= A
.
Example: 
p
 
 q 
 
p 
 q 
 
(p 
 
q) 
 (p
 
 q) 
 (p 
 
p) 
 (p
 
 q) 
 (p 
 
p) 
 ...
Note: Do not confuse the equivalence of formulas
 A 
 B (‘
 ‘ is a sign of meta-
language!) with a formula of the form A 
 B.
However, it holds that 
A 
 B
 if and only if the formula 
|= 
A 
 B (is a tautology)
.
Example:
 
 
(p 
 q) 
 [(p 
 q) 
 (q 
 p)]
 
  
iff
 
  
|= [(p 
 q) 
 ((p 
 q) 
 (q 
 p))]
Normal forms of formulas of
propositional logic
α
β
 λ
|
-
3
 
 
  
(p 
 q) 
 
[
(p 
 q) 
 (q 
 p)
] 
 
   
[(
p 
 q) 
 (
q 
 p)]
 
   
[(p 
 q) 
 (
p 
 
q)]
 
 ….
It is useful to determine a 
normal (standardized) form 
of a
formula: to select one (or two) determined forms out of these
infinitely many equivalent forms.
The class of equivalent formulas is then represented by the
chosen formula in the normal form.
In the above example the second and third formulas are in a
normal form.
Normal forms of formulas
α
β
 λ
|
-
4
 
Literal
 is a proposition symbol or its negation:  
  
Ex.: 
p, 
q, r
, ...
Elementary conjunction
 (
EC)
 is a conjunction of literals.
  
Ex.: 
p 
 
q, r 
 
r
, ...
Elementary disjunction
 (
ED)
 is a disjunction of literals.
  
Ex.: 
p 
 
q, r 
 
r
, ...
Complete
 elementary conjunction 
(
CEC)
 of a given set S of elementary propositional symbols is an elementary
conjunction in which each symbol (element of S) occurs just once:
       
Ex.: 
p 
 
q
Complete 
elementary disjunction
 (
CED
) of a given set S of elementary propositional symbols is an elementary
disjunction in which each symbol (element of S) occurs just once:
      
 
 
Ex.: 
p 
 
q
Disjunctive normal form
 (
DNF
) of a formula F is a formula F’ such that F’ is equivalent to F and F’ has the form
of a disjunction of elementary conjunctions.
     
Example: 
 
DNF
(p 
 p): 
 
(p 
 p) 
 (
p 
 
p), p 
 
p
Conjunctive normal form
 (
CNF
) of a formula F is a formula F’ such that F’ is equivalent to F and F’ has the form
of a conjunction of elementary disjunctions.
  
CNF
(p 
 p)
: 
(
p 
 p) 
 (
p 
 p
)
Complete 
disjunctive normal form
 (
CDNF
) of a formula F is a formula F’ equivalent to F such that F’ has the
form of a disjunction of 
complete
 elementary conjunctions.
 
UDNF
(p 
 q)
: 
(p 
 q) 
 (
p 
 
q)
Complete
 conjunctive normal form
 (
CCNF
) of a formula F is a formula F’ equivalent to F such that F’ has the
form of a conjunction of 
complete
 elementary disjunctions.
 
UKNF
(p 
 q)
: 
(
p 
 q) 
 (
q 
 p)
CDNF and CCNF are called 
canonic (or standard) forms 
of a formula
.
Normal forms (of PL formulas):
definition
α
β
 λ
|
-
5
 
How to find canonic forms (i.e., CDNF, CCNF) of a formula
?
C
DNF: disjunc
tion
 = 1, 
if at least one CEC 
= 1, 
i.e., 
 
all the
literals in this C
E
C
 = 1.
CC
NF: 
conjunction
 = 0, 
if at least one C
ED = 0, 
i.e., 
 
all the
literals in this C
ED = 0.
Therefore
: 
C
DNF (
CC
NF) 
can be constructed from the
truth-table in such a way, that we take into account only
rows with the value 
1 (0) a
nd ensure “the 
 
correct value
of literals”
 – 1 (0).
Normal forms of PL formulas
α
β
 λ
|
-
6
Find the C
DNF, 
CC
NF
of the formula
: 
 
 
(p
q)
C
DNF: 
p

q
CC
NF:
(
p

q)
(
p

q)
(
p
q
)
C
DNF, 
CC
NF - 
the truth-table method
α
β
 λ
|
-
7
 
 

p 
 q
 
 

p 
 q
 
 (p 
 
q)
 CCNF 
[p 
 (q 
 
q
] 
 [
q 
 (p 
 
p
] 
 
 
 
p 
 q
 
 
p 
 
q
 
 

p 
 
q
 CDNF
Note
: In the second line we make use of the fact that a
disjunction of any formula A with a contradiction F is
equivalent to A: A 
 F 
 A
 
 
In the third line we make use of distributive laws
Statement
: Each
 formula which is not a contradiction has a
CDNF, and
 
 
each formula which is not a tautology has a CCNF
C
DNF, 
CC
NF - 
by equivalent
transforming method:
α
β
 λ
|
-
8
 
Example
An alchemist is imprisoned. He received 5 messages with the following content:
p:
  
You will succeed in converting lead to gold.
q: 
 
On April 1
st
 your brother-in-law will become an attorney.
r: 
 
After April 1
st
 you may expect pleading.
 
 
1
st
 message says: 
 
p 
 q 
 r
 
 
2
nd
 message says: 
 
p 
 q 
 
r
 
 
3
rd
 
message says:
 
 
p 
 
q 
 r
 
 
4
th
 message says: 
 
p 
 
q 
 
r
 
 
5
th
 message: At least one of the previous messages is true.
Question
: What did the poor alchemist learn?
Solution
: 
(p 
 q 
 r) 
 (p 
 q 
 
r) 
 (
p 
 
q 
 r) 
 (
p 
 
q 
 
r)
.
Hence we need to find a formula F which has the above CDNF.
By means of distribute laws we obtain:
(p 
 q 
 r) 
 (p 
 q 
 
r) 
 (
p 
 
q 
 r) 
 (
p 
 
q 
 
r) 
(p 
 q) 
 (r 
 
r) 
 (
p 
 
q) 
 (r 
 
r) 
 (p 
 q) 
 (
p 
 
q) 
 
(p 
 q)
Answer
: You will succeed in converting lead to gold if and only if on April 1
st
 your brother-in-
law becomes an attorney.
Reverse task
given a
 
C
DNF, 
CC
NF
,
find a simpler original formula
α
β
 λ
|
-
Question
how many binary truth-value functions
(
hence how many binary connectives
)
 are there
?
α
β
 λ
|
-
10
 
According to the Statement on normal forms (see slide 7) the
following connectives suffice
: 
, 
, 
(funkcion
ally complete system
)
The following systems of truth-functional connectives are
functionally complete
:
1.
 
{
, 
, 
}
,
2.
 
{
, 
}
 o
r
 
{
, 
}
,
3.
 
{
, 
}
,
4.
{
}
 o
r
 
{
}
.
Hence in order to express any truth-value function (and thus any PL
formula) just one connective suffices
!
Either
 
Scheffer
’s
 NAND 
 
o
r
 
Pierce
’s
 NOR 
Which is the minimal number of
truth-functional connectives
?
α
β
 λ
|
-
11
 
The system 
{
, 
, 
} 
is sufficient according to the Statement on
normal forms
Transition to the system
 {
, 
} o
r
 {
, 
}:
A 
 B 
 
(
A 
 
B),
A 
 B 
 
(
A 
 
B)
Transition to the system
 {
, 
}:
A 
 B 
 
A 
 B,
A 
 B 
 
(A 
 
B)
Transition to the system
 {
} o
r
 {
}:
 
A 
 A
A, A
B 
 (A
B)
(A
B),
  
(
 
is
 NAND
)
,
 
A 
 A
A, A
B 
 (A
B)
(A
B),
  (
 is NOR).
Proof on the minimum of connectives
α
β
 λ
|
-
12
 
Looking at a tableau, you can easily see why
a 
tautolog
y does not have a complete conjunctive normal form
(
CC
NF) a
nd why
a contradiction does not have a complete disjunctive normal form
(
C
DNF):
If a formula is a tautoloy, then all the branches of a conjunctive tableau
are closed, i.e., in each 
ED
 there is a couple of opposite literals
 
p
, 
p
,
which means 
p
 
 
p
. but then the elementary disjunction is 
not
complete
.
Hence the CCNF of the formula does not exist
.
Similarly for C
DNF.
Complete normal forms
α
β
 λ
|
-
13
T1
 
p 
 
p
T2 
 
(p 
 q) 
 (p 
 
q) 
 (
p 
 q) 
 (
p 
 
q)
T3
 
(p 
 q 
 r) 
 (p 
 q 
 
r) 
 (p 
 
q 
 r) 
  
(p 
 
q 
 
r) 
 
(
p 
 q 
 r) 
 (
p 
 q 
 
r) 
 
  
(
p 
 
q 
 r) 
 (
p 
 
q 
 
r)
For each valuation 
v 
there has to be at least one C
E
C
true
.
CDNF of tautology with one (T1),
two (T2), three (T3) variables
α
β
 λ
|
-
14
 
If a formula is not a tautology, at least one of these
CECs has to be missing in the respective C
DNF.
Therefore, if we construe a 
C
DNF 
from a truth table
,
we take into account only those rows, where the
function has the value 
1 
(
value False – 0 does not
matter, because 
A 
 F 
 A) a
nd construe CEC in
such a way that the CEC is true
.
Similarly for 
CC
NF – 
take into account 
0
-s
.
α
β
 λ
|
-
 
From a practical point of view a semantic tableau is not
favourable
If you want to prove that
P
1
,...,
P
n
 
|= 
Z
, it is equivalent to proving
tautology 
|=
 (
P
1
 ... 
 
P
n
)
 
 
Z
,
i.e., 
P
1
 ... 
 
P
n
 
 
Z
 
is a contradiction
.
But, to prove it by the tableau method, you need the
disjun
ctive
 
norm
al
 form.
Which means that you have to transform the formula that is
(almost) in the conjunctive form into the disjunctive form,
which yields a lot of applications of the distributive law.
Using a tableau often yields a lot distributive steps
It is easier to directly prove the contradiction, i.e., that the
formula 
P
1
 ... 
 
P
n
 
 
Z
 is 
not satisfiable
.
Resolution method in the propositional logic
α
β
 λ
|
-
16
 
Let 
l 
be a literal
. 
From 
(A 
 
l
) 
 (B 
 
l
) 
infer
 (A 
 B). 
Notation
:
      
 
(A 
 
l
) 
 (B 
 
l
)
      
 
–––––––––––––––
             
 
      (A 
 B)
  
resolvent
This rule does not lead to an equivalent formula. But it preserves 
satisfiability
.
Proof
: 
Let formula 
(A 
 
l
) 
 (B 
 
l
)
 
be non-contradictory. hence there is a
valuation 
v
 
in which it is true.
But then in this 
v 
both the disjuncts 
(
so called
 
c
laus
es
)
 are true
:
   
(A 
 
l
) a
nd
 (B 
 
l
).
Let 
v
(
l
) = 0
. 
Then
 
w
(A) = 1
 a
nd
 
w
(A 
 B) = 1
.
Let 
v
(
l
) = 1
. 
Then
 
w
(
l
) = 0
 a
nd
 
w
(B) = 1
, a
 thus 
w
(A 
 B) = 1
.
 
In both cases the 
formul
a
 
A 
 B
 
is true in the model 
v
 
of the opriginal
formula, hence it is not a contradiction
.
Resolution rule in the propositional logic
α
β
 λ
|
-
17
 
 
If you realise that the above proof is valid for any valuation 
v,
then you see that the rule is
 
truth preserving
:
    
(A 
 
l
) 
 (B 
 
l
) |= (A 
 B)
.
Thus you obtained also a method of finding 
logical
consequences of a formula
.
Moreover
:
(A 
 
l
) 
 (B 
 
l
) 
 (A 
 
l
) 
 (B 
 
l
) 
 (A 
 B)
Proof by resolution in PL
α
β
 λ
|
-
18
 
The conjunctive normal form is called 
clausal form
. 
Particular
conjuncts 
(
i.e., 
element
ary disjunctions
) 
are called 
clauses
.
Example
: 
Transition of a formula into the clausal form
:
[
(
(p 
 q) 
 (r 
 
q) 
 
r)
 
 
p]
 
(
(p 
 q) 
 (r 
 
q) 
 
r) 
 p 
 
 
 
(
p 
 q) 
 (r 
 
q) 
 
r 
 p
The formula consists of four clauses
.
The proof of contradiction
:
(
p 
 
q) 
 
(r 
 
q) 
 
(
p 
 r)
 
 
r 
 
p
 
 
p
Clausular form
α
β
 λ
|
-
19
 
R(F) – 
c
onjun
ctive extension 
of a formula F by all its resolvents
R
0
(F) = F, R
i
(F) = R(R
i-1
(F)) – rezolu
tion closure of
 F.
It holds that
 
  
R
i
(F) 
 F
Proof:
 
A 
is a contradiction
 (
not satisfiable
): 
there is an 
n 
such that
 
R
n
(A) 
contains
the empty clause
:
Proof:
 
A 
is a tautology
: 
A 
is a contradiction
Proof: 
a set of formulas {
A
1
,…,A
n
}
 
is not satisfiable.
 
We prove that the formula 
A
1
... 
 
A
n 
is a contradiction
Infer logical consequences of {
A
1
,…,A
n
}: infer all the resolvents
Proof of validity:
 A
1
,…,A
n
 |= Z
Direct
: 
by step-by-step inferring resolvents from 
A
1
,…,A
n
 you obtain 
Z
Indirect
: 
prove that 
A
1
 
...
 
A
n 
 Z 
is a tautology, i.e.,
A
1
 
...
 A
n 
 
Z 
is a contradiction, i.e., the set {
A
1
,
...
,
 A
n
,
,
Z
} is not satisfiable
Proof by resolution
α
β
 λ
|
-
20
 
Particular clauses are numbered. gradually infer resolvents (that
logically follow from the clauses). When performing an indirect
proof, you have to infer
p 
 
p
, the empty clause
Prove that the following formula is a contradiction
:
(
q
 
 p) 
 (p 
 r) 
 (q 
 
r) 
 
p
1.
q 
 p
2.
p 
 r

q 
 
r

p
5.
p 
 
r
  
rezolu
tion:
 1, 3
6.
p
   
rezolu
tion:
 2, 5
7.
 
 
 
 
 
4, 6
Question
: 
What follows from the formula
 
   
(
q
 
 p) 
 (p 
 r) 
 (q 
 
r) ?
Answer:
 
 
the formula
 
p
Examples
α
β
 λ
|
-
21
 
Direct proof
:
p 
 q 
 r, 
s 
 
q, t 
 
r |= p 
 (s 
 t)

p 
 
q 
 r
2.
s 
 
q
3.
t 
 
r

p 
 
s 
 r
  
rezolu
tion
 1, 2

p 
 
s 
 t
  
rezolu
tion
 3, 4

p 
 
s 
 t 
 
p 
 (s 
 t) 
 
QED
Examples
α
β
 λ
|
-
22
 
Indirect proof
:
p 
 q 
 r, 
s 
 
q, t 
 
r |= p 
 (s 
 t)
1.
 
 
p 
 
q 
 r
2.
 
 
s 
 
q
3.
 
 
t 
 
r
4.
 
 
p 
 
s 
 r
  
rezolu
tion
 1, 2
5.
 
 
p 
 
s 
 t
  
rezolu
tion
 3, 4
6.
 
 
p  
   
neg
a
-
7.
 
 
s 
   
ted
8.
 
 
t 
   
conclusion
9.
 
 
p 
 
s 
 t
, p, 
s
, 
t
 
|= 
s 
 t
, 
s
, 
t
 |= t, 
t
 |=
Examples
α
β
 λ
|
-
Slide Note
Embed
Share

Explore the concept of normal forms in propositional logic, where each formula has a unique truth-value function. Learn about equivalence of formulas, determining normal forms, and canonic forms like Disjunctive Normal Form (DNF) and Conjunctive Normal Form (CNF). Discover how to find canonic forms and the significance of Complete Disjunctive Normal Form (CDNF) and Complete Conjunctive Normal Form (CCNF).


Uploaded on Sep 08, 2024 | 1 Views


Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

E N D

Presentation Transcript


  1. Department of Computer Science, Faculty of Electrical Engineering and Computer Science, VSB - Technical University of Ostrava Propositiponal logic 1

  2. Normal forms of formulas of propositional logic To each formula of propositional logic there is just one truth-value function, i.e., mapping {p, q, r } {0, 1} (the truth-value table). On the other hand, to each such function there are infinitely many formulas, which are mutually equivalent. Definition: Formulas A, B are equivalent, notation A B, if A, B have exactly the same models, i.e., A and B express the same truth-value function. In other words, A entails B, and vice versa: A B iff A |= B a B |= A. Example: p q p q (p q) (p q) (p p) (p q) (p p) Note: Do not confuse the equivalence of formulas A B ( is a sign of meta- language!) with a formula of the form A B. However, it holds that A B if and only if the formula |= A B (is a tautology). Example: (p q) [(p q) (q p)] |= [(p q) ((p q) (q p))] ... iff 2

  3. Normal forms of formulas (p q) [(p q) (q p)] [( p q) ( q p)] [(p q) ( p q)] . It is useful to determine a normal (standardized) form of a formula: to select one (or two) determined forms out of these infinitely many equivalent forms. The class of equivalent formulas is then represented by the chosen formula in the normal form. In the above example the second and third formulas are in a normal form. 3

  4. Normal forms (of PL formulas): definition Ex.: p, q, r, ... Literal is a proposition symbol or its negation: Ex.: p q, r r, ... Ex.: p q, r r, ... Elementary conjunction (EC) is a conjunction of literals. Elementary disjunction (ED) is a disjunction of literals. Complete elementary conjunction (CEC) of a given set S of elementary propositional symbols is an elementary conjunction in which each symbol (element of S) occurs just once: Ex.: p q Complete elementary disjunction (CED) of a given set S of elementary propositional symbols is an elementary disjunction in which each symbol (element of S) occurs just once: Ex.: p q Disjunctive normal form (DNF) of a formula F is a formula F such that F is equivalent to F and F has the form of a disjunction of elementary conjunctions. DNF(p p): (p p) ( p p), p p Example: Conjunctive normal form (CNF) of a formula F is a formula F such that F is equivalent to F and F has the form of a conjunction of elementary disjunctions. CNF(p p): ( p p) ( p p) Complete disjunctive normal form (CDNF) of a formula F is a formula F equivalent to F such that F has the form of a disjunction of complete elementary conjunctions. UDNF(p q): (p q) ( p q) Complete conjunctive normal form (CCNF) of a formula F is a formula F equivalent to F such that F has the form of a conjunction of complete elementary disjunctions. UKNF(p q): ( p q) ( q p) CDNF and CCNF are called canonic (or standard) forms of a formula. 4

  5. Normal forms of PL formulas How to find canonic forms (i.e., CDNF, CCNF) of a formula? CDNF: disjunction = 1, if at least one CEC = 1, i.e., all the literals in this CEC = 1. CCNF: conjunction = 0, if at least one CED = 0, i.e., all the literals in this CED = 0. Therefore: CDNF (CCNF) can be constructed from the truth-table in such a way, that we take into account only rows with the value 1 (0) and ensure the correct value of literals 1 (0). 5

  6. CDNF, CCNF - the truth-table method p q (p q) UEK UED Find the CDNF, CCNF of the formula: (p q) p q 1 1 0 p q 1 0 1 CDNF: p CCNF: ( p q) (p q p q 0 1 0 p q 0 0 0 q) (p q) 6

  7. CDNF, CCNF - by equivalent transforming method: ( (p q) ) [p (q q) )] [ q (p p) )] ( (p q) ) ( (p q) ) ( Note: In the second line we make use of the fact that a disjunction of any formula A with a contradiction F is equivalent to A: A F A In the third line we make use of distributive laws Statement: Each formula which is not a contradiction has a CDNF, and each formula which is not a tautology has a CCNF ( ( p q) ) (p q) CCNF ( p q) ) CDNF 7

  8. Reverse task: given a CDNF, CCNF, find a simpler original formula Example An alchemist is imprisoned. He received 5 messages with the following content: p: You will succeed in converting lead to gold. q: On April 1styour brother-in-law will become an attorney. r: After April 1styou may expect pleading. 1stmessage says: p q r 2ndmessage says: p q r 3rdmessage says: p q r 4thmessage says: p q r 5thmessage: At least one of the previous messages is true. Question: What did the poor alchemist learn? Solution: (p q r) (p q r) ( p q r) ( p q r). Hence we need to find a formula F which has the above CDNF. By means of distribute laws we obtain: (p q r) (p q r) ( p q r) ( p q r) (p q) (r r) ( p q) (r r) (p q) ( p q) Answer: You will succeed in converting lead to gold if and only if on April 1styour brother-in- law becomes an attorney. (p q) 8

  9. Question: how many binary truth-value functions (hence how many binary connectives) are there? X Y 0 1 2 3 4 5 6 7 8 9 1 1 1 1 2 1 3 1 4 1 5 0 1 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 1 0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 1 0 0 0 0 1 1 1 1 0 0 0 0 1 1 1 1 0 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1

  10. Which is the minimal number of truth-functional connectives? According to the Statement on normal forms (see slide 7) the following connectives suffice: , , (funkcionally complete system) The following systems of truth-functional connectives are functionally complete: 1. { , , }, 2. { , } or { , }, 3. { , }, 4. { } or { }. Hence in order to express any truth-value function (and thus any PL formula) just one connective suffices! Either Scheffer s NAND or Pierce s NOR 10

  11. Proof on the minimum of connectives The system { , , } is sufficient according to the Statement on normal forms Transition to the system { , } or { , }: A B ( A B), A B ( A B) Transition to the system { , }: A B A B, A B (A B) Transition to the system { } or { }: A A A, A B (A B) (A B), ( is NAND), A A A, A B (A B) (A B), ( is NOR). 11

  12. Complete normal forms Looking at a tableau, you can easily see why a tautology does not have a complete conjunctive normal form (CCNF) and why a contradiction does not have a complete disjunctive normal form (CDNF): If a formula is a tautoloy, then all the branches of a conjunctive tableau are closed, i.e., in each ED there is a couple of opposite literals p, p, which means p p. but then the elementary disjunction is not complete. Hence the CCNF of the formula does not exist. Similarly for CDNF. 12

  13. CDNF of tautology with one (T1), two (T2), three (T3) variables p p T1 (p q) (p q) ( p q) ( p q) T2 (p q r) (p q r) (p q r) (p q r) ( p q r) ( p q r) ( p q r) ( p q r) T3 For each valuation v there has to be at least one CEC true. 13

  14. If a formula is not a tautology, at least one of these CECs has to be missing in the respective CDNF. Therefore, if we construe a CDNF from a truth table, we take into account only those rows, where the function has the value 1 (value False 0 does not matter, because A F A) and construe CEC in such a way that the CEC is true. Similarly for CCNF take into account 0-s. 14

  15. Resolution method in the propositional logic From a practical point of view a semantic tableau is not favourable If you want to prove that P1,...,Pn |= Z, it is equivalent to proving tautology |= (P1 ... Pn) Z, i.e., P1 ... Pn Z is a contradiction. But, to prove it by the tableau method, you need the disjunctive normal form. Which means that you have to transform the formula that is (almost) in the conjunctive form into the disjunctive form, which yields a lot of applications of the distributive law. Using a tableau often yields a lot distributive steps It is easier to directly prove the contradiction, i.e., that the formula P1 ... Pn Z is not satisfiable.

  16. Resolution rule in the propositional logic Let l be a literal. From (A l) (B l) infer (A B). Notation: (A l) (B l) (A B) This rule does not lead to an equivalent formula. But it preserves satisfiability. Proof: Let formula (A l) (B l) be non-contradictory. hence there is a valuation v in which it is true. But then in this v both the disjuncts (so called clauses) are true: (A l) and (B l). Let v(l) = 0. Then w(A) = 1 and w(A B) = 1. Let v(l) = 1. Then w( l) = 0 and w(B) = 1, a thus w(A B) = 1. In both cases the formula A Bis true in the model vof the opriginal formula, hence it is not a contradiction. resolvent 16

  17. Proof by resolution in PL If you realise that the above proof is valid for any valuation v, then you see that the rule is truth preserving: (A l) (B l) |= (A B). Thus you obtained also a method of finding logical consequences of a formula. Moreover: (A l) (B l) (A l) (B l) (A B) 17

  18. Clausular form The conjunctive normal form is called clausal form. Particular conjuncts (i.e., elementary disjunctions) are called clauses. Example: Transition of a formula into the clausal form: [((p q) (r q) r) p] ((p q) (r q) r) p ( p q) (r q) r p The formula consists of four clauses. The proof of contradiction: ( p q) (r q) ( p r) r p p 18

  19. Proof by resolution R(F) conjunctive extension of a formula F by all its resolvents R0(F) = F, Ri(F) = R(Ri-1(F)) rezolution closure of F. It holds that Ri(F) F Proof: A is a contradiction (not satisfiable): there is an n such that Rn(A) contains the empty clause: Proof: A is a tautology: A is a contradiction Proof: a set of formulas {A1, ,An} is not satisfiable. We prove that the formula A1 ... An is a contradiction Infer logical consequences of {A1, ,An}: infer all the resolvents Proof of validity: A1, ,An|= Z Direct: by step-by-step inferring resolvents from A1, ,Anyou obtain Z Indirect: prove that A1 ... An Z is a tautology, i.e., A1 ... An Z is a contradiction, i.e., the set {A1,..., An,, Z} is not satisfiable 19

  20. Examples Particular clauses are numbered. gradually infer resolvents (that logically follow from the clauses). When performing an indirect proof, you have to infer p p, the empty clause Prove that the following formula is a contradiction: ( q p) (p r) (q r) p q p p r q r p p r rezolution: 1, 3 p rezolution: 2, 5 4, 6 Question: What follows from the formula ( q p) (p r) (q r) ? Answer: the formula p 1. 2. 3. 4. 5. 6. 7. 20

  21. Examples Direct proof: p q r, s q, t r |= p (s t) p q r s q t r p s r p s t p s t p (s t) 1. 2. 3. 4. 5. 6. rezolution 1, 2 rezolution 3, 4 QED 21

  22. Examples Indirect proof: p q r, s q, t r |= p (s t) 1. p q r 2. s q 3. t r 4. p s r 5. p s t 6. p 7. s 8. t 9. p s t, p, s, t |= s t, s, t |= t, t |= rezolution 1, 2 rezolution 3, 4 nega- ted conclusion 22

More Related Content

giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#