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.