Cut-elimination and the decidability of reachability in alternating pushdown systems
Logic in Computer Science
2014-10-31 v1
Abstract
We give a new proof of the decidability of reachability in alternating pushdown systems, showing that it is a simple consequence of a cut-elimination theorem for some natural-deduction style inference systems. Then, we show how this result can be used to extend an alternating pushdown system into a complete system where for every configuration , either or is provable.
Keywords
Cite
@article{arxiv.1410.8470,
title = {Cut-elimination and the decidability of reachability in alternating pushdown systems},
author = {Gilles Dowek and Ying Jiang},
journal= {arXiv preprint arXiv:1410.8470},
year = {2014}
}