![]() |
![]() |
University of Birmingham > Talks@bham > Theoretical computer science seminar > Improving proof compression by better controlling cut and sharing
Improving proof compression by better controlling cut and sharingAdd to your list(s) Download to your calendar using vCal
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:
Note that ex-directory lists are not shown. |
Other listsBiosciences seminars Human Computer Interaction seminars Condensed Matter Group MeetingsOther talksSignatures of structural criticality and universality in the cellular anatomy of the brain The percolating cluster is invisible to image recognition with deep learning [Friday seminar]: Irradiated brown dwarfs in the desert Provably Convergent Plug-and-Play Quasi-Newton Methods for Imaging Inverse Problems |