On the proof complexity of deep inference

P Bruscoli, Alessio Guglielmi

Research output: Contribution to journalArticlepeer-review

39 Citations (SciVal)
225 Downloads (Pure)


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 languageEnglish
Article number14
Number of pages34
JournalACM Transactions on Computational Logic
Issue number2
Publication statusPublished - Feb 2009


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


Dive into the research topics of 'On the proof complexity of deep inference'. Together they form a unique fingerprint.

Cite this