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

Gilles Dowek, Ying Jiang

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-deduc…