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复杂度类的若干自然子类。实验结果表明，仅在少数情况下简单判定过程需要大量计算时间。