Research

A quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae


Reference:

Bruscoli, P., Guglielmi, A., Gundersen, T. and Parigot, M., 2010. A quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae. In: Clarke, E. M. and Voronkov, A., eds. Logic for programming, artificial intelligence, and reasoning: 16th International Conference, LPAR-16, Dakar, Senegal, April 25–May 1, 2010, revised selected papers. Berlin: Springer, pp. 136-153. (Lecture Notes in Computer Science; 6355)

Related documents:

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

    Official URL:

    http://dx.doi.org/10.1007/978-3-642-17511-4_9

    Related URLs:

    Abstract

    Jeřábek showed in 2008 that cuts in propositional-logic deep-inference proofs can be eliminated in quasipolynomial time. The proof is an indirect one relying on a result of Atserias, Galesi and Pudlák about monotone sequent calculus and a correspondence between this system and cut-free deep-inference proofs. In this paper we give a direct proof of Jeřábek’s result: we give a quasipolynomial-time cut-elimination procedure in propositional-logic deep inference. The main new ingredient is the use of a computational trace of deep-inference proofs called atomic flows, which are both very simple (they trace only structural rules and forget logical rules) and strong enough to faithfully represent the cut-elimination.

    Details

    Item Type Book Sections
    CreatorsBruscoli, P., Guglielmi, A., Gundersen, T. and Parigot, M.
    EditorsClarke, E. M.and Voronkov, A.
    DOI10.1007/978-3-642-17511-4_9
    Related URLs
    URLURL Type
    http://arxiv.org/abs/0903.5392v1Free Full-text
    DepartmentsFaculty of Science > Computer Science
    Publisher StatementQPNDI.pdf: The original publication is available at www.springerlink.com
    StatusPublished
    ID Code25869

    Export

    Actions (login required)

    View Item

    Document Downloads

    More statistics for this item...