前缀与后缀逻辑在同质性假设下为初等可判定
计算机科学中的逻辑
2023-04-25 v1
摘要
本文研究在同质性假设下逻辑 BE 的有限可满足性问题。BE 是 Halpern 和 Shoham 区间时序逻辑的基石，其模态算子对应于区间上的前缀（亦称“Begins”）与后缀（亦称“Ends”）关系。在复杂度方面，BE 介于“Chop 逻辑 C”（其可满足性问题已知为非初等）与子区间（亦称“During”）关系的 PSPACE 完全区间逻辑 D 之间。BE 已被证明为 EXPSPACE 困难，且唯一已知的可满足性过程是原始递归的，但非初等。我们的贡献在于通过证明 BE 的可满足性问题是 EXPSPACE 完全的，从而收紧了其复杂度界限。为此，我们设计了一种具有有界多层嵌套模态的等可满足范式。该规范化技术类似于 Scott 的量词消去，但由于同质性假设所施加的限制，其实现过程要复杂得多。
引用
@article{arxiv.2304.11483,
title = {The Logic of Prefixes and Suffixes is Elementary under Homogeneity},
author = {Dario Della Monica and Angelo Montanari and Gabriele Puppis and Pietro Sala},
journal= {arXiv preprint arXiv:2304.11483},
year = {2023}
}