From QBFs to MALL and back via focussing
- Submitting institution
-
The University of Birmingham
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 91987256
- Type
- D - Journal article
- DOI
-
10.1007/s10817-020-09564-x
- Title of journal
- Journal of Automated Reasoning
- Article number
- -
- First page
- 1221
- Volume
- 64
- Issue
- 7
- ISSN
- 0168-7433
- Open access status
- Compliant
- Month of publication
- May
- 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
-
0
- Research group(s)
-
-
- Citation count
- 0
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper studies the alternation complexity of proof search. It is
significant because it
* applies novel proof-theoretic methods ('focussing') to derive alternating time bounds.
* obtains a tight delineation of MALL formulas according to each level of the polynomial hierarchy, improving the PSPACE-completeness result from the early '90s.
This was the first time alternation complexity in proof search gave such fine-grained bounds.
The short version was published at IJCAR'18, the top automated reasoning conference, and was invited to this special journal issue.
This work was invited for presentation at 'SAT and Interactions', a 2020 Dagstuhl seminar.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -