An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic
Jörg Hudelmaier · Journal of Logic and Computation · 1993
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.