Samuel R. Buss
    "Cut Elimination In Situ"
    To appear in Gentzen's Centenary: The Quest for Consistency
    R. Kahle and M. Rathjen, eds.,
    Springer Verlag, 2015, pp. 245-277.

    Download manuscript: PDF.

Abstract:  We present methods for removing top-level cuts from a proof without significantly increasing the space used for storing the proof. For propositional logic, this requires converting a proof from tree-like to dag-like form, but it most doubles the number of lines in the proof. For first-order logic, the proof size can grow exponentially, but the proof has a succinct description and is polynomial-time uniform. We use direct, global constructions that give polynomial time methods for removing all top-level cuts from proofs. By exploiting prenex representations, this extends to removing all cuts, with proof size bounded superexponentially in the alternation of quantifiers in cut formulas.

Back to Sam Buss's publications page.