Bruscoli, P. and Guglielmi, A., 2009. On the proof complexity of deep inference. ACM Transactions on Computational Logic, 10 (2), 14.
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.
|Item Type ||Articles|
|Creators||Bruscoli, P.and Guglielmi, A.|
|Uncontrolled Keywords||frege systems, calculus of structures, deep inference, analyticity, statman tautologies, theory|
|Departments||Faculty of Science > Computer Science|
|Publisher Statement||PrComplDI.pdf: © 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.|
Actions (login required)