We present a new propositional proof system based on a recent new characterization of polynomial space (PSPACE) called Boolean Programs, due to Cook and Soltys. We show that this new system, BPLK, is polynomially equivalent to the system G, which is based on the familiar and very different quantified Boolean formula (QBF) characterization of PSPACE due to Stockmeyer and Meyer. We conclude with a discussion of some closely related open problems and their implications.
展开▼
