DHARM128 MATHEMATICAL FOUNDATION OF COMPUTER SCIENCEThus we have,
/∴ ((A → B) ∧ (B → C)) → (A → C)- ((A → B) ∧ (B → C)) /∴ (A → C) CP
- A/∴ C CP
Assume that the negation of formula is true and apply method of contradiction.
Therefore,- ~ C IP
- A → B 1, Simp
- B 4 & 2, MP
- (B → C) ∧ (A → B) 1, Comm
- (B → C) 6, Simp
- C 7 & 5, MP
- C ∧ ~ C 8 & 3 Conj
Since we obtain a contradiction therefore our assumption must be wrong. Hence, for-
mula must be tautology.
So far our discussion to prove the validity of an argument using natural deduction method
we have complete our study with,
· 9-Inference Rules
· 10-Replacement Rules
· 1-Conditional Proof Method
· 1-Indirect Proof Method
This set of rules is called ‘Complete’. For any valid argument the complete must be
follow. Consequently, complete must be the basis for the valid argument.
5.6.3 Analytical Tableaux Method (ATM)..................................................................
In section 5.6.2 we discussed the solution to the problem for validity is provided by the truth
table method. The method of natural deduction just discussed determines whether argument
is valid in finite number of steps. On the other hand, if the argument is invalid, then it is very
difficult to decide, after a finite number of steps. Also, Deduction a lot depends upon the practice,
familiarity and ingenuity of the person to make the right decision at each step. To overcome
these problems we shall now describe another method namely analytical tableaux method
which is based on the formation tree of the formula, that do allow one to determine after a
sequence of steps, whether an argument is valid or invalid.
Analytical tableaux method is based on the formation tree of the formula. There are two
categories of the formulas. One category of formula is called α-formula and other category is
β-formula. Fig 5.26 shows the list of α-formulas, where α 1 or α 1 and α 2 are its extended for-
mula/s; similarly other column shows the ß-formulas and β 1 or β 2 are its extended formulas.