seminaire PPS *mardi* 30/3, 14h, salle 0C02

Chers tous,
cette semaine, le seminaire PPS est

le *mardi* 30 Mars, 14h (en salle 0C02):

David Baelde (University of Minnesota, USA)

Finite automata and regular fixed point formulas in muMALL

http://www.pps.jussieu.fr/seminaire/

Abstract:
We present muMALL, an extension of multiplicative additive linear logic
with least and greatest fixed points, and illustrate its expressiveness
through the model-checking problem of non-deterministic finite automata
inclusion.

We consider encoding automata as least fixed points in muMALL, and use its
general induction scheme to reason about them. We provide a coinductive
characterization of inclusion that yields a natural bridge to
proof-theory. This yields a completeness theorem, but can also be
generalized to the fragment of "regular formulas", obtaining new insights
about inductive theorem proving and cyclic proofs in particular.