We now both have the semantics and the syntax of propositional logic. With this in place we only need to evaluate every permutation of atoms. We need to delve into what a model is: a concrete assignment of atoms from the set {true,false}. Say we have the contingent proposition p \Rightarrow q \Rightarrow r. We can list this in a truth table as
| p | q | r | p ⇒ q ⇒ r |
| T | T | T | T |
| F | T | T | T |
| T | F | T | T |
| F | F | T | T |
| T | T | F | F |
| F | T | F | T |
| T | F | F | T |
| F | F | F | T |
Here every ordered set of atomic values describes a model. This we have as the set of ordered sets: {{T,T,T},{F,T,T},{T,F,T} ... {F,F,F}}. Each of these models are used to evaluate more and more complex propositions. The simplest way I found to create these models is to alternate. First for n different atomic variables we have 2^{n} permutations or models. The left most column, the one under p, we alternate for every new model. For the next column we alternate for every 2 models. For the next for every 4 models and so on. We just double the number for which we alternate.
Now for every model we evaluate the parse tree to obtain a truth value for the whole expression.
And we have our application. Simple as that.
If we have some proposition, we can proof its validity by creating the truth table. If the truth table results in a tautology, the proposition is proofed.