Wangs algorithm Begin

Step I: Starting condition: Represent all sentences, involving only A, V and —I operators.

Step II: Recursive procedure: Repeat steps (a), (b) or (c) whichever is appropriate until the stopping condition, presented in step III, occurs.

a) Negation Removal: In case negated term is present at any side (separated by comma) bring it to the other side of implication symbol without its negation symbol.

e.g., p, q, - r ^ s |= p, q ^ r, s b) AND, OR Removal: If the L.H.S. contains A operator, replace it by a comma. On the other hand if R.H.S. contains V operator, also replace it by a comma.

1= p, r, s ^ s, t c) Theorem splitting: If the L.H.S. contains OR operator, then split the theorem into two sub-theorems by replacing the OR operator. Alternatively, if the R.H.S. contains AND operator, then also split the theorem into two sub-theorems.

1= p ^ s, t & r ^ s, t : Sub-theorems e.g., p, r ^ s A t

Step III: Stopping Condition: Stop theorem proving process if either of (a) or (b), listed below, occurs.

a) If both L.H.S. and R.H.S. contain common atomic terms, then stop.

b) If L.H.S. and R.H.S. have been represented as a collection of atomic terms, separated by commas only and there exist no common terms on both sides, then stop.

End.

In case all the sub-theorems are stopped, satisfying condition III (a), then the theorem holds good. We would construct a tree structure to prove theorems using Wang's algorithm. The tree structure is necessary to break each theorem into sub-theorems.

Example 5. 5: Prove the chaining rule with Modus Ponens using Wang's algorithm.

Proof: The chaining rule with Modus Ponens can be described as p, p^ q, q ^ r ^ r where p, q and r are propositions (atomic).

We now construct the tree. A node in the tree denotes one propositional expression. An arc in the tree denotes the step of Wang's algorithm, which is applied to produce the next step. The bold symbols in both the left- and right-hand side of the implication symbol describe the termination of the sub-tree by step III (a).

Fig. 5.2: Tree used to prove a propositional theorem by Wang's algorithm.

Since all the terminals of the tree have been stopped by using III (a), the theorem holds good. □

+1 0