| The tree method for logical decomposition is useful when dealing with
a large number of clauses and variables inside a logical expression.
Each clause can be broken down into smaller clauses. This is can be more useful than truth tables at times.
AND | NOT AND
1) A and B x | 1) !(A and B) x
---------- | -------------
2) A | /\
3) B | / \
| / \
| 2)!A 3)!B
-------------------+------------------
OR | NOT OR
1) A or B x | 1) !(A or B) x
--------- | ------------
/\ | 2) !A
/ \ | 3) !B
/ \ |
2)A 3)B |
-------------------+------------------
IMPLIES | NOT IMPLIES
1) A -> B x | 1) !(A -> B) x
--------- | ------------
/\ | 2) A
/ \ | 3) !B
/ \ |
2)!A 3)A |
4)B |
-------------------+------------------
IFF | NOT IFF
1) A <=> B x | 1) !(A <=> B) x
---------- | -------------
/\ | /\
/ \ | / \
/ \ | / \
2)A 3)!A | 2)!A 3)A
4)B 5)!B | 4)B 5)!B
Complex statements can be broken up into smaller ones.
1) (A or (B or C)) <=> (D and (E -> F)) x
---------------------------------------
/\
/ \
/ \
/ \
/ \
/ \
2) (A or (B or C) 3)!(A or B (or C))
4)(D and (E -> F)) 4)!(D and (E -> F)
After each line is decomposed, an 'x' is placed next to the line to
show that it has already been taken care of. It is often a good idea
to put a comment on the right hand side showing where the statement
came from for checking the work.
When a branch has a logical inconsistency in it (both 'A' and '!A' show up in the same branch), an 'x' is placed under that branch with the
two statement numbers that have the inconsistency. No further work need be done on that branch.
| 
