Complexity of deep inference via atomic flows

Anupam Das. In proceedings of Turing Centenary Conference: CiE 2012. DOI PDF

We consider the fragment of deep inference free of compression mechanisms and compare its proof complexity to other systems, utilising ‘atomic flows’ to examine size of proofs. Results include a simulation of Resolution and dag-like cut-free Gentzen, as well as a separation from bounded-depth Frege.

NB: There are errors in some statements and proofs of this article that have been amended in the long version, On the relative proof complexity of deep inference via atomic flows.