[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.
Disciplines :
Computer science
Author, co-author :
D’Agostino, Marcello
GABBAY, Dov M. ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
Modgil, Sanjay
External co-authors :
yes
Language :
English
Title :
Normality, non-contamination and logical depth in classical natural deduction
scite shows how a scientific paper has been cited by providing the context of the citation, a classification describing whether it supports, mentions, or contrasts the cited claim, and a label indicating in which section the citation was made.