Lower Bounds: From Circuits to QBF Proof Systems

No abstract is available for this paper.

• Publication year

  2016

• Venue

  Information Technology Convergence and Services

• Publication date

  2016-01-14

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1145/2840728.2840740
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Proof Complexity of Resolution-based QBF Calculi

  2015influential reference
• Expansion-based QBF solving versus Q-resolution

  2015influential reference
• Feasible Interpolation for QBF Resolution Calculi

  2015cited by this paper
• On Unification of QBF Resolution-Based Calculi

  2014influential reference
• Unified Characterisations of Resolution Hardness Measures

  2014cited by this paper
• A Unified Proof System for QBF Preprocessing

  2014cited by this paper
• QBF Resolution Systems and Their Proof Complexities

  2014cited by this paper
• Conformant planning as a case study of incremental QBF solving

  2014cited by this paper
• Contributions to the Theory of Practical Quantified Boolean Formula Solving

  2012influential reference
• Annals of Pure and Applied Logic

  2012influential reference
• Unified QBF certification and its applications

  2012cited by this paper
• On Sequent Systems and Resolution for QBFs

  2012cited by this paper
• Complexity of Propositional Proofs

  2010cited by this paper
• Introduction to Circuit Complexity: A Uniform Approach

  2010cited by this paper
• Computational Complexity: A Modern Approach

  2009cited by this paper
• On lengths of proofs in non-classical logics

  2009cited by this paper
• Substitution Frege and extended Frege proof systems in non-classical logics

  2009cited by this paper
• QBF-Based Formal Verification: Experience and Perspectives

  2008cited by this paper
• Using the Groebner Basis Algorithm to Nd Proofs of Unsatissability

  2008cited by this paper
• Interpolation Theorems, Lower Bounds for Proof Systems, and Independence Results for Bounded Arithmetic

  2007cited by this paper
• Asymptotically Optimal Encodings of Conformant Planning in QBF

  2007cited by this paper
• Quantified propositional calculus and a second-order theory for NC1

  2005cited by this paper
• Weak Pigeonhole Principle, and Randomized Computation

  2005cited by this paper
• Learning decision lists

  2004cited by this paper
• Propositional Proof Complexity: Past, Present and Future

  2001cited by this paper
• Short proofs are narrow—resolution made simple

  2001cited by this paper
• On Interpolation and Automatization for Frege Systems

  2000cited by this paper
• Non-Automatizability of Bounded-Depth Frege Proofs

  1999cited by this paper
• Some Consequences of Cryptographical Conjectures for S12 and EF

  1998cited by this paper
• Lower bounds for resolution and cutting plane proofs and monotone computations

  1997cited by this paper
• Using the Groebner basis algorithm to find proofs of unsatisfiability

  1996influential reference
• Cutting planes, connectivity, and threshold logic

  1996cited by this paper
• Resolution for Quantified Boolean Formulas

  1995cited by this paper
• An Exponential Lower Bound to the Size of Bounded Depth Frege Proofs of the Pigeonhole Principle

  1995influential reference
• Bounded arithmetic, propositional logic, and complexity theory

  1995cited by this paper
• Exponential lower bounds for the pigeonhole principle

  1993cited by this paper
• Quantified propositional calculi and fragments of bounded arithmetic

  1990cited by this paper
• In handbook of theoretical computer science

  1990cited by this paper
• Propositional proof systems, the consistency of first order theories and the complexity of computations

  1989cited by this paper
• The complexity of the Pigeonhole Principle

  1988cited by this paper
• On the complexity of cutting-plane proofs

  1987cited by this paper
• Algebraic methods in the theory of lower bounds for Boolean circuit complexity

  1987cited by this paper
• Lower bounds on the size of bounded depth circuits over a complete basis with logical addition

  1987influential reference
• Almost optimal lower bounds for small depth circuits

  1986influential reference
• The Intractability of Resolution

  1985cited by this paper
• The Relative Efficiency of Propositional Proof Systems

  1979influential reference
• Bounds to Complexities of Networks for Sorting and for Switching

  1975cited by this paper
• A Machine-Oriented Logic Based on the Resolution Principle

  1965cited by this paper
• Review: C. West Churchman, Elements of Logic and Formal Science

  1941cited by this paper
• Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence A Uniform Approach for Generating Proofs and Strategies for Both True and False QBF Formulas

  year unknowncited by this paper

• Semi-Algebraic Proof Systems for QBF

  2025cites this paper
• Strong (D)QBF Dependency Schemes via Implication-free Resolution Paths

  2024cites this paper
• The Riis Complexity Gap for QBF Resolution

  2024cites this paper
• Understanding Nullstellensatz for QBFs

  2023cites this paper
• Hardness Characterisations and Size-width Lower Bounds for QBF Resolution

  2022influential citation
