Finite Variable Counting Logics with Restricted Requantification
本文研究限制部分变量再量化的计数逻辑，通过引入双射石子游戏和双参数Weisfeiler-Leman算法，阐明其表达能力，并发现不可再量化变量在空间复杂性上仅增加多项式因子，且可识别有界树深度和3连通平面图。
2024-11-11 cs.CC cs.LO
A Game for Counting Logic Formula Size and an Application to Linear Orders
本文提出一种 EF 博弈来刻画有界变量计数逻辑的公式大小，并利用它将线性序的公式大小下界从 3 变量一阶逻辑扩展到 3 变量计数逻辑，首次给出计数逻辑的公式大小下界。
2025-05-22 cs.LO
Counting proofs in propositional logic
本文给出了一个计算各种命题逻辑中公式的不同证明的方法。这个数字要么是整数（如果公式不可证明，则可能是0），要么是无限大。
2009-05-18 cs.LO math.LO
Model-checking Counting Temporal Logics on Flat Structures
我们研究了几个扩展的线性时间和计算树的时间逻辑与量词，允许计数经常某些属性举行。对于大多数这些扩展，模型检验问题是不可判定的，但我们表明，可判定性可以恢复考虑平坦的Kripke结构，每个状态属于最多一个简单的循环。大多数决策程序是基于（平面）计数器系统的结果，其中计数器用于实现计数运算符的评估。
2017-06-26 cs.LO
Regular graphs and the spectra of two-variable logic with counting
一阶逻辑语句的{ \em谱}是作为其有限模型基数的自然数的集合。在本文中，我们表明，当限制到只使用两个变量，但允许计数量词，一阶逻辑句子的谱是半线性的，因此，在补下关闭。我们证明的核心是正则图和双正则图存在性的半线性特征，这类图的顶点度存在先验界限。我们的证明还提供了一个简单的表征模型的两个变量的逻辑计数-也就是说，到重命名和扩展的关系名称，它们只是一个集合的定期和birregular图。
2014-06-11 cs.CC cs.DM 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
Graded modal logic and counting bisimulation
本文将互模拟不变片段的刻画定理推广到分级多模态逻辑，证明其在所有及有限点态 Kripke 结构上恰好对应计数互模拟等价下保持的一阶性质。
2023-07-18 cs.LO math.LO
On Presburger arithmetic extended with non-unary counting quantifiers
研究扩展了非一元计数量词的Presburger算术，通过量词消去与归约技术证明其满足性在两重指数空间内可判定，并给出不同量词组合下的计算复杂度上界。
2023-07-11 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
The Complexity of Reasoning for Fragments of Autoepistemic Logic
自认知逻辑通过模态算子L扩展命题逻辑。前面有L的公式被称为“相信”。该逻辑由Moore在1985年引入，用于对理想理性主体的行为和对自己信念的推理进行建模。本文分析了自认知逻辑中所有布尔片断的三个最常见的决策问题--扩展存在、勇敢推理和谨慎推理的计算复杂性。作为第二个贡献，我们分类的计算复杂性计数的数量稳定的扩展一个给定的知识库。据我们所知，这是第一篇分析自认知逻辑计数问题的论文。
2010-06-01 cs.CC cs.LO
Extending Two-Variable Logic on Trees
最近证明了在树上解释的一阶逻辑的两个变量片段的有限可满足性问题是ExpSpace完备的。我们考虑这个逻辑的两个扩展。我们发现，添加额外的二进制符号或计数量词的逻辑不影响有限可满足性问题的复杂性。然而，结合两个扩展并添加二进制符号和计数量词会导致这种复杂性的爆炸。我们还比较了两个变量的片段的表达能力，其扩展与计数量词的树木。事实证明，这两种逻辑具有同样的表达能力，尽管在无序树的限制情况下，计数量词确实增加了表达能力。
2016-11-24 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
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
Definability of linear equation systems over groups and rings
出于对PTIME逻辑的追求和最近的见解，从线性代数问题的描述复杂性是这个问题的一个重要方面，我们研究了线性方程组的可解性有限群和环的逻辑（间）定义的观点。我们考虑的所有问题都是在多项式时间内可判定的，但不能用带计数的不动点逻辑来表示。他们还提供了一个自然的候选人分离的多项式时间从秩逻辑，扩展不动点逻辑的运营商确定的秩可定义的矩阵，这是足够的可解性问题领域。基于有限环的结构理论，我们建立了各种可解性问题的逻辑归约。我们的研究结果表明，所有的线性方程组的可解性问题，分离不动点逻辑计数PTIME可以减少到可解性交换环。此外，我们证明了封闭性质的查询类，减少到可解性环，这提供了范式的逻辑扩展与可解性运营商。我们的结论是研究在何种程度上的不动点逻辑计数可以表示问题的线性代数有限交换环，推广已知的结果在有限域的线性代数问题的逻辑定义。
2013-11-11 cs.CC cs.LO
The Complexity of Temporal Logic over the Reals
本文证明了实数时间上具有until和since连接词的时态逻辑的判定问题是PSPACE完全的。
1999-10-13 cs.CC cs.LO
Modulo-Counting First-Order Logic on Bounded Expansion Classes
我们证明了，在有界扩展类，每一个一阶公式与模计数是等价的，在线性时间可计算的一元扩展，一个存在的一阶公式。因此，我们得出，有界扩展类，一阶转换与模计数具有相同的编码能力作为存在的一阶转换。此外，模计数的一阶模型检验和计算的规模可定义在模计数的一阶逻辑可以实现在线性时间上有界的扩展类。作为应用，我们证明了一个图类具有结构有界扩张当且仅当它是一个有界扩张类中的一个有界深度顶点子式类。我们还展示了如何我们的结果可以用来实现快速矩阵演算有限域上的有界扩展矩阵。
2023-03-23 cs.LO math.CO
One-Variable Logic Meets Presburger Arithmetic
我们考虑一阶逻辑的一个变量片段扩展Presburger约束。该逻辑的设计方式是，它包含了以前已知的片段扩展计数，模计数或基数比较，并结合他们的表达能力。我们证明了NP-完全的逻辑，提出了一个最佳的算法来解决其有限的可满足性问题。
2019-09-16 cs.LO
Counting Homomorphisms from Hypergraphs of Bounded Generalised Hypertree Width: A Logical Characterisation
本研究提出双类型计数逻辑$GC^k$，证明其等价于广义超树宽度至多k的超图类上的同态不可区分性，将图领域的相关经典结论推广至超图场景。
2023-08-21 cs.LO
Interleaving Logic and Counting
本文研究自然语言推理中逻辑与计数的结合，通过带计数的单子一阶逻辑及其强化形式，分析可定义性、公理化与可判定性，并联系语言量词和认知科学。
2025-07-07 cs.CL cs.LO math.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
Two variable logic with ultimately periodic counting
本文研究带最终周期计数量词的二变量逻辑，证明其可满足性与有限可满足性可判定，并证明句子谱可在Presburger算术中定义，同时改进了双正则图方法。
2024-04-03 cs.LO math.CO
Undecidable propositional bimodal logics and one-variable first-order linear temporal logics with counting
一阶时态逻辑因其糟糕的计算行为而臭名昭著。众所周知，即使是两个变量的一元片段在各种线性时间线上也是高度不可判定的，并且在分支时间上，即使是一个变量的片段也可能是不可判定的。然而，已经有几个试图找到良好的一阶时序逻辑和相关的时序描述逻辑的片段，主要是通过限制可用的量词模式，或考虑子布尔语言。在这里，我们分析看似“温和”的扩展可判定的一个变量的片段与计数能力，解释模型与恒定，减少，扩大一阶域。我们表明，在大多数类的线性订单，这些逻辑是（有时高度）不可判定的，即使没有常数和函数符号，并与唯一的时间运营商“最终”。我们建立连接与双峰逻辑在二维产品结构具有线性和“差异”（不等式）组件的关系，并证明我们的结果在此双峰设置。我们给出了一个普遍的结果，即许多具有可交换线性和差分关系的双峰模型的可满足性是不可判定的。作为一个副产品，我们还获得了新的例子，但Kripke不完全双峰逻辑的axiomatisable。我们的结果推广了双峰逻辑在两个线性关系的乘积上的类似下界，并且我们的证明方法与这些结果的证明有很大的不同。与以前的证明，第一个“对角编码”的无限网格，然后使用减少平铺或图灵机的问题，在这里，我们直接使用的网格状结构的产品框架，并获得undecidability减少计数器（明斯基）机的问题。
2015-06-08 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
Strong Equivalence of Logic Programs with Counting
在答案集编程中，如果两组规则在任何上下文中具有相同的含义，则它们被认为是强等价的。在某些情况下，可以通过从另一个程序的规则中推导出每个程序的规则来建立接地外国佬的输入语言的程序的强等价性。这种证明的可能性已经在该语言的一个子集上得到了证明，该子集包括比较、算术运算和简单的选择规则，但不包括聚合。这个方法在这里被扩展到一类允许使用#count聚合的程序。本文件正在考虑被TPLP接受。
2022-05-16 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
Graded modal logic and counting message passing automata
本研究探讨分级多模态逻辑与计数消息传递自动机的关联，提出分级多模态类型与推广Weisfeiler-Leman算法的自动机，证明二者识别模型类的等价性，并给出带Härtig量词和最大不动点的一阶逻辑执行该算法的方法。
2024-01-26 cs.DC cs.LO
Learning Aggregate Queries Defined by First-Order Logic with Counting
本文研究超越布尔分类的多类整数分类问题，提出在拟线性时间内构建索引结构，实现FOC1可定义整数值分类器的高效学习。
2024-11-06 cs.DB 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
Counting CTL
本文提出了一系列的定量扩展的时序逻辑CTL。我们增强了时间模态的能力，以约束满足某些子公式沿路径的状态的数量。通过选择约束中允许的布尔运算和算术运算的组合，可以得到几个不同的推广CTL的逻辑。我们提供了一个彻底的分析，他们的表现力和简洁性，以及他们的模型检查和可满足性问题的复杂性（范围从P-完全不可判定）。最后，我们提出了两种具有相似特征的替代逻辑，并对这两种变体的性质进行了比较研究。
2013-02-15 cs.LO
A Fine-Grained Dichotomy for Bounded-Variable Query Evaluation: The Calculus of Relations, a Boolean Modal Logic, and One-Variable Counting Logic
Chiba University（千叶大学）；CyberAgent, Inc.（CyberAgent公司）；National Institute of Informatics（信息学国立研究所）
本文针对稀疏结构上的有界变量布尔一阶查询，在稀疏MAX-3-SAT假设下证明了细粒度二分定理，刻画了可处理片段并归约到关系演算、新布尔模态逻辑和单变量计数逻辑。
2026-10-06 cs.CC cs.DB 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
Learning Concepts Definable in First-Order Logic with Counting
该研究将多对数度结构上一阶逻辑可定义分类器的亚线性时间学习结果推广至带计数的一阶逻辑FOCN，拓展到特定度界的不可知PAC学习，并证明无界度下亚线性学习不可行。
2025-07-24 cs.AI cs.LG cs.LO
On Generalized Records and Spatial Conjunction in Role Logic
我们以前已经介绍了角色逻辑作为一种符号，用于描述形状分析，数据库和知识库中的关系结构的属性。角色逻辑的自然片段对应于具有计数的二元逻辑，因此是可判定的。我们展示了如何使用角色逻辑来描述打开和关闭的记录，以及记录的对偶，反向记录。我们观察到分离逻辑的空间合取操作自然地模拟记录连接。此外，我们还讨论了如何用计数消除一阶逻辑中量词深度为1的公式的空间合取。因此，允许量词深度1的公式的空间合取保持了具有计数的二元逻辑的可判定性。这一结果同样适用于双变量角色逻辑片段。由此产生的逻辑顺利地集成了类型系统和谓词演算符号，可以被看作是一个自然的概括符号的约束中出现的角色分析和类似的形状分析方法。
2004-08-05 cs.LO cs.PL
Epistemic Logic Programs: Non-Ground and Counting Complexity
Institute of Logic and Computation, TU Wien（维也纳技术大学逻辑与计算研究所）；Department of Computer and Information Science (IDA), Linköping University（林雪平大学计算机与信息科学系）；Univ. Artois, CNRS, CRIL（阿图瓦大学、法国国家科学研究中心、CRIL研究所）
本文研究了非基础认知逻辑程序（ELP）的计算复杂性，确立了其著名片段在 NEXPTIME 类的完备性，并提供了计数复杂性、有界谓词元数及树宽参数下的ETH紧密运行时间结果。
2025-01-31 cs.AI cs.CC cs.LO
Logic Column 19: Symbolic Model Checking for Temporal-Epistemic Logics
本文综述了近年来通过符号模型检验验证时态认知逻辑的一些工作，重点介绍了基于OBDD和基于SAT的离散和实时分支时态逻辑的认知逻辑验证方法。
2007-09-04 cs.LO
$ω$-Forest Algebras and Temporal Logics
我们使用[4]中介绍的无限树语言的代数框架来导出各种时态逻辑的有效特征，特别是逻辑EF（CTL的一个片段）及其计数变体cEF。
2022-03-25 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
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
Modulo Counting on Words and Trees
本文研究了用模计数量词扩展的一阶逻辑的二元片段在有限字或树上的可满足性问题。我们证明了这个逻辑的小模型属性，这给出了一个技术，用于确定可满足性问题。在词的情况下，这给出了一个新的证明EXPSPACE上界，并在树的情况下，它给出了一个2EXPTIME算法。该算法是最优的：我们证明了一个匹配的下界从交替图灵机工作在指数空间的通用减少，减少涉及到一个新版本的平铺游戏的发展。
2017-10-16 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
Logic Column 11: The Finite and the Infinite in Temporal Logic
本文研究了有限和无限序列上的LTL时态算子的解释。这是用来作为一个健全的和完整的公理化的Caret，最近的时间逻辑推理嵌套过程调用和返回的程序推导的基础。
2005-04-24 cs.LO
Analysis of logics with arithmetic
该研究针对带计数与算术的逻辑的有限可满足性问题，给出局部Presburger量词逻辑可满足性复杂度紧界与双变量计数逻辑基数半线性表示，还简化了部分已有关键结果的证明。
2025-10-29 cs.LO
Constant time testability of first-order logic with modulo counting on finitary graphs
University of Bamberg（班贝格大学）
本文研究了在有界度模型下，常数运行时间的属性测试算法元定理。针对有界组件大小的图类，证明了一阶逻辑带模计数（FOMOD）的常数时间可测试性，并引入了数论中的'补充分条件'来推断全局信息。
2026-05-11 cs.LO math.LO
Inapproximability of Unique Games in Fixed-Point Logic with Counting
本文在带计数的定点逻辑中证明唯一博弈问题存在不可近似间隙及任意常数因子内不可近似，并提出基于大围长图和随机仿射向量空间标记的新构造方法。
2024-04-17 cs.LO
Graphs Identified by Logics with Counting
我们对图进行分类，更一般地说，对由C2标识的有限关系结构进行分类，即具有计数的双变量一阶逻辑。使用这种分类，我们表明，它可以决定在几乎线性的时间是否一个结构被确定为C2。我们的分类意味着，对于这个逻辑识别的每个图，它的所有顶点颜色版本也被识别。对于有限关系结构，也有类似的说法。我们提供了解决线性时间有限结构反演问题的构造。这个问题以前已被证明是多项式时间可解的马丁奥托。对于图，我们得出结论，每个C2-等价类包含一个图，其轨道正是其顶点集的C2-划分的类，并有一个单一的自同构证明这一事实。对于一般k，我们表明，这种说法是不正确的，通过提供的例子，图的大小线性k确定的C3，但其轨道分区是严格精细比CK-分区。我们还提供了确定的图形，顶点颜色的版本，不确定的CK。
2015-03-30 cs.DM cs.LO math.CO
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
Interval Temporal Logic Decision Tree Learning
决策树是一种简单但功能强大的分类模型，用于分类分类和数值数据，尽管简单，但它们通常用于运筹学和管理以及知识挖掘。从逻辑的角度来看，决策树可以看作是用命题逻辑编写的逻辑规则的结构化集合。由于知识挖掘正迅速向时态知识挖掘发展，并且由于在许多情况下时态信息最好由区间时态逻辑描述，因此命题逻辑决策树可能向区间时态逻辑决策树发展。本文定义了区间时态逻辑决策树学习问题，并提出了一种推广经典决策树学习的解决方案。
2020-03-12 cs.LO
