On the proof complexity of deep inference

P Bruscoli, Alessio Guglielmi

Research output: Contribution to journalArticle

  • 33 Citations

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.
LanguageEnglish
Article number14
Number of pages34
JournalACM Transactions on Computational Logic
Volume10
Issue number2
DOIs
StatusPublished - Feb 2009

Fingerprint

Proof Complexity
Proof System
Substitution reactions
Substitution
Speedup

Keywords

  • Frege systems
  • calculus of structures
  • deep inference
  • Analyticity
  • Statman tautologies
  • Theory

Cite this

On the proof complexity of deep inference. / Bruscoli, P; Guglielmi, Alessio.

In: ACM Transactions on Computational Logic, Vol. 10, No. 2, 14, 02.2009.

Research output: Contribution to journalArticle

@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 = "2",
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

VL - 10

JO - ACM Transactions on Computational Logic

T2 - ACM Transactions on Computational Logic

JF - ACM Transactions on Computational Logic

SN - 1529-3785

IS - 2

M1 - 14

ER -