Frege Systems for Quantified Boolean Logic
| Autor: | Olaf Beyersdorff, Ilario Bonacina, Ján Pich, Leroy Chew |
|---|---|
| Přispěvatelé: | Universitat Politècnica de Catalunya. Departament de Ciències de la Computació |
| Rok vydání: | 2020 |
| Předmět: |
Simulations
Frege system 0102 computer and information sciences Intuitionistic logic 01 natural sciences Upper and lower bounds Sequent calculus Artificial Intelligence Sequent 0101 mathematics Circuit complexity Complexitat computacional Mathematics Discrete mathematics Proof complexity 010102 general mathematics Lower bounds Informàtica::Informàtica teòrica::Algorísmica i teoria de la complexitat [Àrees temàtiques de la UPC] Exponential function Computational complexity QBF proof complexity TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Strategy extraction 010201 computation theory & mathematics Hardware and Architecture Control and Systems Engineering Frege systems Software Information Systems |
| Zdroj: | UPCommons. Portal del coneixement obert de la UPC Universitat Politècnica de Catalunya (UPC) |
| ISSN: | 1557-735X 0004-5411 |
| DOI: | 10.1145/3381881 |
| Popis: | We define and investigate Frege systems for quantified Boolean formulas (QBF). For these new proof systems, we develop a lower bound technique that directly lifts circuit lower bounds for a circuit class C to the QBF Frege system operating with lines from C. Such a direct transfer from circuit to proof complexity lower bounds has often been postulated for propositional systems but had not been formally established in such generality for any proof systems prior to this work. This leads to strong lower bounds for restricted versions of QBF Frege, in particular an exponential lower bound for QBF Frege systems operating with AC0[p] circuits. In contrast, any non-trivial lower bound for propositional AC0[p]-Frege constitutes a major open problem. Improving these lower bounds to unrestricted QBF Frege tightly corresponds to the major problems in circuit complexity and propositional proof complexity. In particular, proving a lower bound for QBF Frege systems operating with arbitrary P/poly circuits is equivalent to either showing a lower bound for P/poly or for propositional extended Frege (which operates with P/poly circuits). We also compare our new QBF Frege systems to standard sequent calculi for QBF and establish a correspondence to intuitionistic bounded arithmetic. This research was supported by grant nos. 48138 and 60842 from the John Templeton Foundation, EPSRC grant EP/L024233/1, and a Doctoral Prize Fellowship from EPSRC (third author). The second author was funded by the European Research Council under the European Union’s Seventh Framework Programme (FP7/2007–2013)/ERC grant agreement no. 279611 and under the European Union’s Horizon 2020 Research and Innovation Programme/ERC grant agreement no. 648276 AUTAR. The fourth author was supported by the Austrian Science Fund (FWF) under project number P28699 and by the European Research Council under the European Union’s Seventh Framework Programme (FP7/2007-2014)/ERC Grant Agreement no. 61507. Part of this work was done when Beyersdorff and Pich were at the University of Leeds and Bonacina at Sapienza University Rome. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|