| A form of proof in propositional logic that determines whether a proposition follows from other propositions, by working through the truth tables for the premisses, and checking whether the consequent is true whenever the premisses are. If so, the consequent is proved. The method is guaranteed to be correct but is impossibly cumbersome beyond small examples because the size of the calculation is exponential on the number of premisses.
Contrast syntactic proof, which uses logical operations such as modus ponens to rearrange and combine theorems derived from the premisses, but which is not guaranteed to find an elegant solution.
Suppose we know that (A) I won't need my umbrella just in case it doesn't rain today, (B) it always rains on Saturdays, and (C) today is Saturday. We want to prove whether I'll need my umbrella. Let these propositions be built out of simple ones:
P = I'll need my umbrella
Q = it will rain today
R = today is Saturday
Then the propositions we know as premisses (know to be true; are assuming to be true) are:
(A) ~Q <-> ~P
(B) R -> Q
(C) R
And what we want to ascertain is whether P (I'll need my umbrella) is a valid deduction from these.
Now we build the truth table for these:
P Q R ~Q <-> ~P , R -> Q
T T T
T T F
T F T
T F F
F T T
F T F
F F T
F F F
Boolean operators inside complex propositions need to evaluated in order of bracketing or binding, innermost to outermost. So do the negatives first:
P Q R ~Q <-> ~P , R -> Q
T T T F F
T T F F F
T F T T F
T F F T F
F T T F T
F T F F T
F F T T T
F F F T T
Now do the biconditional and the implication:
P Q R ~Q <-> ~P , R -> Q
T T T F T F T
T T F F T F T
T F T T F F F
T F F T F F T
F T T F F T T
F T F F F T T
F F T T T T F
F F F T T T T
We want to work out what follows if all three of our premisses are true. The first premiss (A), which is ~Q <-> ~P, is true in the following lines of the table:
P Q R ~Q <-> ~P , R -> Q
T T T F T F T
T T F F T F T
F F T T T T F
F F F T T T T
The next one, (B) which is R -> Q, is true in the following lines of that subtable:
P Q R ~Q <-> ~P , R -> Q
T T T F T F T
T T F F T F T
F F F T T T T
The final premiss (C) is R, and that's true in the following part of the previous subtable:
P Q R ~Q <-> ~P , R -> Q
T T T F T F T
The conclusion we're looking for is P. We see that in all lines of the current table, P is true. So P follows deductively from the three premisses. | 
