关于扩展非一元计数量词的Presburger算术
摘要：整数加法的一阶逻辑,具有模余计数、门槛计数和精确计数量化符号,都应用于变量元组(这里,余数给定为项,而模数和门槛则明确给出)。我们的主要结果表明,这种逻辑的满足性在双指数空间中是可判定的。如果只允许门槛计数和精确计数量化符号,我们证明了交替双指数时间和线性个交替的上限。后者的结果几乎与Berman关于没有计数量化符号的一阶逻辑的精确复杂度相匹配。 为了得到这些结果,我们首先将门槛计数和精确计数量化符号在多项式时间内转换为经典一阶逻辑(这已经证明了第二个结果)。为了处理剩余的关于元组的模余计数量化符号,我们首先将它们在双指数时间内减少到元素的模余计数量化符号。对于这些量化符号,我们提供了一个类似于Reddy和Loveland关于一阶逻辑的量词消除过程并分析了在这个过程中出现的系数、常数和模数的增长。这样得到的边界可以将原始公式中的量化限制为具有有限大小的整数,这样就得到了上面提到的第一个结果。 我们的逻辑与Chistikov等人在2022年考虑的逻辑不可比较。他们允许更一般的计数操作在量化符号中,但只有一元的量化符号。从一元到非一元量化符号的转换是非平凡的,因为例如H"artig量化符号的非一元版本会导致一个不可判定的理论。
作者：Peter Habermehl, Dietrich Kuske
论文ID：2204.03903
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-12