From axioms to synthetic inference rules via focusing

Abstract: 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. This is joint work with Dale Miller, Elaine Pimentel, and Marco Volpe.

formal languages and automata theorylogic in computer sciencelogic

Audience: researchers in the discipline

Online Worldwide Seminar on Logic and Semantics (OWLS)

Series comments: The Online Worldwide Seminar on Logic and Semantics is a new series of research talks, highlighting the most exciting recent work in the international computer science logic community. The scope of the seminar series is roughly that of the major computer science logic conferences such as LICS, ICALP and FSCD. It takes place on most Wednesdays, with a focus every other week on the work of young researchers.

In this time of restricted international travel, a key aim of this series is to provide a forum for the informal discussion and social interaction that is so important for the progress of science. To facilitate this, the seminar incorporates in virtual form a number of features more normally associated with physical meetings.

For more details, please visit the homepage. There is no need to register for the talks, just show up.