Between proof construction and SAT-solving
Aleksy Schubert, Paweł Urzyczyn, Konrad Zdanowski
TL;DR
This work argues that provability in the implicational fragment of intuitionistic propositional logic (IIPC) serves as a natural, expressive tool for encoding and solving $\,\mathrm{PSPACE}$-class problems. It shows that full IPC provability reduces to the provability of order-$3$ implicational formulas and offers an alternating-automata interpretation that aligns proof search with computation. The paper identifies concrete low-order fragments corresponding to $\mathrm{P}$, $\mathrm{NP}$, and $\mathrm{co}$-$\mathrm{NP}$, providing precise complexity results and reductions (e.g., $\mathbb{T}_{3-}$ is $\mathrm{NP}$-complete, order-$2$ plus is $\mathrm{co}$-$\mathrm{NP}$-complete). Overall, it highlights the computational content of constructive proof search and suggests interactive approaches for PSPACE problems, with ties to modal formalisms via embeddings to $\mathrm{S4}$.
Abstract
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.