A Constructive Completeness Proof for Intuitionistic Propositional Calculus
| dc.contributor.author | Underwood, Judith | en_US |
| dc.date.accessioned | 2007-04-23T17:51:22Z | |
| dc.date.available | 2007-04-23T17:51:22Z | |
| dc.date.issued | 1990-12 | en_US |
| dc.description.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. | en_US |
| dc.format.extent | 824362 bytes | |
| dc.format.extent | 197270 bytes | |
| dc.format.mimetype | application/pdf | |
| dc.format.mimetype | application/postscript | |
| dc.identifier.citation | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR90-1179 | en_US |
| dc.identifier.uri | https://hdl.handle.net/1813/7019 | |
| dc.language.iso | en_US | en_US |
| dc.publisher | Cornell University | en_US |
| dc.subject | computer science | en_US |
| dc.subject | technical report | en_US |
| dc.title | A Constructive Completeness Proof for Intuitionistic Propositional Calculus | en_US |
| dc.type | technical report | en_US |