### Abstract

Language | English |
---|---|

Article number | 14 |

Number of pages | 34 |

Journal | ACM Transactions on Computational Logic |

Volume | 10 |

Issue number | 2 |

DOIs | |

Status | Published - Feb 2009 |

### Fingerprint

### 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.

Research output: Contribution to journal › Article

*ACM Transactions on Computational Logic*, vol. 10, no. 2, 14. DOI: 10.1145/1462179.1462186

}

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 -