A proof calculus which reduces syntactic bureaucracy

Alessio Guglielmi, Tom Gundersen, M Parigot

Research output: Chapter in Book/Report/Conference proceedingChapter

  • 16 Citations

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.
LanguageEnglish
Title of host publicationProceedings of the 21st International Conference on Rewriting Techniques and Applications
Place of PublicationDagstuhl, Germany
PublisherLeibniz International Proceedings in Informatics
Pages135-150
Number of pages16
Volume6
DOIs
StatusPublished - 2010

Fingerprint

Calculus
Sequent Calculus
Proof System
Cut-elimination
Propositional Logic
Rewriting
Tree Structure
Trace
Syntax
Logic

Cite this

Guglielmi, A., Gundersen, T., & Parigot, M. (2010). A proof calculus which reduces syntactic bureaucracy. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications (Vol. 6, pp. 135-150). Dagstuhl, Germany: Leibniz International Proceedings in Informatics. DOI: 10.4230/LIPIcs.RTA.2010.135

A proof calculus which reduces syntactic bureaucracy. / Guglielmi, Alessio; Gundersen, Tom; Parigot, M.

Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Vol. 6 Dagstuhl, Germany : Leibniz International Proceedings in Informatics, 2010. p. 135-150.

Research output: Chapter in Book/Report/Conference proceedingChapter

Guglielmi, A, Gundersen, T & Parigot, M 2010, A proof calculus which reduces syntactic bureaucracy. in Proceedings of the 21st International Conference on Rewriting Techniques and Applications. vol. 6, Leibniz International Proceedings in Informatics, Dagstuhl, Germany, pp. 135-150. DOI: 10.4230/LIPIcs.RTA.2010.135
Guglielmi A, Gundersen T, Parigot M. A proof calculus which reduces syntactic bureaucracy. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Vol. 6. Dagstuhl, Germany: Leibniz International Proceedings in Informatics. 2010. p. 135-150. Available from, DOI: 10.4230/LIPIcs.RTA.2010.135
Guglielmi, Alessio ; Gundersen, Tom ; Parigot, M. / A proof calculus which reduces syntactic bureaucracy. Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Vol. 6 Dagstuhl, Germany : Leibniz International Proceedings in Informatics, 2010. pp. 135-150
@inbook{0314b54d3c764758b418494516c0da36,
title = "A proof calculus which reduces syntactic bureaucracy",
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.",
author = "Alessio Guglielmi and Tom Gundersen and M Parigot",
year = "2010",
doi = "10.4230/LIPIcs.RTA.2010.135",
language = "English",
volume = "6",
pages = "135--150",
booktitle = "Proceedings of the 21st International Conference on Rewriting Techniques and Applications",
publisher = "Leibniz International Proceedings in Informatics",

}

TY - CHAP

T1 - A proof calculus which reduces syntactic bureaucracy

AU - Guglielmi,Alessio

AU - Gundersen,Tom

AU - Parigot,M

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

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

U2 - 10.4230/LIPIcs.RTA.2010.135

DO - 10.4230/LIPIcs.RTA.2010.135

M3 - Chapter

VL - 6

SP - 135

EP - 150

BT - Proceedings of the 21st International Conference on Rewriting Techniques and Applications

PB - Leibniz International Proceedings in Informatics

CY - Dagstuhl, Germany

ER -