LSV Seminar
The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Past Seminars
Regular fixed points, non-deterministic cyclic proofs and finite automata
- Date
- Wednesday, July 15 2009 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- David Baelde (LIX, École Polytechnique, Palaiseau)
We consider encoding finite automata as least fixed points in a proof-theoretical framework equipped with a general induction scheme, and study automata inclusion in that setting. We provide a coinductive characterization of inclusion that yields a natural bridge to proof-theory. This leads us to generalize these observations to regular formulas, obtaining new insights about inductive theorem proving and cyclic proofs in particular.