Logica Universalis 4 (1):1-29 (2010)
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)|
References found in this work BETA
Citations of this work BETA
No citations found.
Similar books and articles
Syntactical Results on the Arithmetical Completeness of Modal Logic.Paolo Gentilini - 1993 - Studia Logica 52 (4):549 - 564.
The Deduction Rule and Linear and Near-Linear Proof Simulations.Maria Luisa Bonet & Samuel R. Buss - 1993 - Journal of Symbolic Logic 58 (2):688-709.
Indexed Systems of Sequents and Cut-Elimination.Grigori Mints - 1997 - Journal of Philosophical Logic 26 (6):671-696.
Identity of Proofs Based on Normalization and Generality.Kosta Došen - 2003 - Bulletin of Symbolic Logic 9 (4):477-503.
Ultimate Normal Forms for Parallelized Natural Deductions.Neil Tennant - 2002 - Logic Journal of the IGPL 10 (3):299-337.
Corrigendum to "Strong Normalization Proof with CPS-Translation for Second Order Classical Natural Deduction".Koji Nakazawa & Makoto Tatsuta - 2003 - Journal of Symbolic Logic 68 (4):1415-1416.
Strong Normalization Proof with CPS-Translation for Second Order Classical Natural Deduction.Koji Nakazawa & Makoto Tatsuta - 2003 - Journal of Symbolic Logic 68 (3):851-859.
A Short Proof of the Strong Normalization of Classical Natural Deduction with Disjunction.René David & Karim Nour - 2003 - Journal of Symbolic Logic 68 (4):1277-1288.
Added to index2010-02-15
Total downloads57 ( #90,808 of 2,158,195 )
Recent downloads (6 months)1 ( #356,322 of 2,158,195 )
How can I increase my downloads?