Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/hal-00772502
Contributor : Dale Miller <>
Submitted on : Thursday, January 10, 2013 - 3:42:08 PM
Last modification on : Thursday, March 5, 2020 - 6:27:36 PM
Long-term archiving on: : Thursday, April 11, 2013 - 4:06:39 AM

File

baelde09tableaux.pdf
Files produced by the author(s)

Identifiers

  • 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. ⟨hal-00772502⟩

Share

Metrics

Record views

184

Files downloads

267