动作逻辑是不可判定的
计算机科学中的逻辑
2019-12-25 v1 逻辑
摘要
动作逻辑是剩余Kleene格的代数逻辑(不等价理论)。该逻辑涉及Kleene星,由归纳模式公理化。对于使用ω-规则(无穷动作逻辑)的更强系统,Buszkowski与Palka(2007)已证明其为Π₁⁰-完备(即不可判定)。动作逻辑自身的可判定性是D. Kozen于1994年提出的开放问题。本文中,我们证明其不可判定,更确切地说,为Σ₁⁰-完备。我们还对动作逻辑与无穷动作逻辑之间所有递归可枚举逻辑、对这些逻辑仅含两种格(加性)连接词之一的片段、以及扩展以分配律的动作逻辑,证明了相同的复杂度结果。
引用
@article{arxiv.1912.11273,
title = {Action Logic is Undecidable},
author = {Stepan Kuznetsov},
journal= {arXiv preprint arXiv:1912.11273},
year = {2019}
}
备注
33 pages