Complexity of deep inference via atomic flows

Abstract

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