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
Social Program
Location and Venue
Colocated Events
Authors' instructions
Print current pagePrint 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 Valid HTML 4.01! Valid CSS! Debian