The classical satisfiability problem (SAT) is used as a natural and general tool to express and solve combinatorial problems that are in NP. We postulate that provability for implicational intuitionistic propositional logic (IIPC) can serve as a similar natural tool to express problems in Pspace. This approach can be particularly convenient for two reasons. One is that provability in full IPC (with all connectives) can be reduced to provability of implicational formulas of order three. Another advantage is a convenient interpretation in terms of simple alternating automata. Additionally, we distinguish some natural subclasses of IIPC corresponding to the complexity classes NP and co-NP. Our experimental results show that a simple decision procedure requires a significant amount of time only in a small fraction of cases.

翻译：经典可满足性问题（SAT）被用作表达和求解NP中组合问题的自然通用工具。我们提出，直觉主义命题逻辑蕴涵片段（IIPC）的可证性可作为表达PSPACE中问题的类似自然工具。这一方法具有双重便利性：其一，完整IPC（含所有连接词）的可证性可归约为三阶蕴涵公式的可证性；其二，可借助简单交替自动机进行直观解释。此外，我们区分了IIPC中对应于复杂度类NP和co-NP的若干自然子类。实验结果表明，仅在少数情形下，简单判定程序需要显著的计算时间。