eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-08-16
9:1
9:17
10.4230/LIPIcs.CSL.2017.9
article
Removing Cycles from Proofs
Aler Tubella, Andrea
Guglielmi, Alessio
Ralph, Benjamin
If we track atom occurrences in classical propositional proofs in deep inference, we see that they can form cyclic structures between cuts and identity steps. These cycles are an obstacle to a very natural form of normalisation, that simply unfolds all the contractions in a proof. This mechanism, which we call ‘decomposition’, has many points of contact with explicit substitutions in lambda calculi. In the presence of cycles, decomposition does not terminate, and this is an obvious drawback if we want to interpret proofs computationally. One way of eliminating cycles is eliminating cuts. However, we could ask ourselves whether it is possible to eliminate cycles independently of (general) cut elimination. This paper shows an efficient way to do so, therefore establishing the independence of decomposition from cut elimination. In other words, cut elimination in propositional logic can be separated into three separate procedures: 1) cycle elimination, 2) unfolding of contractions, 3) elimination of cuts in the linear fragment.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol082-csl2017/LIPIcs.CSL.2017.9/LIPIcs.CSL.2017.9.pdf
proof theory
deep inference
proof complexity