Logica Universalis 4 (1):1-29 (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||Formal systems proof tree transformation weak andstrong normalization cut-elimination rewriting|
|Categories||categorize this paper)|
|Through your library||Configure|
Similar books and articles
Paolo 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.
Added to index2010-02-15
Total downloads9 ( #122,297 of 722,681 )
Recent downloads (6 months)1 ( #60,006 of 722,681 )
How can I increase my downloads?