Loading...
Please wait, while we are loading the content...
Similar Documents
Tableaux for the Logic of Proofs
| Content Provider | Semantic Scholar |
|---|---|
| Author | Renne, Bryan |
| Copyright Year | 2004 |
| Abstract | The Logic of Proofs, LP, is an explicit provability logic due to Artemov. The introduction of LP answered a long-standing question concerning the intended semantics of Gödel’s provability calculus and provability semantics for intuitionistic logic. The explicit nature of LP and its ability to naturally represent both modal logic and typed λcalculi, especially in light of the Curry-Howard Isomorphism, makes its applicability to Computer Science a primary focus of research in this area. In the present paper, I develop a tableau system for LP and give a semantic proof of cut elimination. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | https://academicworks.cuny.edu/cgi/viewcontent.cgi?article=1236&context=gc_cs_tr |
| Alternate Webpage(s) | http://tr.cs.gc.cuny.edu/tr/files/TR-2004001.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
