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

2014/10/30 by Dowek, Gilles, Jiang, Ying
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1410.8470

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 ¬ A is provable.

Related

• Reachability in Trace-Pushdown Systems
• On Boundedness Problems for Pushdown Vector Addition Systems
• Reachability analysis of first-order definable pushdown systems
• The theory of reachability in trace-pushdown systems
• On the convergence of reduction-based and model-based methods in proof theory