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. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Brünnler, K. (2003). Atomic cut elimination for classical logic. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2803, 86–97. https://doi.org/10.1007/978-3-540-45220-1_9
Mendeley helps you to discover research relevant for your work.