Frege systems for quantified Boolean logic
- Submitting institution
-
University of Oxford
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 11842
- Type
- D - Journal article
- DOI
-
10.1145/3381881
- Title of journal
- Journal of the ACM
- Article number
- 9
- First page
- 1
- Volume
- 67
- Issue
- 2
- ISSN
- 0004-5411
- Open access status
- Compliant
- Month of publication
- April
- Year of publication
- 2020
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
3
- Research group(s)
-
-
- Citation count
- 1
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This is the journal version of conference papers in ITCS'16 and LICS'16. It introduces Frege proof systems for quantified Boolean formulas (QBF) and proves length-of-proofs lower bounds for some of these systems. Moreover, it shows that proving lower bounds for QBF Frege systems is equivalent to proving either circuit lower bounds or Frege lower bounds, which reduces the complexity of QBF solving to central problems in circuit complexity and proof complexity. Many subsequent works expanded the methods introduced in the paper with a particular focus on weaker proof systems which are closer to the practice of QBF solving.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -