Skip to main content
PRL Project

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

by James L. Caldwell

Unpublished manuscript

  • unofficial copies PDF, PS

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.

bibTex ref: Cal97b

cite link