In this paper a strongly normalizing cut-elimination procedure is presented for classical logic. The procedure adapts the standard cut transformations, see for example [12]. In particular our cutelimination procedure requires no special annotations on formulae. We design a term calculus for a variant of Kleene’s sequent calculus G3 via the Curry-Howard correspondence and the cut-elimination steps are given as rewrite rules. In the strong normalization proof we adapt the symmetric reducibility candidates developed by Barbanera and Berardi.
CITATION STYLE
Urban, C., & Bierman, G. M. (1999). Strong normalisation of cut-elimination in classical logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1581, pp. 365–380). Springer Verlag. https://doi.org/10.1007/3-540-48959-2_26
Mendeley helps you to discover research relevant for your work.