On the proof complexity of deep inference

Research output: Contribution to journalArticle

37 Citations (Scopus)
131 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 languageEnglish
Article number14
Number of pages34
JournalACM Transactions on Computational Logic
Volume10
Issue number2
DOIs
Publication statusPublished - Feb 2009

Keywords

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

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

  • Projects

  • Cite this