Sequent Calculi for QBFs : Their relation to bounded arithmetic, and the complexity of the witnessing problem

Abstract

G_i is Gentzen-like sequent calculi for proving QBFs, in which applications of the cut rule are restricted to QBFs form the ith level in the hierarchy of QBFs. The target formula of a quantifier rule in these calculi is restricted to quantifier-free formulas. The system G_i is closely related to theories of bounded arithmetic. A proof of a bounded formula can be translated to a G_i-proof of a QBF.For a proof system H we define the witnessing problem for a QBF from the kth level in the hierarchy to be the problem which takes as input an H-proof of a QBF form the kth level and an assignment to its free variables. The solution to the problem is a witness for the outermost existentially quantified variables.Stephen A. Cook and Tsuyoshi Morioka studied the complexity of the witnessing problem using the systems G_i. This thesis explores the complexity of the witnessing problem as studied by Cook and Morioka, brings together all of the different tools they used in their research, and presents it along with the results they proved to the reader.