Atomic Cut Elimination for classical Logic

System SKS is a set of rules for classical propositional logic presented in the calculus of structures. Like sequent systems and unlike natural deduction systems, it has an explicit cut rule, which is admissible. In contrast to sequent systems, the cut rule can easily be reduced to atomic form. This allows for a very simple cut elimination procedure based on plugging in parts of a proof, like normalisation in natural deduction and unlike cut elimination in the sequent calculus. It should thus be a good common starting point for investigations into both proof search as computation and proof normalisation as computation. Keywords. sequent calculus, natural deduction, cut elimination, classical logic, atomic cut.

• Type: Conference
• Year: 2003
• Where: CSL
• Authors: Kai Brünnler
• Keywords: CSL 2003, Cut Elimination, Natural Deduction, Sequent