On the proof complexity of deep inference

P Bruscoli; Alessio Guglielmi

doi:10.1145/1462179.1462186

On the proof complexity of deep inference

P Bruscoli, Alessio Guglielmi

Research output: Contribution to journal › Article › peer-review

41 Citations (SciVal)

255 Downloads (Pure)

Abstract

We obtain two results about the proof complexity of deep inference: (1) Deep-inference proof systems are as powerful as Frege ones, even when both are extended with the Tseitin extension rule or with the substitution rule; (2) there are analytic deep-inference proof systems that exhibit an exponential speedup over analytic Gentzen proof systems that they polynomially simulate.

Original language	English
Article number	14
Number of pages	34
Journal	ACM Transactions on Computational Logic
Volume	10
Issue number	2
DOIs	https://doi.org/10.1145/1462179.1462186
Publication status	Published - Feb 2009

Keywords

Frege systems
calculus of structures
deep inference
Analyticity
Statman tautologies
Theory

Access to Document

10.1145/1462179.1462186

Author's accepted version
© ACM, 2009. This is the authors’ version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACM Transactions on Computational Logic 10 (2:14) 2009, pp. 1–34, http://doi.acm.org/10.1145/1462179.1462186.
Accepted author manuscript, 331 KB

Cite this

@article{4abd5e89ff9c4dacba8ab802d01deb80,

title = "On the proof complexity of deep inference",

abstract = "We obtain two results about the proof complexity of deep inference: (1) Deep-inference proof systems are as powerful as Frege ones, even when both are extended with the Tseitin extension rule or with the substitution rule; (2) there are analytic deep-inference proof systems that exhibit an exponential speedup over analytic Gentzen proof systems that they polynomially simulate.",

keywords = "Frege systems, calculus of structures, deep inference, Analyticity, Statman tautologies, Theory",

author = "P Bruscoli and Alessio Guglielmi",

year = "2009",

month = feb,

doi = "10.1145/1462179.1462186",

language = "English",

volume = "10",

journal = "ACM Transactions on Computational Logic",

issn = "1529-3785",

publisher = "Association for Computing Machinery",

number = "2",

}

TY - JOUR

T1 - On the proof complexity of deep inference

AU - Bruscoli, P

AU - Guglielmi, Alessio

PY - 2009/2

Y1 - 2009/2

N2 - We obtain two results about the proof complexity of deep inference: (1) Deep-inference proof systems are as powerful as Frege ones, even when both are extended with the Tseitin extension rule or with the substitution rule; (2) there are analytic deep-inference proof systems that exhibit an exponential speedup over analytic Gentzen proof systems that they polynomially simulate.

AB - We obtain two results about the proof complexity of deep inference: (1) Deep-inference proof systems are as powerful as Frege ones, even when both are extended with the Tseitin extension rule or with the substitution rule; (2) there are analytic deep-inference proof systems that exhibit an exponential speedup over analytic Gentzen proof systems that they polynomially simulate.

KW - Frege systems

KW - calculus of structures

KW - deep inference

KW - Analyticity

KW - Statman tautologies

KW - Theory

UR - http://www.scopus.com/inward/record.url?scp=62149132432&partnerID=8YFLogxK

UR - http://dx.doi.org/10.1145/1462179.1462186

U2 - 10.1145/1462179.1462186

DO - 10.1145/1462179.1462186

M3 - Article

SN - 1529-3785

VL - 10

JO - ACM Transactions on Computational Logic

JF - ACM Transactions on Computational Logic

IS - 2

M1 - 14

ER -

On the proof complexity of deep inference

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

COMPLEXITY AND NON-DETERMINISM IN DEEP INFERENCE

Cite this

On the proof complexity of deep inference

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Projects

COMPLEXITY AND NON-DETERMINISM IN DEEP INFERENCE

Cite this