• Extending Prolog for Quantified Boolean Horn Formulas

  2021cites this paper
• How QBF Expansion Makes Strategy Extraction Hard

  2020cites this paper
• Hard QBFs for Merge Resolution

  2020cites this paper
• Frege Systems for Quantified Boolean Logic

  2020cites this paper
• Strong (D)QBF Dependency Schemes via Tautology-Free Resolution Paths

  2020cites this paper
• Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution

  2020influential citation
• Building Strategies into QBF Proofs

  2020cites this paper
• Fd and Logical Restrictions

  2019cites this paper
• Frege Systems

  2019cites this paper
• Proof complexity

  2019cites this paper
• QRAT Polynomially Simulates ∀-Exp+Res

  2019cites this paper
• Lower Bound Techniques for QBF Expansion

  2019cites this paper
• New Resolution-Based QBF Calculi and Their Proof Complexity

  2019cites this paper
• Concepts and Problems

  2019cites this paper
• Reasons for hardness in QBF proof complexity

  2019cites this paper
• Proof complexity of modal resolution systems

  2019influential citation
• Optimality

  2019cites this paper
• Algebraic and Geometric Proof Systems

  2019cites this paper
• Model Theory and Lower Bounds

  2019cites this paper
• Up to EF via the 〈. . .〉 Translation

  2019cites this paper
• Introduction

  2019cites this paper
• Hard Tautologies

  2019cites this paper
• The Two Worlds of Bounded Arithmetic

  2019cites this paper
• Further Proof Systems

  2019cites this paper
• Bibliography

  2019cites this paper
• LKd+1/2 and Combinatorial Restrictions

  2019cites this paper
• Feasible Interpolation: Applications

  2019cites this paper
• Basic Example of the Correspondence between Theories and Proof Systems

  2019cites this paper
• Sequent Calculus

  2019cites this paper
• Quantified Propositional Calculus

  2019cites this paper
• Feasible Interpolation: A Framework

  2019cites this paper
• Index

  2019cites this paper
• Preface

  2019cites this paper
• Examples of Upper Bounds and p-Simulations

  2019cites this paper
• Beyond EF via the || . . . || Translation

  2019cites this paper
• The Nature of Proof Complexity

  2019cites this paper
• R and R-Like Proof Systems

  2019cites this paper
• Short Proofs in QBF Expansion

  2019cites this paper
• Characterising tree-like Frege proofs for QBF

  2019cites this paper
• QRAT Polynomially Simulates ∀ \text -Exp+Res

  2019cites this paper
• Relating size and width in variants of Q-resolution

  2018cites this paper
• This is a repository copy of Size , Cost , and Capacity : A Semantic Technique for Hard Random

  2018influential citation
• Hardness and Optimality in QBF Proof Systems Modulo NP

  2018influential citation
• Understanding Cutting Planes for QBFs

  2018cites this paper
• Genuine Lower Bounds for QBF Expansion

  2018cites this paper
• Lower Bound Techniques for QBF Proof Systems

  2018cites this paper
• Reasons for Hardness in QBF Proof Systems

  2018influential citation
• Local Soundness for QBF Calculi

  2018cites this paper
• More on Size and Width in QBF Resolution

  2018cites this paper
• Formulas with Large Weight: a New Technique for Genuine QBF Lower Bounds

  2017influential citation
• A Little Blocked Literal Goes a Long Way

  2017cites this paper
• 2 Reasons for Hardness in QBF Proof Systems ( QU-Res )

  2017cites this paper
• Reasons for Hardness in Quantified Boolean Formulas ?

  2017influential citation
• Size, Cost, and Capacity: A Semantic Technique for Hard Random QBFs

  2017influential citation
• QBF proof complexity

  2017cites this paper
• Lifting QBF Resolution Calculi to DQBF

  2016cites this paper
• Dependency Schemes in QBF Calculi: Semantics and Soundness

  2016cites this paper
• Solving QBF by Abstraction

  2016cites this paper
• 2 Understanding Cutting Planes for QBFs

  2016cites this paper
• Extension Variables in QBF Resolution

  2016cites this paper
• Are Short Proofs Narrow? QBF Resolution Is Not So Simple

  2016influential citation
• Understanding Gentzen and Frege Systems for QBF

  2016influential citation
• A Game Characterisation of Tree-like Q-resolution Size

  2015cites this paper
• Feasible Interpolation for QBF Resolution Calculi

  2015cites this paper
• Towards P (cid:54) = NP from Extended Frege lower bounds

  year unknowncites this paper
• EasyChair Preprint No 362 Local Soundness for QBF Calculi

  year unknowncites this paper
• Frege Systems for Quantified Boolean Logic

  year unknowncites this paper