Propositional Logics Complexity and the Sub-Formula Property
In 1979 Richard Statman proved, using proof-theory, that the purely implicational fragment of Intuitionistic Logic (M-imply) is PSPACE-complete. He showed a polynomially bounded translation from full Intuitionistic Propositional Logic into its implicational fragment. By the PSPACE-completeness of S4...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2015-04-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1401.8209v3 |