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 in 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. (shrink)

Can argumentation form the basis for any form of reasoning, informal or formal logical reasoning? We examine this question from the particular perspective of the recent developments in logic-based Artificial Intelligence (AI). We propose that argumentation provides the wider framework encompassing uniformly all reasoning, with strict or formal logical reasoning being a special boundary case. We also attempt to link this unifying role of argumentation with Aristotle’s original investigation of methods and forrmalisms for the systematic study of human reasoning.