From QBFs to MALL and back via focussing

Anupam Das*

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

106 Downloads (Pure)


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
Issue number7
Early online date22 May 2020
Publication statusPublished - Oct 2020

Bibliographical note

Funding Information:
The author was supported by a Marie Skłodowska-Curie fellowship, ERC Grant 753431, while conducting part of this research.

I would like to thank Taus Brock-Nannestad, Kaustuv Chaudhuri, Sonia Marin and Dale Miller for many fruitful discussions about focussing, in particular on the presentation of it herein. I am particularly grateful to Sonia Marin and the anonymous reviewers of both this work and the previous conference version, [9], for their careful and helpful proofreading.

Publisher Copyright:
© 2020, The Author(s).


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

ASJC Scopus subject areas

  • Software
  • Computational Theory and Mathematics
  • Artificial Intelligence


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

Cite this