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.
1. Introduction 1.1. Background and Motivation 1.2. Overview of Thesis 2. Preliminaries 2.1. Propositional Proof Systems 2.2. LK and Quantified Propositional Logic 2.3. Boolean Programs 2.4. Notational Conventions 3. BPLK and G 3.1. BPLK 3.2. Basic Results on BPLK and G 4. BPLK P-Stimulates G 4.1. Special Notation 4.2. A Translation from the Language of G to that of BPLK 4.3. A Simulation of G by BPLK 5. G P-Stimulates BPLK 5.1. A Translation from the Language of BPLK to that of G 5.2. A Simulation of BPLK by G 6. Future Work and Conclusion 6.1. A Technical Improvement 6.2. Witnessing and Search Problems 6.3. Subsystems of BPLK 6.4. Miscellaneous Bibliography
