Title: Strong Normalisation of Cut-Elimination in Classical Logic
Abstract: In this paper a strongly normalizing cut-elimination procedure is presented for classical logic. The procedure adapts the standard cut transformations, see for example []. 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.
Publication Year: 1999
Publication Date: 1999-01-01
Language: en
Type: book-chapter
Indexed In: ['crossref']
Access and Citation
Cited By Count: 17
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot