Some general results about proof normalization
Logica Universalis 4 (1) (2010)
| Abstract | In this paper, we provide a general setting under which results of normalization of proof trees such as, for instance, the logicality result in equational reasoning and the cut-elimination property in sequent or natural deduction calculi, can be unified and generalized. This is achieved by giving simple conditions which are sufficient to ensure that such normalization results hold, and which can be automatically checked since they are syntactical. These conditions are based on basic properties of elementary combinations of inference rules which ensure that the induced global proof tree transformation processes do terminate. | |||||||||
| Keywords | No keywords specified (fix it) | |||||||||
| Categories | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,672 |
| External links |
 |
| Through your library | Configure |
Similar books and articlesPaolo Gentilini (1993). Syntactical Results on the Arithmetical Completeness of Modal Logic. Studia Logica 52 (4):549 - 564.
Maria Luisa Bonet & Samuel R. Buss (1993). The Deduction Rule and Linear and Near-Linear Proof Simulations. Journal of Symbolic Logic 58 (2):688-709.
Grigori Mints (1997). Indexed Systems of Sequents and Cut-Elimination. Journal of Philosophical Logic 26 (6):671-696.
Kosta Došen (2003). Identity of Proofs Based on Normalization and Generality. Bulletin of Symbolic Logic 9 (4):477-503.
David J. Pym (1995). A Note on the Proof Theory the λII-Calculus. Studia Logica 54 (2):199 - 230.
Koji Nakazawa & Makoto Tatsuta (2003). Corrigendum to "Strong Normalization Proof with CPS-Translation for Second Order Classical Natural Deduction". Journal of Symbolic Logic 68 (4):1415-1416.
Koji Nakazawa & Makoto Tatsuta (2003). Strong Normalization Proof with CPS-Translation for Second Order Classical Natural Deduction. Journal of Symbolic Logic 68 (3):851-859.
Ulrich Berger, Stefan Berghofer, Pierre Letouzey & Helmut Schwichtenberg (2006). Program Extraction From Normalization Proofs. Studia Logica 82 (1):25 - 49.
René David & Karim Nour (2003). A Short Proof of the Strong Normalization of Classical Natural Deduction with Disjunction. Journal of Symbolic Logic 68 (4):1277-1288.
Analytics
Monthly downloads
Sorry, there are not enough data points to plot this chart.
|
Added to index2010-02-15Total downloads8 ( #123,036 of 549,070 )Recent downloads (6 months)0How can I increase my downloads? |
My notes
Discussion
