Journal article icon

Journal article

Frege systems for quantified Boolean logic

Abstract:

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 le...

Expand abstract
Publication status:
Published
Peer review status:
Peer reviewed

Actions


Access Document


Files:
Publisher copy:
10.1145/3381881

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Role:
Author
Publisher:
Association for Computing Machinery
Journal:
Journal of the ACM More from this journal
Volume:
67
Issue:
2
Article number:
9
Publication date:
2020-04-01
Acceptance date:
2020-02-01
DOI:
EISSN:
1557-735X
ISSN:
0004-5411
Language:
English
Keywords:
Pubs id:
1104892
Local pid:
pubs:1104892
Deposit date:
2020-05-19

Terms of use


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP