Reference : Normality, non-contamination and logical depth in classical natural deduction
Scientific journals : Article
Engineering, computing & technology : Computer science
Normality, non-contamination and logical depth in classical natural deduction
D’Agostino, Marcello [> >]
Gabbay, Dov M. mailto [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)]
Modgil, Sanjay [> >]
Studia Logica
[en] In this paper we provide a detailed proof-theoretical analysis of a natural deduction system for classical propositional logic that (i) represents classical proofs in a more natural way than standard Gentzen-style natural deduction, (ii) admits of a simple normalization procedure such that normal proofs enjoy the Weak Subformula Property, (iii) provides the means to prove a Non-Contamination Property of normal proofs that is not satisfied by normal proofs in the Gentzen tradition and is useful for applications, especially to formal argumentation, (iv) naturally leads to defining a notion of depth of a proof, to the effect that, for every fixed natural k, normal k-depth deducibility is a tractable problem and converges to classical deducibility as k tends to infinity.

File(s) associated to this reference

Fulltext file(s):

Limited access
NNC_rev.pdfAuthor postprint435.66 kBRequest a copy

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.