JavaScript is disabled for your browser. Some features of this site may not work without it.
eCommons will become read-only at noon on May 26 for an infrastructure update. Submissions will not be accepted at this time. We anticipate that this update will be completed by June 2 at 5 p.m.
Please contact us at ecommons-admin@cornell.edu if you have questions or concerns.
A Constructive Completeness Proof for Intuitionistic Propositional Calculus
Abstract
This paper presents a constructive proof of completeness of Kripke models for the intuitionistic propositional calculus. The computational content of the proof is a form of the tableau decision procedure. If a formula is valid, the algorithm produces a proof of the formula in the form of an inhabitant of the corresponding type; if not, it produces a Kripke model and a state in the model such that the formula is not forced at that state in that model.
Date Issued
1990-12Publisher
Cornell University
Subject
computer science; technical report
Previously Published As
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR90-1179
Type
technical report