On the Proof Theory of Regular Fixed Points

Abstract : 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.
Type de document :
Communication dans un congrès
Automated Reasoning with Analytic Tableaux and Related Methods, 18th International Conference, TABLEAUX 2009, Jul 2009, Oslo, Norway. 2009
Liste complète des métadonnées

Littérature citée [14 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00772502
Contributeur : Dale Miller <>
Soumis le : jeudi 10 janvier 2013 - 15:42:08
Dernière modification le : mercredi 25 avril 2018 - 10:45:20
Document(s) archivé(s) le : jeudi 11 avril 2013 - 04:06:39

Fichier

baelde09tableaux.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00772502, version 1

Collections

Citation

David Baelde. On the Proof Theory of Regular Fixed Points. Automated Reasoning with Analytic Tableaux and Related Methods, 18th International Conference, TABLEAUX 2009, Jul 2009, Oslo, Norway. 2009. 〈hal-00772502〉

Partager

Métriques

Consultations de la notice

109

Téléchargements de fichiers

62