Computer Science Logic and 8th Kurt Gödel Colloquium Kai Brünnler: Atomic Cut Elimination for Classical Logic

Welcome and News Host Institutions Calls and Deadlines Program Social Program Registration Location and Venue Accommodation Committees Contact Colocated Events Authors' instructions

Print this page 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. © 2002-2003 Kurt Gödel Society, Norbert Preining. 2003-06-04