变域上带计数量词的一阶模态逻辑的可判定片段
计算机科学中的逻辑
2018-12-18 v1
摘要
本文探讨了在常域和变域上，添加了计数量词的各种自然单变量一阶模态逻辑片段的计算复杂性。计数量词的添加为我们提供了一种丰富的语言，可用单个变量简洁地表达关于满足给定一阶性质的客体数量的陈述。对于最小一阶模态逻辑 QK 的单变量片段在常域和扩张/收缩域模型上的可满足性问题，当计数量词编码为二进制串时，给出了最优的 NExpTime 上界。对于计数量词编码为一元串或限制为有限量词集合的情况，表明在扩张域上的可满足性问题是 PSpace 完全的，而在收缩域上的问题则是 ExpTime 难的。
引用
@article{arxiv.1812.06341,
title = {Decidable fragments of first-order modal logics with counting quantifiers over varying domains},
author = {Christopher Hampson},
journal= {arXiv preprint arXiv:1812.06341},
year = {2018}
}