关于最短发展的注记
计算机科学中的逻辑
2015-07-01 v2
摘要
De Vrijer 曾提出有限发展定理的证明，该证明不仅表明所有发展都是有限的，还给出了计算最长发展的有效归约策略以及计算其长度的简单公式。我们表明，通过将一种相当简单且直观的对偶原理应用于 de Vrijer 的方法，可以得到一个证明，表明某些发展是有限的，并且该证明还能给出计算最短发展的有效归约策略以及计算其长度的简单公式。这种对偶性在一般的-归约中不成立。我们的结果简化了 Khasidashvili 先前的工作。
引用
@article{arxiv.0708.0200,
title = {A Note on Shortest Developments},
author = {Morten Heine Sørensen},
journal= {arXiv preprint arXiv:0708.0200},
year = {2015}
}