Classical Propositional Decidability via Nuprl Proof Extraction

unofficial copies [PDF], [PS]

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, 1998.


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