Some General Results About Proof Normalization

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 si...

Full description

Saved in:
Bibliographic Details
Published in:Logica universalis 2010-03, Vol.4 (1), p.1-29
Main Authors: Aiguier, Marc, Longuet, Delphine
Format: Article
Language:English
Subjects:
Computer Science
Logic
Logic in Computer Science
Mathematics
Mathematics and Statistics
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1661-8297
1661-8300
DOI:10.1007/s11787-010-0011-4