## Alternating time bounds from variants of focussed proof systems

Intuitionistic logic and the polynomial hierarchy We conduct a complexity-theoretic study of focussed proof systems, relating the alternation of synchronous and asynchronous phases in a proof to an appropriate alternating time hierarchy, for instance the polynomial hierarchy. We propose a notion of ‘over-focussing’ that admits non-branching invertible rules during synchronous phases, due to the fact …