Simulating non-prenex cuts in quantified propositional calculus
We show that the quantified propositional proof systems Gi are polynomially equivalent to their restricted versions that require all cut formulas to be prenex ?qi (or prenex ?qi). Previously this was known only for the treelike systems G*i.  2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim
quantified propositional calculus proof complexity prenex cuts msc (2010) 03f20