An \(O(n\;\log\;n)\)-space decision procedure for intuitionistic propositional logic. (English) Zbl 0788.03010

Hudelmaier, Jörg

J. Log. Comput. 3, No. 1, 63-75 (1993).

Summary: We present a certain calculus LG which is equivalent to intuitionistic propositional 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 propositional logic. The system LG is easily implemented as a tableau system for intuitionistic logic. It is therefore of interest in its own right.

MSC:

03B25	Decidability of theories and sets of sentences
03D15	Complexity of computation (including implicit computational complexity)
03B20	Subsystems of classical logic (including intuitionistic logic)
68Q25	Analysis of algorithms and problem complexity
03F05	Cut-elimination and normal-form theorems

Keywords:

decision procedure; sequent calculus; intuitionistic propositional logic; decision algorithm; tableau system; intuitionistic logic