A Proof Calculus Which Reduces Syntactic Bureaucracy
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.
Logic
Proof theory
Deep Inference
Flow graphs
Proof Systems
Open Deduction
Rewriting
Confluence
Termination
135-150
Regular Paper
Alessio
Guglielmi
Alessio Guglielmi
Tom
Gundersen
Tom Gundersen
Michel
Parigot
Michel Parigot
10.4230/LIPIcs.RTA.2010.135
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode