From axioms to synthetic inference rules via focusing

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

• Sonia Marin (University of Birmingham)
• Friday 12 November 2021, 14:00-15:00
• LG23, SoCS and Zoom (see abstract for link).

If you have a question about this talk, please contact Anupam Das.

Focusing is a general technique that was designed to improve proof search, but has since become increasingly relevant in structural proof theory. The essential idea is to identify and merge the non-deterministic choices in a proof. A focused proof is then given by the alternation of phases where invertible rules are applied eagerly (bottom-up) and phases where the other rules are confined and controlled. The focusing theorem, which asserts the completeness of focused proofs, delivers strong representational benefits. For instance, by ignoring the internal structure of the phases one obtains a well-behaved notion of ‘synthetic rule’ (e.g. they commute with cut-reduction steps).

In this talk, we will present a careful study of a family of synthetic rules, the bipoles, giving a fresh view to an old problem: how to incorporate inference rules corresponding to axioms into proof systems for classical and intuitionistic logics. As different synthetic inference rules can be produced for the same axiom, we in fact unify and generalise previous approaches for transforming axioms into rules.

=== Zoom Details ===

Topic: Sonia Marin – Theory Seminar, 12/11/2021 Time: Nov 12, 2021 01:45 PM London

Join Zoom Meeting https://bham-ac-uk.zoom.us/j/81701087797?pwd=cE1sM1Evbm83bjVMVXdXL1RwWUZMUT09

Meeting ID: 817 0108 7797 Passcode: 369578 One tap mobile +441314601196,,81701087797#,,,,369578# United Kingdom +442034815237,,81701087797#,,,,369578# United Kingdom

Dial by your location +44 131 460 1196 United Kingdom +44 203 481 5237 United Kingdom +44 203 481 5240 United Kingdom +44 203 901 7895 United Kingdom +44 208 080 6591 United Kingdom +44 208 080 6592 United Kingdom +44 330 088 5830 United Kingdom Meeting ID: 817 0108 7797 Passcode: 369578 Find your local number: https://bham-ac-uk.zoom.us/u/kcJUZAHrfR

Join by SIP 81701087797@zoomcrc.com

Join by H.323 162.255.37.11 (US West) 162.255.36.11 (US East) 115.114.131.7 (India Mumbai) 115.114.115.7 (India Hyderabad) 213.19.144.110 (Amsterdam Netherlands) 213.244.140.110 (Germany) 103.122.166.55 (Australia Sydney) 103.122.167.55 (Australia Melbourne) 149.137.40.110 (Singapore) 64.211.144.160 (Brazil) 149.137.68.253 (Mexico) 69.174.57.160 (Canada Toronto) 65.39.152.160 (Canada Vancouver) 207.226.132.110 (Japan Tokyo) 149.137.24.110 (Japan Osaka) Meeting ID: 817 0108 7797 Passcode: 369578

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

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• LG23, SoCS and Zoom (see abstract for link)
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.