## From QBFs to MALL and back via focussing

*IJCAR '18*paper). arXiv

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 …