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 …

Characterising aspects of proof compression

Anupam Das. Note. PDF

We consider deep inference proof formalisms, which are flexible enough to embed many widely used proof systems, and construe compression mechanisms `cut’ and `dag’ in a way that is independent of any particular proof system, but in a way that nonetheless has the same effect from the point of view of proof complexity. The main …

On the proof complexity of cut-free bounded deep inference

Anupam Das. In proceedings of Tableaux '11. DOI PDF

It has recently been shown that cut-free deep inference systems exhibit an exponential speed-up over cut-free sequent systems, in terms of proof size. While this is good for proof complexity, there remains the problem of typically high proof search non-determinism induced by the deep inference methodology: the higher the depth of inference, the higher the …