Powered by OpenAIRE graph
Found an issue? Give us feedback
image/svg+xml Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Closed Access logo, derived from PLoS Open Access logo. This version with transparent background. http://commons.wikimedia.org/wiki/File:Closed_Access_logo_transparent.svg Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Archivio istituziona...arrow_drop_down
image/svg+xml Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Closed Access logo, derived from PLoS Open Access logo. This version with transparent background. http://commons.wikimedia.org/wiki/File:Closed_Access_logo_transparent.svg Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao
versions View all 2 versions
addClaim

Classical Natural Deduction.

Authors: D'AGOSTINO, Marcello;

Classical Natural Deduction.

Abstract

Gentzen introduced his sequent calculi LK and LJ, as well as his natural deduction systems NK and NJ, in his celebrated “Investigations into Logical Deduction” (1935). As far as classical logic is concerned both the natural deduction calculus NK and the sequent calculus LK run into serious difficulties from the computational viewpoint. In this work we argue that the origin of such computational problems can be traced back to the fact that, contrary to a widespread opinion, neither of these calculi provides an adequate representation of the classical notion of deduction (in particular of the bivalent semantics on which it is based), and propose an alternative approach: a new system of “classical natural deduction” which substantially differs from Gentzen’s one and closely corresponds to classical semantics. We then prove two main results: (i) a normalization theorem for our new classical system and (ii) an exponential speed-up of this system over Gentzen’s ones; normal deductions in our system are uniformly shorter, and often exponentially shorter, than normal (or cut-free) deductions in Gentzen’s systems.

Country
Italy
Related Organizations
Keywords

Natural Deduction; Classical semantics; Computational Complexity; Normalization

  • BIP!
    Impact byBIP!
    selected citations
    These citations are derived from selected sources.
    This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    0
    popularity
    This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
    Average
    influence
    This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    Average
    impulse
    This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
    Average
Powered by OpenAIRE graph
Found an issue? Give us feedback
selected citations
These citations are derived from selected sources.
This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Citations provided by BIP!
popularity
This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
BIP!Popularity provided by BIP!
influence
This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Influence provided by BIP!
impulse
This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
BIP!Impulse provided by BIP!
0
Average
Average
Average
Upload OA version
Are you the author of this publication? Upload your Open Access version to Zenodo!
It’s fast and easy, just two clicks!