Research

On the proof complexity of deep inference


Reference:

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

Related documents:

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

    Official URL:

    http://dx.doi.org/10.1145/1462179.1462186

    Abstract

    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.

    Details

    Item Type Articles
    CreatorsBruscoli, P.and Guglielmi, A.
    DOI10.1145/1462179.1462186
    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, http://doi.acm.org/10.1145/1462179.1462186.
    RefereedYes
    StatusPublished
    ID Code14343

    Export

    Actions (login required)

    View Item

    Document Downloads

    More statistics for this item...