BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Sonia Marin (University College London) DTSTART:20210203T140000Z DTEND:20210203T150000Z DTSTAMP:20260423T052454Z UID:OWLS/20 DESCRIPTION:Title: Fr om axioms to synthetic inference rules via focusing\nby Sonia Marin (U niversity College London) as part of Online Worldwide Seminar on Logic and Semantics (OWLS)\n\n\nAbstract\nFocusing is a general technique that was designed to improve proof search\, but has since become increasingly relev ant in structural proof theory. The essential idea is to identify and merg e the non-deterministic choices in a proof. A focused proof is then given by the alternation of phases where invertible rules are applied eagerly (b ottom-up) and phases where the other rules are confined and controlled. Th e focusing theorem\, which asserts the completeness of focused proofs\, de livers strong representational benefits. For instance\, by ignoring the in ternal structure of the phases one obtains a well-behaved notion of ‘syn thetic 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 bip oles\, giving a fresh view to an old problem: how to incorporate inference rules corresponding to axioms into proof systems for classical and intuit ionistic logics. As different synthetic inference rules can be produced fo r the same axiom\, we in fact unify and generalise previous approaches for transforming axioms into rules. This is joint work with Dale Miller\, Ela ine Pimentel\, and Marco Volpe.\n LOCATION:https://researchseminars.org/talk/OWLS/20/ END:VEVENT END:VCALENDAR