The Logic of Counting Query Answers
我们考虑有限结构上一阶公式的答案个数的计数问题。我们提出并研究了一阶逻辑的扩展，在这种计算问题的算法可以自然和方便地表示，在意义上说，是精确的，这是出于希望了解听话的情况下的计数问题。
2017-04-20 cs.CC cs.LO
Modulo-Counting First-Order Logic on Bounded Expansion Classes
我们证明了，在有界扩展类，每一个一阶公式与模计数是等价的，在线性时间可计算的一元扩展，一个存在的一阶公式。因此，我们得出，有界扩展类，一阶转换与模计数具有相同的编码能力作为存在的一阶转换。此外，模计数的一阶模型检验和计算的规模可定义在模计数的一阶逻辑可以实现在线性时间上有界的扩展类。作为应用，我们证明了一个图类具有结构有界扩张当且仅当它是一个有界扩张类中的一个有界深度顶点子式类。我们还展示了如何我们的结果可以用来实现快速矩阵演算有限域上的有界扩展矩阵。
2023-03-23 cs.LO math.CO
Counting of Teams in First-Order Team Logics
本文研究了从#P到# $\cdot$ NP范围内的计数复杂性类的描述复杂性。Fagin用存在二阶逻辑刻画NP的一个推论是，#P可以逻辑上描述为一阶公式中计算满足对自由关系变量的赋值的函数类。在本文中，我们将这项研究扩展到类以外的#P和扩展的一阶逻辑与团队语义。这些团队为基础的逻辑是密切相关的存在的二阶逻辑和它的片段，因此我们的结果也揭示了复杂的计数扩展的FO塔斯基的语义。我们的结果表明，类# $\cdot$ NP可以用独立逻辑和存在二阶逻辑进行逻辑刻画，而依赖逻辑和包含逻辑分别产生了类# $\cdot$ NP和类#P的子类.我们的主要技术结果表明，单调布尔$Σ_1$公式满足赋值的计数问题是# $\cdot$ NP-完全的，对于依赖逻辑生成的函数类也是完全的.
2020-12-29 cs.CC cs.LO
Two variable logic with ultimately periodic counting
本文研究带最终周期计数量词的二变量逻辑，证明其可满足性与有限可满足性可判定，并证明句子谱可在Presburger算术中定义，同时改进了双正则图方法。
2024-04-03 cs.LO math.CO
Interleaving Logic and Counting
本文研究自然语言推理中逻辑与计数的结合，通过带计数的单子一阶逻辑及其强化形式，分析可定义性、公理化与可判定性，并联系语言量词和认知科学。
2025-07-07 cs.CL cs.LO math.LO
A Game for Counting Logic Formula Size and an Application to Linear Orders
本文提出一种 EF 博弈来刻画有界变量计数逻辑的公式大小，并利用它将线性序的公式大小下界从 3 变量一阶逻辑扩展到 3 变量计数逻辑，首次给出计数逻辑的公式大小下界。
2025-05-22 cs.LO
The Complexity of Counting Models of Linear-time Temporal Logic
我们确定的复杂性计数模型的有界大小的规格表示的线性时间时序逻辑。如果边界是以一元形式给出的，那么计算单词模型是P-完全的;如果边界是以二进制形式给出的，那么计算非确定性多项式空间图灵机的运行次数是一样困难的。如果边界是以一元形式给出的，那么对树模型进行计数就像对非确定性指数时间图灵机的接受运行进行计数一样困难。对于边界的二进制编码，这个问题至少和计算非确定性指数空间图灵机的接受次数一样困难。另一方面，它并不比计数非确定性双指数时间图灵机的接受运行更难。
2014-10-06 cs.CC cs.LO
Model-checking Counting Temporal Logics on Flat Structures
我们研究了几个扩展的线性时间和计算树的时间逻辑与量词，允许计数经常某些属性举行。对于大多数这些扩展，模型检验问题是不可判定的，但我们表明，可判定性可以恢复考虑平坦的Kripke结构，每个状态属于最多一个简单的循环。大多数决策程序是基于（平面）计数器系统的结果，其中计数器用于实现计数运算符的评估。
2017-06-26 cs.LO
When Do You Start Counting? Revisiting Counting and Pnueli Modalities in Timed Logics
本文证明在时序逻辑中，[0, b>区间的计数能力与任意区间<a, b>等价，并给出一般性质在EMITL中仅用[0, b>的可表达性结果。
2024-10-01 cs.LO
Decidable fragments of first-order modal logics with counting quantifiers over varying domains
本文探讨了在常数域和变域上，一阶模态逻辑的各种自然单变量片段加上计数量词的计算复杂性。计数量词的加入为我们提供了一种丰富的语言，可以用它来简洁地表达关于满足给定一阶性质的对象的数量的陈述，使用单个变量。最佳NExpTime上界提供的最小一阶模态逻辑QK的一个变量片段的可满足性问题，在恒定和扩大/减少领域模型，计数量词被编码为二进制字符串。对于计数量词被编码为一元字符串的情况下，或被限制为一个有限的量词集，它表明，可满足性问题的扩展域是PSpace完全的，而减少域的问题是ExpTime-hard。
2018-12-15 cs.LO
Witnessed Symmetric Choice and Interpretations in Fixed-Point Logic with Counting
RWTH Aachen University（亚琛工业大学）
研究固定点逻辑加计数（IFPC）中见证对称选择（IFPC+WSC）与解释操作符（IFPC+WSC+I）的扩展，探讨其表达能力及与计数的关系。
2026-04-13 cs.LO math.LO
On Presburger arithmetic extended with non-unary counting quantifiers
研究扩展了非一元计数量词的Presburger算术，通过量词消去与归约技术证明其满足性在两重指数空间内可判定，并给出不同量词组合下的计算复杂度上界。
2023-07-11 cs.LO
Extending Two-Variable Logic on Trees
最近证明了在树上解释的一阶逻辑的两个变量片段的有限可满足性问题是ExpSpace完备的。我们考虑这个逻辑的两个扩展。我们发现，添加额外的二进制符号或计数量词的逻辑不影响有限可满足性问题的复杂性。然而，结合两个扩展并添加二进制符号和计数量词会导致这种复杂性的爆炸。我们还比较了两个变量的片段的表达能力，其扩展与计数量词的树木。事实证明，这两种逻辑具有同样的表达能力，尽管在无序树的限制情况下，计数量词确实增加了表达能力。
2016-11-24 cs.LO
Maximum Matching and Linear Programming in Fixed-Point Logic with Counting
我们建立了一些自然多项式时间问题的可表达性与计数定点逻辑（FPC）。特别是，我们表明，在一个图中的最大匹配的大小是可定义的FPC。这解决了Blass、Gurevich和Shelah首先提出的一个开放性问题，他们询问是否可以用更强大的无选择多项式时间的形式主义来确定一般图中完美匹配的存在。我们的结果是建立在椭圆形方法求解线性规划可以实现在FPC。这使我们能够证明，线性规划可以在FPC中优化，如果相应的分离预言问题可以在FPC中定义。在为最大匹配问题定义合适的分离预言机的过程中，我们给出了容量限制图中定义最大流和标准最小割的FPC公式。
2013-04-25 cs.CC cs.DM cs.LO
Arithmetic, First-Order Logic, and Counting Quantifiers
本文给出了一个全面的概述，什么是已知的一阶逻辑计数量词和算术谓词。作为一个主要定理，我们证明了Presburger算术在一元计数量词下是封闭的。确切地说，这意味着对于每个一阶公式phi（y，z_1，.，z_k）上存在一阶公式Psi（x，z_1，...，z_k），其在结构<Nat，<，+>上（分别在该结构的初始段上）表示变量x被变量y的可能解释的数量精确地解释，对于该变量y，公式phi（y，z_1，...，z_k）满足。应用这一定理，我们得到一个简单的证明鲁尔的结果，可达性（同样，连接）在有限的图形是不可表达的一阶逻辑与一元计数量词和加法。此外，关于Presburger算法的上述结果有助于表明Crane Beach猜想的一个特定版本的失败。
2002-11-19 cs.LO
Separation and Definability in Fragments of Two-Variable First-Order Logic with Counting
本文研究了带计数的两变量一阶逻辑片段中的可定义性与分离问题，证明了在包含逆算子和名义时分离问题不可判定，而去除这些特征时其复杂度降为coNExpTime或2ExpTime完全，并指出可定义性问题通常可多项式归约至有效性问题。
2025-08-15 cs.LO
Complexity of Clique-Guarded First-Order Logic with Counting
Humboldt-Universität zu Berlin（柏林洪堡大学）
引入团保护的一阶计数逻辑(cgFOC)，证明其在无稠密关系结构类上的VC维和计数项图维数的可计算上界，并给出局部有界扩张类上的查询、枚举和PAC学习元定理。
2026-06-24 cs.LO
Counting Like Transformers: Compiling Temporal Counting Logic Into Softmax Transformers
University of Notre Dame（圣母大学）
该研究提出时序计数逻辑 K_t[#] 与 C-RASP，并证明二者等价且可编译为未来掩码软注意力 Transformer，从而给出其无界输入下表达能力的已知最佳下界。
2024-12-01 cs.CL cs.FL cs.LG
Weighted model counting beyond two-variable logic
最近van den Broeck等人证明了二元逻辑FO 2语句的对称加权一阶模型计数问题（WFOMC）是多项式时间的，而对于某些FO 3-语句则是Sharp-P_1完全的.我们延长FO 2的结果在两个独立的方向：句子的形式“phi和\forall \exists^= 1 psi”与phi和psi在FO 2，和句子制定的统一的一维片段FO，最近推出的扩展双变量逻辑的能力，以处理关系符号的所有arities。注意，前者用函数关系符号推广了FO 2的扩展。根据WFOMC是多项式时间还是Sharp-P_1完备，我们给出了一阶前缀类的完全分类。
2018-04-26 cs.LO
Two-variable Logic with Counting and a Linear Order
研究了在线性序结构上用计数量词（C2）扩展的一阶逻辑二元片段的有限可满足性问题。我们表明，问题是不可判定的情况下，两个线性订单（在存在两个其他二进制符号）。在一个线性顺序的情况下，它是NEXPTIME-完全的，即使在后继关系的存在。令人惊讶的是，当我们再增加一个二进制符号时，问题的复杂性就会爆炸：具有一个线性顺序并且存在其他二进制谓词符号的C2在初等约简下等价于多计数器自动机的空问题。
2016-06-22 cs.LO
Metric Temporal Logic with Counting
在资源受限的实时的计算规范中，能够计算在指定时间间隔内事件发生的次数是非常有用的。在本文中，我们研究了度量时态逻辑（$\mathsf{MTL}$）的扩展与两个不同的计数模态称为$\mathsf{C}$和$\mathsf{UT}$（直到与阈值），这提高了表达能力的$\mathsf{MTL}$在正交的方式。我们仅限于有限时间词上逐点解释的$\mathsf{MTL}$的未来片段。我们提供了一个全面的研究的表达能力的逻辑$\mathsf{CTMTL}$和它的片段使用EF游戏扩展与适当的计数移动的技术。最后，作为我们的主要结果，我们建立了$\mathsf{CTMTL}$的可判定性，给出了从$\mathsf{CTMTL}$到$\mathsf{MTL}$的等价约简。这种减少提供了一个使用时间预测的例子，上面介绍了过采样来证明可判定性。我们的约简也意味着用$\mathsf{C}$和$\mathsf{UT}$模态扩展的$\mathsf{MITL}$是基本可判定的。
2015-12-30 cs.LO
Deductive Systems for Logic Programs with Counting
University of Nebraska Omaha（内布拉斯加大学奥马哈分校）；University of Texas at Austin（德克萨斯大学奥斯汀分校）
本文提出了一种扩展的演绎系统，用于证明包含计数聚合的逻辑程序之间的强等价性。
2025-11-24 cs.AI cs.LO
Approximate Evaluation of First-Order Counting Queries
Kuske和Schweikardt引入了非常有表现力的一阶计数逻辑FOC（P）来建模具有计数操作的数据库查询。他们证明了在有界度的图上存在一个有效的模型检查算法，而Grohe和Schweikardt证明了在有界深度的树上可能不存在这样的算法。我们分析这个逻辑的片段FO（{>0}）。虽然我们删除了例如两个非原子计数项之间的减法和比较，但这种逻辑仍然非常有表现力：我们允许计数项和任意大的数字之间的嵌套计数和比较。我们的主要结果是一个近似计划的模型检测问题FO（{>0}），运行在线性FPT时间上的结构有界扩展。这个方案要么给出正确答案，要么说“我不知道。“后一个答案只能在公式的数字符号的小扰动可以使它既满意又不满意的情况下给出。这是通过证明精确地解决FO（{>0}）的模型检查问题在有界深度的树上已经很难，并且仅仅稍微增加FO（{>0}）的表达能力就很难在树上近似来补充的。
2020-10-28 cs.DM cs.LO
Counting Distinctions: On the Conceptual Foundations of Shannon's Information Theory
范畴逻辑已经表明，现代逻辑本质上是子集逻辑（或“子子集”）。划分是子集的对偶，因此存在划分的对偶逻辑，其中“区别”[来自全域U的不同元素（u，u '）的有序对]是“元素”的对偶。在子集中的元素类似于U上的划分p，从而进行区分，即，如果u和u'在p的不同块中。子集逻辑通过将（拉普拉斯）概率作为有限论域的每个子集事件的归一化大小而导致有限概率论。划分逻辑中的类似步骤是将划分的区分数分配给划分，该区分数由来自有限论域的有序对|UxU|的总数归一化。这就产生了划分的“逻辑熵”概念和“逻辑信息论”。“逻辑理论直接计算分区中的（标准化）区别数量，而香农的理论给出了做出这些相同区别所需的二进制分区的平均数量。因此，逻辑理论被看作是为香农的理论提供了一个概念性的基础上的逻辑概念的“区别”。“（即将发表于《综合》）
2009-02-11 cs.IT cs.LO math.IT
Constant time testability of first-order logic with modulo counting on finitary graphs
University of Bamberg（班贝格大学）
本文研究了在有界度模型下，常数运行时间的属性测试算法元定理。针对有界组件大小的图类，证明了一阶逻辑带模计数（FOMOD）的常数时间可测试性，并引入了数论中的'补充分条件'来推断全局信息。
2026-05-11 cs.LO math.LO
One-Variable Logic Meets Presburger Arithmetic
我们考虑一阶逻辑的一个变量片段扩展Presburger约束。该逻辑的设计方式是，它包含了以前已知的片段扩展计数，模计数或基数比较，并结合他们的表达能力。我们证明了NP-完全的逻辑，提出了一个最佳的算法来解决其有限的可满足性问题。
2019-09-16 cs.LO
Graded modal logic and counting message passing automata
本研究探讨分级多模态逻辑与计数消息传递自动机的关联，提出分级多模态类型与推广Weisfeiler-Leman算法的自动机，证明二者识别模型类的等价性，并给出带Härtig量词和最大不动点的一阶逻辑执行该算法的方法。
2024-01-26 cs.DC cs.LO
Counting Homomorphisms from Hypergraphs of Bounded Generalised Hypertree Width: A Logical Characterisation
本研究提出双类型计数逻辑$GC^k$，证明其等价于广义超树宽度至多k的超图类上的同态不可区分性，将图领域的相关经典结论推广至超图场景。
2023-08-21 cs.LO
Learning Aggregate Queries Defined by First-Order Logic with Counting
本文研究超越布尔分类的多类整数分类问题，提出在拟线性时间内构建索引结构，实现FOC1可定义整数值分类器的高效学习。
2024-11-06 cs.DB cs.LO
Undecidable propositional bimodal logics and one-variable first-order linear temporal logics with counting
一阶时态逻辑因其糟糕的计算行为而臭名昭著。众所周知，即使是两个变量的一元片段在各种线性时间线上也是高度不可判定的，并且在分支时间上，即使是一个变量的片段也可能是不可判定的。然而，已经有几个试图找到良好的一阶时序逻辑和相关的时序描述逻辑的片段，主要是通过限制可用的量词模式，或考虑子布尔语言。在这里，我们分析看似“温和”的扩展可判定的一个变量的片段与计数能力，解释模型与恒定，减少，扩大一阶域。我们表明，在大多数类的线性订单，这些逻辑是（有时高度）不可判定的，即使没有常数和函数符号，并与唯一的时间运营商“最终”。我们建立连接与双峰逻辑在二维产品结构具有线性和“差异”（不等式）组件的关系，并证明我们的结果在此双峰设置。我们给出了一个普遍的结果，即许多具有可交换线性和差分关系的双峰模型的可满足性是不可判定的。作为一个副产品，我们还获得了新的例子，但Kripke不完全双峰逻辑的axiomatisable。我们的结果推广了双峰逻辑在两个线性关系的乘积上的类似下界，并且我们的证明方法与这些结果的证明有很大的不同。与以前的证明，第一个“对角编码”的无限网格，然后使用减少平铺或图灵机的问题，在这里，我们直接使用的网格状结构的产品框架，并获得undecidability减少计数器（明斯基）机的问题。
2015-06-08 cs.LO
Walk refinement, walk logic, and the iteration number of the Weisfeiler-Leman algorithm
我们表明，2维Weisfeiler-Leman算法稳定n顶点图后，最多O（n log n）迭代。这意味着，如果这样的图是可区分的3-变量一阶逻辑计数，那么他们也可以区分在这个逻辑的量词深度公式最多O（n log n）。为此，我们利用一个新的细化计数行走的基础上，并认为它的迭代次数不同于经典的Weisfeiler-Leman细化最多的对数因子。然后，我们证明匹配的线性上界和下界的行走细化的迭代次数。这是通过利用半单矩阵代数的性质来实现的代数方法。我们还定义了一个行走逻辑和一个双射行走卵石游戏，它们精确地对应于新的行走细化。
2019-05-09 cs.DM cs.LO math.CO
Strong Equivalence of Logic Programs with Counting
在答案集编程中，如果两组规则在任何上下文中具有相同的含义，则它们被认为是强等价的。在某些情况下，可以通过从另一个程序的规则中推导出每个程序的规则来建立接地外国佬的输入语言的程序的强等价性。这种证明的可能性已经在该语言的一个子集上得到了证明，该子集包括比较、算术运算和简单的选择规则，但不包括聚合。这个方法在这里被扩展到一类允许使用#count聚合的程序。本文件正在考虑被TPLP接受。
2022-05-16 cs.LO
Learning Concepts Definable in First-Order Logic with Counting
该研究将多对数度结构上一阶逻辑可定义分类器的亚线性时间学习结果推广至带计数的一阶逻辑FOCN，拓展到特定度界的不可知PAC学习，并证明无界度下亚线性学习不可行。
2025-07-24 cs.AI cs.LG cs.LO
Descriptive Complexity for Counting Complexity Classes
本文提出基于加权逻辑的量化二阶逻辑框架，用于系统刻画FP、#P、FPSPACE等计数复杂度类，并在#P内建立层次结构，通过添加递归捕获#L等低层类。
2020-02-07 cs.LO
Towards Capturing PTIME with no Counting Construct (but with a Choice Operator)
描述复杂性的核心问题是是否存在一种逻辑，它描述了关系结构上的确定性多项式时间（PTIME）。为了实现这一目标，我们定义了一个逻辑，是从一阶逻辑与不动点，FO（FP），通过一系列的转换，包括限制逻辑连接词和添加一个动态版本的希尔伯特的选择算子Eppery。形式主义可以同时被看作是二元关系的代数和线性时间模态动态逻辑，其中描述“证明”或“程序”的代数表达式出现在模态中。我们展示了如何计数，可达性和“混合”的例子（包括线性方程模2）公理化的逻辑，以及如何任意PTIME图灵机可以编码。对于每个固定的Choice函数，模型检验的数据复杂度为PTIME。然而，可以有指数级的多个这样的函数。一个关键的问题是，在什么样的语法条件下，代数项只检查一个选择函数是足够的。解决这个问题需要研究计算之间的对称性。本文通过代数和自动机理论的技术对这样的研究设置数学基础。
2021-11-15 cs.LO
L-Recursion and a new Logic for Logarithmic Space
我们扩展一阶逻辑计数的一个新的运营商，使其能够正式的有限形式的递归，可以在对数空间进行评估。由此产生的逻辑LREC具有LOGSPACE中的数据复杂性，并且它定义了LOGSPACE完全问题，如确定性可达性和布尔公式求值。我们证明了LREC的严格表达能力比具有计数的确定性传递闭包逻辑更强，而与对称传递闭包逻辑STC和传递闭包逻辑（有或没有计数）的表达能力是不可比拟的。LREC严格包含在具有计数FPC的定点逻辑中。我们还研究了LREC的一个扩展LREC=，它具有更好的闭包性质，比LREC和STC更有表现力，但仍然包含在FPC中，并且在LOGSPACE中具有数据复杂度。我们的主要结果是，LREC捕获LOGSPACE类的有向树和LREC=捕获LOGSPACE类的区间图。
2013-03-18 cs.CC cs.LO
Counting Bounded Tree Depth Homomorphisms
本文证明了图G，G'满足量词秩至多为k的一阶逻辑的相同命题当且仅当它们在树深至多为k的所有图的类上是同态不可区分的。这里G，G'是一类图C上的同态不可区分的，如果对于C中的每个图F，从F到G的同态数等于从F到G'的同态数。
2020-03-18 cs.DM cs.LO math.CO
On Generalized Records and Spatial Conjunction in Role Logic
我们以前已经介绍了角色逻辑作为一种符号，用于描述形状分析，数据库和知识库中的关系结构的属性。角色逻辑的自然片段对应于具有计数的二元逻辑，因此是可判定的。我们展示了如何使用角色逻辑来描述打开和关闭的记录，以及记录的对偶，反向记录。我们观察到分离逻辑的空间合取操作自然地模拟记录连接。此外，我们还讨论了如何用计数消除一阶逻辑中量词深度为1的公式的空间合取。因此，允许量词深度1的公式的空间合取保持了具有计数的二元逻辑的可判定性。这一结果同样适用于双变量角色逻辑片段。由此产生的逻辑顺利地集成了类型系统和谓词演算符号，可以被看作是一个自然的概括符号的约束中出现的角色分析和类似的形状分析方法。
2004-08-05 cs.LO cs.PL
Finite Variable Counting Logics with Restricted Requantification
本文研究限制部分变量再量化的计数逻辑，通过引入双射石子游戏和双参数Weisfeiler-Leman算法，阐明其表达能力，并发现不可再量化变量在空间复杂性上仅增加多项式因子，且可识别有界树深度和3连通平面图。
2024-11-11 cs.CC cs.LO
Counting CTL
本文提出了一系列的定量扩展的时序逻辑CTL。我们增强了时间模态的能力，以约束满足某些子公式沿路径的状态的数量。通过选择约束中允许的布尔运算和算术运算的组合，可以得到几个不同的推广CTL的逻辑。我们提供了一个彻底的分析，他们的表现力和简洁性，以及他们的模型检查和可满足性问题的复杂性（范围从P-完全不可判定）。最后，我们提出了两种具有相似特征的替代逻辑，并对这两种变体的性质进行了比较研究。
2013-02-15 cs.LO
First-Order Logic with Counting: At Least, Weak Hanf Normal Forms Always Exist and Can Be Computed!
我们介绍了逻辑FOCN（P），它扩展了一阶逻辑计数和数值谓词从一个集合P，它可以被看作是一个自然的概括各种计数逻辑，已在文献中研究。我们得到了一个局部性结果，表明每个FOCN（P）-公式都可以变换成Hanf范式公式，该公式在所有有限结构上等价，且次数不超过d.一个公式是Hanf范式，如果它是一个布尔组合的公式描述周围的自由变量元组和算术句子的谓词从P在原子语句描述的数量实现的类型与一个单一的中心。转换成Hanf范式可以实现在$d$中的时间初等和输入公式的大小。由这个局部性结果，我们得到了以下应用：（*）有界量词交替深度的一阶公式的Hanf局部性秩仅随公式大小多项式增长。（*）有界度结构上FOCN（P）的片段FOC（P）的模型检验问题是固定参数易处理的（具有基本参数依赖性）。（*）在度最大为d的完全动态数据库上，FOC（P）的固定查询的查询评估问题可以有效地解决：有一个动态算法可以以恒定的延迟枚举查询结果中的元组，并且允许计算查询结果的大小，并在每次数据库更新后的恒定时间内测试给定元组是否属于查询结果。
2017-03-03 cs.LO
Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures
提出$ω$MSO$\Join$BAPA逻辑，通过Parikh-Muller树自动机证明其在树可解释结构上的可满足性可判定，并推广至带高级计数的双变量逻辑与$μ$-演算。
2023-11-23 cs.FL cs.LO
Capturing Logarithmic Space and Polynomial Time on Chordal Claw-Free Graphs
本文证明弦无爪图类允许LREC$_=$可定义的规范化，从而存在对数空间规范化算法和同构测试，并由此捕获对数空间；由于LREC$_=$包含于带计数的定点逻辑，后者在该图类上捕获多项式时间。
2019-07-05 cs.DM cs.LO
Going Deep and Going Wide: Counting Logic and Homomorphism Indistinguishability over Graphs of Bounded Treedepth and Treewidth
本文用初等技巧重新证明计数一阶逻辑片段 $\mathsf{C}^k_q$ 与图类 $\mathcal{T}^k_q$ 上同态不可区分性的对应关系，并通过图论分析将其与有界树宽和树深图类的交集分离，同时证明 $\mathcal{TD}_q$ 同态区分封闭。
2023-08-11 cs.DM cs.LO
The Complexity of Reasoning for Fragments of Autoepistemic Logic
自认知逻辑通过模态算子L扩展命题逻辑。前面有L的公式被称为“相信”。该逻辑由Moore在1985年引入，用于对理想理性主体的行为和对自己信念的推理进行建模。本文分析了自认知逻辑中所有布尔片断的三个最常见的决策问题--扩展存在、勇敢推理和谨慎推理的计算复杂性。作为第二个贡献，我们分类的计算复杂性计数的数量稳定的扩展一个给定的知识库。据我们所知，这是第一篇分析自认知逻辑计数问题的论文。
2010-06-01 cs.CC cs.LO
Modulo Counting on Words and Trees
本文研究了用模计数量词扩展的一阶逻辑的二元片段在有限字或树上的可满足性问题。我们证明了这个逻辑的小模型属性，这给出了一个技术，用于确定可满足性问题。在词的情况下，这给出了一个新的证明EXPSPACE上界，并在树的情况下，它给出了一个2EXPTIME算法。该算法是最优的：我们证明了一个匹配的下界从交替图灵机工作在指数空间的通用减少，减少涉及到一个新版本的平铺游戏的发展。
2017-10-16 cs.LO
Lifted Inference beyond First-Order Logic
University of Padova（帕多瓦大学）
本研究扩展了C^2逻辑片段的域可提升性，使其能处理有向无环图、连通图、树和森林等现实数据属性，并提出“通过分裂计数”的新方法论，为概率推理和组合结构计数提供通用框架。
2025-02-25 cs.AI cs.LO math.CO
Nominals, Inverses, Counting, and Conjunctive Queries or: Why Infinity is your Friend!
Karlsruhe Institute of Technology（卡尔斯鲁厄理工学院）；Oxford University Computing Laboratory（牛津大学计算实验室）
描述逻辑是知识表示的形式主义，它提供了例如W3C OWL标准的逻辑基础。合取查询是数据库中的标准查询语言，作为查询描述逻辑知识库的一种表达形式，近年来得到了广泛的关注。几种不同的技术，决定合取查询蕴涵可用于广泛的DL。然而，OWL 1和OWL 2 DL中的名词、逆角色和数量限制的组合导致了迄今为止可用的技术无法解决的问题。我们解决这个问题，并提出了一个决定性的结果蕴涵工会的合取查询在DL ALCHOIQb，同时包含所有三个有问题的建设者。提供查询只包含简单的角色，我们的结果也显示了可判定性蕴涵（工会）合取查询的逻辑，支持OWL 1 DL，我们相信，所提出的结果将铺平道路，进一步取得进展合取查询蕴涵决策程序的描述逻辑基础的OWL标准。
2014-01-16 cs.AI cs.LO
Connection Matrices and the Definability of Graph Parameters
本文推广并详细证明了B. Godlin，T. Kotek和J.A. Makowsky（2008）和J.A. Makowsky（2009）.我们证明了它的巨大的适用性，在简化已知的和新的不可定义的结果的图形属性，并找到新的不可定义的结果的图形参数。我们还证明了一个Feferman-Vaught定理的逻辑CFOL，一阶逻辑与模计数量词。
2014-10-27 cs.LO math.CO
Analysis of logics with arithmetic
该研究针对带计数与算术的逻辑的有限可满足性问题，给出局部Presburger量词逻辑可满足性复杂度紧界与双变量计数逻辑基数半线性表示，还简化了部分已有关键结果的证明。
2025-10-29 cs.LO
Inapproximability of Unique Games in Fixed-Point Logic with Counting
本文在带计数的定点逻辑中证明唯一博弈问题存在不可近似间隙及任意常数因子内不可近似，并提出基于大围长图和随机仿射向量空间标记的新构造方法。
2024-04-17 cs.LO
Universal covers, color refinement, and two-variable counting logic: Lower bounds for the depth
给定一个连通图$G$及其顶点$x$，用$U_x(G)$表示从$x$出发将$G$展开为树所得到的$G$的泛覆盖.令$T=T(n)$是最小数，使得对于每个都具有至多$n$顶点的图$G$和$H$，$U_x(G)$和$U_y(H)$的同构必然从在深度$T$处截断的这些根树的同构得出。受分布式计算理论中应用的启发，Norris [Discrete Appl. Math. 1995]问，如果$T(n)\le n$。我们通过建立$T(n)=(2-o(1))n$来否定地回答这个问题。我们的解决方案使用有限模型理论的基本工具，如Immerman-Lander 2-pebble计数游戏的互模拟版本。为了证明$T(n)$的下界，我们构造了图$G_n$和$H_n$，图$G_n$和$H_n$也给出了其它一些紧下界。$G_n$和$H_n$都有$n$顶点，在2变量计数逻辑中只能用量词深度$(1-o(1))n$区分。由此可见，颜色细化（用于同构测试和用于计算图的粗略公平划分的其他领域的经典过程）需要$(1-o(1))n$轮来在$G_n$和$H_n$中的每一个上实现颜色稳定。有些令人惊讶的是，该轮数不足以在$G_n$和$H_n$的不相交联合上稳定颜色，其中需要$(2-o(1))n$轮。
2015-01-29 cs.DC cs.LO
Randomisation and Derandomisation in Descriptive Complexity Theory
我们从逻辑的角度研究概率复杂性类和去随机化问题。对于每一个逻辑L，我们引入一个新的逻辑BPL，有界错误概率L，这是从L中定义的复杂性类BPP，有界错误概率多项式时间，是从PTIME中定义的类似的方式。我们的主要重点在于问题的去随机化，我们证明，有一个查询是可定义的BPFO，概率版本的一阶逻辑，但不是在Cinf，有限变量无穷逻辑计数。这意味着有限模型理论的许多标准逻辑，如传递闭包逻辑和不动点逻辑，无论有无计数，都不能去随机化。同样，我们提出了一个查询的有序结构，这是在BPFO定义的，但不是在一元二阶逻辑，和一个查询的加法结构，这是在BPFO定义的，但不是在FO。这些查询中的后一个表明，AC0（有界深度多项式大小的电路）的某些统一变体不能被去随机化。这些结果与大多数标准复杂性类可以去随机化的普遍看法相反。最后，我们注意到，BPIFP+C，概率版本的定点逻辑计数，捕获的复杂性类BPP，即使在无序结构。
2011-09-20 cs.LO
Counting on Nowhere Dense Classes
Humboldt-Universität zu Berlin（柏林洪堡大学）
针对有效的无处稠密类，提出几乎线性时间预处理后常数时间计数查询和常数延迟枚举的算法，推广了现有关于一阶逻辑及带计数逻辑的结果。
2026-09-17 cs.LO
