An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic
- 1 February 1993
- journal article
- Published by Oxford University Press (OUP) in Journal of Logic and Computation
- Vol. 3 (1) , 63-75
- https://doi.org/10.1093/logcom/3.1.63
Abstract
We present a certain calculus LG which is equivalent to intuitionistic prepositional logic and in which lengths of deductions are linearly bounded in terms, of the size of the endsequent. Backwards application of the rules of LG thus gives rise to an O(n log n)-SPACE decision algorithm for intuitionistic prepositional logic. The system LG is easily implemented as a tableau system for intuitionistic logic. It is therefore of interest in its own right.Keywords
This publication has 0 references indexed in Scilit: