交替下推系统中可达性的割消去与可判定性
计算机科学中的逻辑
2014-10-31 v1
摘要
我们给出了交替下推系统（alternating pushdown systems）中可达性可判定性的新证明，表明它是某些自然演绎风格推理系统的割消去定理的直接推论。随后，我们展示了如何利用这一结果将交替下推系统扩展为一个完备系统，使得对于每个构型，或均可被证明。
引用
@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}
}