BETWEEN PROOF CONSTRUCTION AND SAT-SOLVING

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 . We demonstrate it by proving two essential results concerning the system. One is a natural reduction from full IPC (with all connectives) to implicational formulas of order three. Another result 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 .