Extracting Propostional Decidability: A Proof of Propositional Decidability in Constructive Type Theory and its Extracted Program

unofficial copies [PDF], [PS]

by James L. Caldwell

Unpublished manuscript, Cornell University, 1997.


This paper describes a formal constructive proof of the decidability of a sequent calculus presentation of classical propositional logic. The Nuprl theories and proofs reported on here are part of a larger program to safely incorporate formally justified decision procedures into theorem provers. The proof is implemented in the Nuprl system and the resulting proof object yields a "correct-by-construction" program for deciding propositional sequents. In the case the sequent is valid, the program reports that fact; in the case the sequent is falsifiable, the program returns a falsifying assignment. Also, the semantics of the propositional sequents is formulated here in Kleene's strong three valued logic which both: agrees with the standard two valued semantics; and gives finer information in case the proposition is falsifiable.