From QBFs to MALL and back via focussing

Research output: Contribution to journalArticlepeer-review

92 Downloads (Pure)

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.

Original languageEnglish
Pages (from-to)1221-1245
Number of pages25
JournalJournal of Automated Reasoning
Volume64
Issue number7
Early online date22 May 2020
DOIs
Publication statusPublished - Oct 2020

Keywords

  • Alternation
  • Focussing
  • Linear logic
  • Polynomial hierarchy
  • QBFs

ASJC Scopus subject areas

  • Software
  • Computational Theory and Mathematics
  • Artificial Intelligence

Fingerprint

Dive into the research topics of 'From QBFs to MALL and back via focussing'. Together they form a unique fingerprint.

Cite this