Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

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

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.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [11 references]  Display  Hide  Download
Contributor : Gilles Dowek <>
Submitted on : Friday, January 30, 2015 - 12:05:31 PM
Last modification on : Friday, May 25, 2018 - 12:02:06 PM
Long-term archiving on: : Friday, September 11, 2015 - 6:27:51 AM


Files produced by the author(s)


Distributed under a Creative Commons Attribution - ShareAlike 4.0 International License


  • HAL Id : hal-01101835, version 1



Gilles Dowek, Ying Jiang. Cut-elimination and the decidability of reachability in alternating pushdown systems. 2015. ⟨hal-01101835⟩



Record views


Files downloads