Theorem Proving by Propositional Logic

2.1.3 Theorem Proving by Propositional Logic:
We present here two techniques for logical theorem proving in propositional logic. These are : (1) Semantic methods , (2) Syntactic methods of theorem proving.
(1) Semantic Method for Theorem Proving:
The following notation will be used to represent a symbolic theorem, stating that conclusion "C" follows from a set of premises p1 ,p2 , ..., pn
p1, p2 , ..., pn ? C
In this technique, we first construct a truth table representing the relationship of p1 through pn with "c". Then we test the validity of the theorem by checking whether both the forward and backward chaining methods, to be presented shortly, hold good. The concept can be best illustrated with an example.
Example 1: Let us redefine p1= the-sky-is-cloudy, p2 = it-will-rain and p3 ? p1? p2 to be three propositions. We now form a truth table of p1, p2 and p3 , and then attempt to check whether forward and backward chaining holds good for the following theorem: p1, p3 ? p2 , We have p3 ? p1 ? p2 ? ?p1 ? p2
p1 p2 p3 (?p1? p2)
0
0
1
1 0
1
0
1 1
1
0
1


Fig.(2.3): Truth Table of p1, p2, p3

Forward chaining: When all the premises are true, check whether the conclusion is true. Under this circumstance, we say that forward chaining holds good.
In this example, when p1 and p3 are true, check if p2 is true. Note that in the last row of the truth table, p1 = 1, p3 = 1 yield p2 = 1. So, forward chaining holds good. Now, we test for backward chaining.
Backward chaining: When all the consequences are false, check whether at least one of the premises is false.
In this example p2=0 in the first and third row. Note that when p2=0, then p1=0, in the first row and p3=0 in the third row. So, backward chaining holds good. As forward and backward chaining both are satisfied together, the theorem: p1, p3 ? p2 also holds good.
Example 2: Show that for example 1, p2, p3 ? p1. It is clear from the truth table 2 that when p1=0, then p2=0 (first row ) and p3 = 1 (first row), backward chaining holds good. But when p2= p3 =1, p1=0 (second row), forward chaining fails. Therefore, the theorem does not hold good.
(2). Syntactic Methods for Theorem Proving:
Before presenting the syntactic methods for theorem proving in propositional logic, we state a few well-known theorems.
Standard theorems in propositional logic:
Assuming p, q and r to be propositions, the list of the standard theorems is:
1. p, q ? p ? q
2. p, p ? q ? q (Modus Ponens)
3. ~p, p ? q ? q
4. ~q, p ? q ? ~p (Modus Tollens)
5. p ? q, p ? r, q ? r ? r
6. p ? q, q ? r ? p ? r (chaining)
7. p, p ? q, q? r ? r (Modus Ponens & chaining)
8. p ? (q ? ~q) ? p
9. p ? (q ? ~q) ? p
10. p ? q ? ~p ? q
11. ~(p ? q) ? p ? ~q
12. p ? q ? (p ? q) ? (q ? p)
13. p ? q ? (p ? q) ? (~p ? ~q)
14. p ? (q ? r) ? (p ? q) ? r
15. p ? q ? ~q ? ~p (contraposition theorem)

The syntactic approach for theorem proving can be done in two ways:
(a) Substitution Method (b) by Wang’s Method.
(a) Method of Substitution
By this method, left-hand side (or right-hand side) of the statement to be proved is chosen and the standard formulas, presented above, are applied selectively to prove the other side of the statement.
Example 3: Prove the contraposition theorem. The contraposition theorem can be stated as follows. When p and q are two propositions, the theorem takes the form of
p?q ? ?q ? ? p
Now , L.H.S = p ? q
? ~p ? q [by (10)]
? q ? ~p
? ~(~q) ? ~p
? ~q ? ~p = R.H.S.
Analogously, starting with the R.H.S, we can easily reach the L.H.S. Hence, the theorem bi-directionally holds good.
Example 4: Prove theorem by method of substitution.
p ? (q ? r) ? (p ? q) ? r
Proof: L.H.S = p?(q?r)
? p ? (~q ? r) [by (10)]
? ~p ? (~q ? r) [by (10)]
? (~p ? ~q) ? r
? ~(p ? q) ? r by De Morgan s law
? (p ? q) ? r = R.H.S [by (10)]
Analogously, the L.H.S. can be equally proved from the R.H.S. Hence, the theorem follows bi-directionally.
(b) Theorem Proving by Using Wang’s Algorithm:
Any theorem of propositional logic is often represented in the following form:
p1, p2 , ... pn ? q1, q2 , ... , qm
where pi and qj represent propositions. The comma in the L.H.S. represents AND operator, while that in the R.H.S. represents OR operator.