Computing with sequents and diagrams in classical logic - calculi *X, dX and ©X

This Ph.D. thesis addresses the problem of giving computational interpretation to proofs in classical logic. As such, it presents three calculi reflecting different approaches in the study of this area. The thesis consists of three parts. The first part introduces the *X calculus, whose terms represent proofs in the classical sequent calculus, and whose reduction rules capture most of the features of cut-elimination in sequent calculus. This calculus introduces terms which enable explicit implementation of erasure and duplication and to the best of our knowledge it is the first such calculus for classical logic. The second part studies the possibility to represent classical computation diagrammatically. We present the dX calculus, the diagrammatic calculus for classical logic, whose diagrams originate from *X-terms. The principal difference lies in the fact that dX has a higher level of abstraction, capturing the essence of sequent calculus proofs, as well as the essence of classical cut-elimination. The third part relates the first two. It presents the ©X calculus, a one-dimensional counterpart of the diagrammatic calculus. We start from *X, where we explicitly identify terms which should be considered the same. These are the terms that code sequent proofs which are equivalent up to permutations of independent inference rules. They also have the same diagrammatic representation. Such identification induces the congruence relation on terms. The reduction relation is defined modulo congruence rules, and reduction rules correspond to those of dX calculus.