In this paper we describe a formal constructive proof of the decidability of a sequent calculus for classical propositional logic. The proof is implemented in the Nuprl system and the resulting proof object yields a "correct-by-construction" program for deciding propositional sequents. If the sequent is valid, the program reports that fact; otherwise, the program returns a counter-example in the form of a falsifying assignment. We employ Kleene's strong three-valued logic to give more informative counter-examples, it is also shown how this semantics agrees with the standard two-valued presentation.

See also: Jim Caldwell's development of Classical Propositional Logic