Cut-elimination and the decidability of reachability in alternating pushdown systems

Abstract : We propose a new approach to formalize alternating pushdown systems as natural-deduction style inference systems. In this approach, the decidability of reachability can be proved as a simple consequence of a cut-elimination theorem for the corresponding inference system. Then, we show how this result can be used to extend an alternating pushdown system into a complete system where, for every configuration $A$, either $A$ or $\neg A$ is provable. The key idea is that cut-elimination permits to build a system where a proposition of the form $\neg A$ has a co-inductive (hence possibly infinite) proof if and only if it has an inductive (hence finite) proof.
Type de document :
Pré-publication, Document de travail
2015
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01101835
Contributeur : Gilles Dowek <>
Soumis le : vendredi 30 janvier 2015 - 12:05:31
Dernière modification le : mardi 17 avril 2018 - 11:25:55
Document(s) archivé(s) le : vendredi 11 septembre 2015 - 06:27:51

Fichiers

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

Licence


Distributed under a Creative Commons Paternité - Partage selon les Conditions Initiales 4.0 International License

Identifiants

  • HAL Id : hal-01101835, version 1

Collections

Citation

Gilles Dowek, Ying Jiang. Cut-elimination and the decidability of reachability in alternating pushdown systems. 2015. 〈hal-01101835〉

Partager

Métriques

Consultations de la notice

129

Téléchargements de fichiers

81