一句话：研究带计数量词的二变量一阶逻辑及分级模态逻辑中可定义与分离问题的可判定性和复杂度。
本文研究带计数量词的一阶逻辑片段 L 中的可定义性问题：给定 L-公式，能否用不含计数的某个 L 片段等价表达；以及更一般的分离问题：两个互斥的 L-公式能否在不含计数的 L 片段中被分离。作者证明，对于带计数量词的二变量一阶逻辑 FO^2，以及带逆、名义词和全称模态词的分级模态逻辑，分离问题是不可判定的。若去掉逆或名义词，分离问题的复杂度分别变为 coNExpTime 完全或 2ExpTime 完全，具体取决于是否含有全称模态词。相比之下，可定义性问题常常可在多项式时间内归约到 L 的有效性判定。作者还考察了均匀分离，并表明其行为通常与可定义性类似。
For fragments L of first-order logic (FO) with counting quantifiers, we consider the definability problem, which asks whether a given L -formula can be equivalently expressed by a formula in some fragment of L without counting, and the more general separation problem asking whether two mutually exclusive L-formulas can be separated in some counting-free fragment of L. We show that separation is undecidable for the two-variable fragment of FO extended with counting quantifiers and for the graded modal logic with inverse, nominals and universal modality. On the other hand, if inverse or nominals are dropped, separation becomes coNExpTime- or 2ExpTime-complete, depending on whether the universal modality is present. In contrast, definability can often be reduced in polynomial time to validity in L. We also consider uniform separation and show that it often behaves similarly to definability.
DOI 原文 ·
@inproceedings{paperbot8651,
title = {Separation and Definability in Fragments of Two-Variable First-Order Logic with Counting},
author = {Louwe Kuijer and Tony Tan and Frank Wolter and Michael Zakharyaschev},
booktitle = {LICS},
year = {2025},
doi = {10.1109/lics65433.2025.00032}
}