Classical Propositional Decidability via Nuprl Proof Extraction
by James L. Caldwell
Proceedings of 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs '98), J. Grundy and M. Newey (eds.), LNCS 1479, pp. 105-122, Springer-Verlag
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.
bibTex ref: Cal98