From QBFs to MALL and Back via Focussing
- PDF / 768,082 Bytes
- 25 Pages / 439.37 x 666.142 pts Page_size
- 43 Downloads / 158 Views
From QBFs to MALL and Back via Focussing Anupam Das1 Received: 8 May 2020 / Accepted: 11 May 2020 © The Author(s) 2020
Abstract In this work we investigate how to extract alternating time bounds from ‘focussed’ proof systems. Our main result is the obtention of fragments of MALLw (MALL with weakening) complete for each level of the polynomial hierarchy. In one direction we encode QBF satisfiability and in the other we encode focussed proof search, and we show that the composition of the two encodings preserves quantifier alternation, yielding the required result. By carefully composing with well-known embeddings of MALLw into MALL, we obtain a similar delineation of MALL formulas, again carving out fragments complete for each level of the polynomial hierarchy. This refines the well-known results that both MALLw and MALL are PSPACE-complete. A key insight is that we have to refine the usual presentation of focussing to account for deterministic computations in proof search, which correspond to invertible rules that do not branch. This is so that we may more faithfully associate phases of focussed proof search to their alternating time complexity. This presentation seems to uncover further dualities, at the level of proof search, than usual presentations, so could be of proof theoretic interest in its own right. Keywords Focussing · Linear logic · QBFs · Alternation · Polynomial hierarchy
1 Introduction and Motivation Proof search is one of the most general ways of deciding formulas of expressive logics, both automatically and interactively. In particular, proof systems can often be found to yield optimal decision algorithms, in terms of asymptotic complexity. To this end, we now know how to extract bounds for proof search in terms of various properties of the proof system at hand. For instance we may establish: – nondeterministic time bounds via proof complexity, e.g. [6,7,13]; – (non)deterministic space bounds via the depth of proofs or search spaces, and loopchecking, e.g. [3,12,23];
The author was supported by a Marie Skłodowska-Curie fellowship, ERC Grant 753431, while conducting part of this research.
B 1
Anupam Das [email protected] University of Birmingham, Birmingham, United Kingdom
123
A. Das
– deterministic or co-nondeterministic time bounds via systems of invertible rules, see e.g. [21,28]. However, despite considerable progress in the field, there still remains a gap between the obtention of (co-)nondeterministic time bounds, such as NP or coNP, and space bounds such as PSPACE. Phrased differently, while we have many logics we know to be PSPACEcomplete (intuitionistic propositional logic, various modal logics, etc.), we have very little understanding of their fragments corresponding to subclasses of PSPACE. An alternative view of space complexity is in terms of alternating time complexity, where a Turing machine may have both existential (i.e. nondeterminstic) and universal (i.e. co-nondeterministic) branching states. In this way PSPACE is known to be equivalent to alternating polynomial time [4]
Data Loading...
