Research

Normalisation control in deep inference via atomic flows


Reference:

Guglielmi, A. and Gundersen, T., 2008. Normalisation control in deep inference via atomic flows. Logical Methods in Computer Science, 4 (1), 9.

Related documents:

[img]
Preview
PDF - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
Download (399kB) | Preview

    Official URL:

    http://dx.doi.org/10.2168/LMCS-4(1:9)2008

    Abstract

    We introduce `atomic flows': they are graphs obtained from derivations by tracing atom occurrences and forgetting the logical structure. We study simple manipulations of atomic flows that correspond to complex reductions on derivations. This allows us to prove, for propositional logic, a new and very general normalisation theorem, which contains cut elimination as a special case. We operate in deep inference, which is more general than other syntactic paradigms, and where normalisation is more difficult to control. We argue that atomic flows are a significant technical advance for normalisation theory, because 1) the technique they support is largely independent of syntax; 2) indeed, it is largely independent of logical inference rules; 3) they constitute a powerful geometric formalism, which is more intuitive than syntax.

    Details

    Item Type Articles
    CreatorsGuglielmi, A.and Gundersen, T.
    DOI10.2168/LMCS-4(1:9)2008
    DepartmentsFaculty of Science > Computer Science
    RefereedYes
    StatusPublished
    ID Code5260

    Export

    Actions (login required)

    View Item

    Document Downloads

    More statistics for this item...