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

TL;DR

This paper proves that reachability in alternating pushdown systems is decidable by establishing a cut-elimination theorem, and extends the system to be complete with respect to provability of configurations.

Contribution

It provides a new proof of decidability via cut-elimination and extends the system to be complete for all configurations.

Findings

Decidability of reachability in alternating pushdown systems

Cut-elimination theorem for natural-deduction inference systems

Extension to a complete system where every configuration is provable or refutable

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 $A$, either $A$ or $\neg A$ is provable.