Research

A proof calculus which reduces syntactic bureaucracy


Reference:

Guglielmi, A., Gundersen, T. and Parigot, M., 2010. A proof calculus which reduces syntactic bureaucracy. In: Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Vol. 6. Dagstuhl, Germany: Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, pp. 135-150.

Related documents:

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

    Official URL:

    http://dx.doi.org/10.4230/LIPIcs.RTA.2010.135

    Related URLs:

    Abstract

    In usual proof systems, like the sequent calculus, only a very limited way of combining proofs is available through the tree structure. We present in this paper a logic-independent proof calculus, where proofs can be freely composed by connectives, and prove its basic properties. The main advantage of this proof calculus is that it allows to avoid certain types of syntactic bureaucracy inherent to all usual proof systems, in particular the sequent calculus. Proofs in this system closely reflect their atomic flow, which traces the behaviour of atoms through structural rules. The general definition is illustrated by the standard deep-inference system for propositional logic, for which there are known rewriting techniques that achieve cut elimination based only on the information in atomic flows.

    Details

    Item Type Book Sections
    CreatorsGuglielmi, A., Gundersen, T. and Parigot, M.
    DOI10.4230/LIPIcs.RTA.2010.135
    Related URLs
    URLURL Type
    http://dx.doi.org/10.4230/LIPIcs.RTA.2010.135Free Full-text
    DepartmentsFaculty of Science > Computer Science
    StatusPublished
    ID Code25870

    Export

    Actions (login required)

    View Item

    Document Downloads

    More statistics for this item...