Rule CP : If we can derive S from R and a set of premises, then we an derive
R
S
→ from the set of premises alone. (Deduction Theorem).
Rules of Infer ence
Implications:
I 1
P Q P
P Q Q
∧ ⇒
∧ ⇒



(Simplification)
I 2
I 3
P
P Q
Q P Q
⇒ ∨
⇒ ∨



(addition)
I 4
I 5
¬ ⇒ →
P
P Q
I 6
Q P Q
⇒ →
I 7
¬ →
⇒
(
)
P Q
P
I 8
¬ →
= ¬
(
)
P Q
Q
I 9
P Q P Q
, ⇒ ∧
I 10
¬
∨ ⇒
P P Q Q
,
(disjunctive syllogism)
I 11
P P Q Q
, → ⇒
(Modus Ponens)
I 12
¬
→ ⇒ ¬
Q P Q
P
,
(Modus Tollens)
I 13
P Q Q R
P
R
→
→ ⇒ →
,
(Hypothetical Syllogism)
I 14
P Q P
R Q R
R
∨
→
→ ⇒
,
,
(dilemma)
Equivalences
E 1
¬ ¬ ⇔
P
P (double Negation)
E 2
P Q Q P
P Q Q P
∧ ⇔ ∧
∨ ⇔ ∨



(Commutative laws)
E 3
E 4
(
)
(
)
(
)
(
)
P Q R
P Q R
P Q R
P Q R
∧ ∧ ⇔ ∧ ∧
∨ ∨ ⇔ ∨ ∨



(Associative laws)
E 5
E 6
P Q R
P Q
P R
P Q R
P Q
P R
∨ ∧
⇔ ∨ ∧ ∨
∧ ∧
⇔ ∧ ∨ ∧



(
)
(
) (
)
(
)
(
) (
)
(Distributive law)
E 7
E 8
¬ ∧
⇔ ¬ ∨ ¬
¬ ∨
⇔ ¬ ∧ ¬



(
)
(
)
P Q
P
Q
P Q
P
Q
(De Morgan' s laws)
E 9
E 10 P P
P
∨ ⇔
E 11 P P
P
∧ ⇔
E 12 R P
P
R
∨ ∧ ¬
⇔
(
)
E 13 R P
P
R
∧ ∨ ¬
⇔
(
)
E 14 R P
P
T
∨ ∨ ¬
⇔
(
)
266
Theory of Automata, Formal Languages and Computation