Classical Proofs' Essence and Diagrammatic Computation

We present a congruence relation on classical proofs represented in the sequent calculus, which identifies proofs up to trivial rule permutation. The study is performed in the framework of *X calculus, designed to provide a Curry-Howard correspondence for classical logic, and the diagrammatic calculus. We show that each congruence class has a single diagrammatic representation. Congruence equations are given explicitly and induce a congruence relation on terms so that reducing modulo this relation, on terms, corresponds to diagram reduction.