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.
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
