Improving proof compression by better controlling cut and sharing

Add to your list(s) Download to your calendar using vCal

• Paola Bruscoli (Bath)
• Friday 16 October 2015, 15:00-16:00
• CS 217.

If you have a question about this talk, please contact Neel Krishnaswami.

There are several mechanisms by which formal proofs can be compressed. Among them, the cut rule and sharing (or dagness) work by reusing parts of proofs as lemmata. In particular, the cut rule provides a powerful compression mechanism, but when analyticity is required (meaning that cut cannot be used) sharing alone does not generally achieve comparable compression.

In Gentzen’s proof theory the use of cut and sharing is limited by some heavy syntactic constraints. On the other hand, in the emerging deep-inference proof theory many of the syntactical constraints that limit cut and sharing have been lifted. This leads to greater freedom in exploiting sharing in absence of cut in order to compress proofs, while retaining analyticity.

I will talk about two results for propositional logic. I will firstly show that deep inference, in the absence of sharing and cut, provides an exponential speed-up over Gentzen. Then I will show how, in deep inference, sharing allows us to eliminate the cut in quasipolynomial time, which is a very surprising result given that, in Gentzen, cut-elimination is provably exponential even in the presence of sharing. This makes us favourably reconsider the cost of analyticity.

The second result is technical but the main idea is rather simple and hopefully enlightening, in particular about the role that sharing can play in future research. I will conclude by mentioning recent notable results in proof complexity and in the computational interpretation of proofs obtained by colleagues in Bath who built on that same idea.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• CS 217
• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.