On the proof complexity of deep inference


Bruscoli, P. and Guglielmi, A., 2009. On the proof complexity of deep inference. ACM Transactions on Computational Logic, 10 (2), 14.

Related documents:

PDF (Author's accepted version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
Download (331kB) | Preview

    Official URL:

    Related URLs:


    We obtain two results about the proof complexity of deep inference: (1) Deep-inference proof systems are as powerful as Frege ones, even when both are extended with the Tseitin extension rule or with the substitution rule; (2) there are analytic deep-inference proof systems that exhibit an exponential speedup over analytic Gentzen proof systems that they polynomially simulate.


    Item Type Articles
    CreatorsBruscoli, P.and Guglielmi, A.
    Related URLs
    URLURL Type
    Uncontrolled Keywordsfrege systems,calculus of structures,deep inference,analyticity,statman tautologies,theory
    DepartmentsFaculty of Science > Computer Science
    Publisher StatementPrComplDI.pdf: © ACM, 2009. This is the authors’ version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACM Transactions on Computational Logic 10 (2:14) 2009, pp. 1–34,
    ID Code14343


    Actions (login required)

    View Item

    Document Downloads

    More statistics for this item...