display | more...
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.

Log in or register to write something here or to contact authors.