The Polylog-Time Hierarchy Captured by Restricted Second-Order Logic
令$\mathrm{SO}^{\mathit{plog}}$表示二阶逻辑的限制，其中二阶量化在结构的大小中最多为多对数的大小关系上的范围。在这篇文章中，我们调查的问题，这图灵机复杂性类被捕获的布尔查询有序的关系结构，可以表示在这个逻辑。为此，我们定义了一个层次的片段$Σ^{\mathit{plog}}_m$（和$Π^{\mathit{plog}}_m$）定义的公式与交替块的存在和通用的二阶量词在量词前趋范式。我们首先表明，存在片段$Σ^{\mathit{plog}}_1$捕获NPolyLogTime，即布尔查询的类，可以接受的非确定性图灵机与随机访问的时间输入$O((\log n)^k)$的一些$k \ge 0$。使用具有随机访问输入的交替图灵机允许我们还将片段$Σ^{\mathit{plog}}_m$（和$Π^{\mathit{plog}}_m$）表示为具有由交替图灵机接受的最多$m$的二阶量词的交替块的那些布尔查询。因此，$\mathrm{SO}^{\mathit{plog}}$捕获整个多对数时间层次。我们通过数据库理论中的几个问题证明了这种逻辑和复杂性类的相关性。
2018-06-19 cs.LO
An effective characterization of the alternation hierarchy in two-variable logic
本文用恒等式刻画了二元一阶逻辑量词交替层次中各个层次的语言。这意味着个人水平的可决定性。更一般地，我们证明了一个可判定簇与簇J的双边半直积是可判定的。
2012-05-22 cs.LO
Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy
证明了对于任何固定的$i>0$，Presburger算术的$Σ_{i+1}$ -片段，即，它对以存在量词开始的$i+1$量词交替的限制对于$\mathsfΣ^{\mathsf{EXP}}_{i}$是完全的，$\mathsfΣ^{\mathsf{EXP}}_{i}$是弱EXP层次的第$i$层，是驻留在$\mathsf{NEXP}$和$\mathsf{EXPSPACE}$之间的多项式时间层次的类似物。这一结果完成了Presburger算法的计算复杂性景观，这一研究可以追溯到Fischer & Rabin在1974年的开创性工作。此外，我们应用的一些技术开发的证明的下限，以建立界限上的自然定义的$Σ_1$ -片段Presburger算法：给定一个$Σ_1$ -公式$Φ(x)$，它表明，一组非负的解决方案是一个最终的周期集，其周期是最多双指数，这个界是紧的。
2014-05-12 cs.LO
Dependence logic with a majority quantifier
本文研究了有限结构上依赖逻辑D的择多量词M的扩张。我们表明，由此产生的逻辑是equi-expressive与二阶逻辑的扩展，由二阶多数量词的所有种族。我们的结果意味着，从描述复杂性理论的角度来看，D（M）捕获的复杂性类计数层次。
2013-03-08 cs.LO math.LO
A Fine-Grained Hierarchy of Hard Problems in the Separated Fragment
最近，分离片段（SF）已被引入，并证明是可判定的。它的定义原则是，普遍存在的量化变量可能不会在原子中一起出现。已知的上界所需的时间来决定SF的可满足性问题制定的量词交替：给定一个SF句子$\exists \vec{z} \forall \vec{x}_1 \exists \vec{y}_1 \ldots \forall \vec{x}_n \exists \vec{y}_n . ψ$，其中$ψ$是量词免费的，可满足性可以决定在非确定性的$n$倍指数时间。在本文中，我们进行了更细粒度的分析SF-可满足性的复杂性。我们推导出一个上限和下限的存在变量的相互作用的程度（短：度）}-一个新的措施，有多少独立的存在量词块在一个句子中连接通过联合出现的变量在原子。我们的主要结果是$k$ -NEXPTIME-完全的满足性问题的集合$SF_{\leq k}$的所有SF句子，度$k$或更小。因此，我们表明，SF-可满足性是非初等的一般，因为SF的定义没有限制的程度。除了平凡的下界之外，迄今为止还没有任何关于SF-可满足性的硬度的知识。
2017-04-07 cs.LO
On the Mints Hierarchy in First-Order Intuitionistic Logic
我们分层的直觉一阶逻辑在$(\forall,\to)$到片段确定的交替出现的量词（薄荷层次）的积极和消极。我们研究这些片段的可判定性和复杂性。我们证明了即使是$Δ_2$水平是不可判定的和$Σ_1$是指数空间完全的。我们还证明了$Σ_1$的arity有界片段对于co-Neptime是完备的。
2016-12-27 cs.LO
Structure Theorem and Strict Alternation Hierarchy for FO^2 on Words
众所周知，词的每个一阶属性最多可以使用三个变量来表达。仅用两个变量可表达的性质的子类也很有趣，并且得到了很好的研究。我们证明了精确的结构定理，其特征在于精确的表达能力的一阶逻辑与两个变量的话。我们的结果适用于有和没有后继关系的情况。对于这两种语言，我们的结构定理准确地显示了使用给定的量词深度n和使用m个交替量词块，对于任何m \leq n，可以表达什么。使用这些特征，我们证明，除其他结果外，有一个严格的层次结构交替量词的两种语言。是否存在这样一种等级制度的问题是完全公开的。作为我们的结构结果的另一个后果，我们表明，可满足性的一阶逻辑与两个变量没有继任者，这是NEXP-完全的一般情况下，成为NP-完全的，一旦我们只考虑有界大小的字母表。
2009-08-03 cs.FL cs.LO
Hierarchies in inclusion logic with lax semantics
我们研究的表达能力的片段包含逻辑下所谓的松散的团队语义。通过限制全称量词的个数或限制分子式中包含原子的丰度来定义碎片。在全称量词的情况下，相应的层次结构在第一级崩溃。通过把这个问题与不动点逻辑中的arity层次的研究联系起来，证明了Arity层次是严格的。
2014-01-14 cs.LO math.LO
From algebra to logic: there and back again -- the story of a hierarchy
这是一个扩展的调查结果有关的层次结构的语言，是紧密相连的量词交替层次内的两个变量片段的一阶逻辑的线性秩序。
2014-06-03 cs.FL cs.LO
Separating regular languages with two quantifier alternations
本文研究自动机理论中的分离问题，针对连接层次，证明了基础有限时级别 3/2 的分离可判定，并推广到点深度层次级别 5/2，解决了 Σ₃ 的分离问题。
2018-11-15 cs.FL cs.LO
Nesting negations in FO2 over infinite words
我们考虑无限词上的二元一阶逻辑FO 2。限制嵌套否定的数量定义了一个无限的层次结构;它的级别通常被称为FO 2量词交替层次结构的半级。对于这个层次结构的每一个层次，我们给出了一个有效的表征。对于较低的水平，这个特征是一个代数和拓扑性质的组合。对于更高的层次，代数性质证明是足够的。在二元一阶逻辑中，每个代数性质都是Ω项的一个有序恒等式。拓扑性质与没有两变量限制的量词交替层次结构的下半层相同（即，Cantor拓扑和字母拓扑）。我们的结果推广了有限词的相应结果。证明使用新的技术，是基于一个完善的Mal'cev产品有序monoid。
2020-12-02 cs.FL cs.LO
On logical hierarchies within FO^2-definable languages
我们考虑一类语言中定义的2变量片段的一阶逻辑的线性秩序。这个类的许多有趣的特征是已知的，以及限制数量词交替产生一个无限层次的事实，其层次是各种语言（因此承认代数特征）。使用这种代数方法，我们证明了FO^{2}[<]中的量词交替层次结构在一个单元内是可判定的。为了这个目的，我们与可判定的各种语言，这可以定义在迭代确定性和协同确定性产品的层次结构的每一个级别。在这个过程中，一个关键的概念是浓缩的等级，这是对Weis和Immerman的等级以及Schwentick，Thérien和Vollmer的海龟语言的改进。
2012-08-14 cs.FL cs.LO
Finite-Degree Predicates and Two-Variable First-Order Logic
我们考虑有限字上的二元一阶逻辑，其量词交替数是固定的。我们表明，所有的语言与一个中立的字母定义的顺序和有限程度的谓词也可以定义的顺序谓词。从这个结果中，我们得到了分离的交替层次的二元逻辑上的这个签名。
2015-07-29 cs.LO
Raising a Hardness Result
Università di Roma “La Sapienza”（罗马第一大学）
本文介绍了一种技术证明问题的多项式层次或PSPACE的类很难。这种技术的基本原理是，一些问题的限制能够模拟存在或全称量词。如果是这种情况，从量化布尔公式（QBF）到这些限制的约简可以被转换为从在前面具有多个量词的QBF的约简。这意味着在多项式层次中的n级的问题的硬度的证明可以被分成n个单独的证明，这可能比直接示出从一类QBF到所考虑的问题的简化的证明更简单。
2007-08-30 cs.AI cs.CC cs.LO
Dynamic Complexity of Parity Exists Queries
研究奇偶存在查询在动态复杂度框架中的可维护性，证明其无法用无量词一阶规则维护，但度受限变体可用完整一阶规则维护。
2021-11-15 cs.LO
The μ-Calculus Alternation Hierarchy Collapses over Structures with Restricted Connectivity
我们知道μ演算中最小和最大不动点算子的交替层次是严格的。然而，严格的交替层次结构并不一定进行时，考虑限制类的结构。一个突出的例子是无限词的类，在这类词上，无选择的片段已经和完整的μ演算一样具有表达力。我们目前对μ演算交替层次结构何时以及为什么不严格的理解是有限的。本文在回答这些问题方面取得了进展，表明μ演算的交替层次结构崩溃的交替自由片段在某些类别的结构，包括无限嵌套的字和有限的图形与反馈顶点集的有界大小。这些类的共同之处在于，来自此类的结构中的组件之间的连通性受到限制，因为从结构的图中移除某些顶点会将其分解为所有路径都具有有限长度的图。我们的崩溃的结果是在自动机理论的设置。他们substrate，推广，并加强先前的结果的表达性的μ演算限制类的结构。
2012-10-09 cs.CC cs.FL cs.LO
The parameterized space complexity of model-checking bounded variable first-order logic
本文研究有界变量一阶查询模型检测的参数化空间复杂度，建立树层次结构完备性，提出高空间效率检测器，并探讨其最优性。
2019-09-19 cs.LO
From QBFs to MALL and back via focussing: fragments of multiplicative additive linear logic for each level of the polynomial hierarchy
在这项工作中，我们将探讨如何提取交替的时间界限从“集中”证明系统。我们的主要结果是获得片段的MALLw（MALL与削弱）完整的多项式层次的每一个级别。在一个方向上，我们编码QBF可满足性，并在另一个方向上，我们编码集中证明搜索，我们表明，这两个编码的组合保留量词交替，产生所需的结果。通过仔细地将众所周知的MALLw嵌入到MALL中，我们获得了MALL公式的类似描述，再次为多项式层次的每一级雕刻出完整的片段。这改进了MALLw和MALL都是PSPACE完备的著名结果。一个关键的见解是，我们必须改进聚焦的通常表示，以解释证明搜索中的确定性计算，这对应于不分支的可逆规则。这是为了我们可以更忠实地将集中证明搜索的阶段与它们的交替时间复杂度相关联。这个演示文稿似乎揭示了进一步的对偶性在水平上的证明搜索比通常的演示文稿，所以可能是进一步的证明理论的兴趣在其本身的权利。
2020-03-03 cs.LO
k variables are needed to define k-Clique in first-order logic
在早期的一篇论文中，Immerman提出了一个关于发展模型理论技术来证明有序结构下界的建议，这代表了有限模型理论的一个长期挑战。一个标志性的问题，代表这样一个挑战是需要多少变量来定义$k$ -团在一阶逻辑类的有限有序图？如果$k$变量是必要的，正如人们普遍认为的那样，这意味着一阶逻辑中的有界（或有限）变量层次对有限有序图类是严格的。2008年，Rossman通过计算$k$ -Clique建立了恒定深度无界扇入电路大小的最优平均情况下限，从而取得了突破性进展。在逻辑方面，这意味着它需要大于$\lfloor\frac{k} {4}\rfloor$变量来描述有限有序图类上的一阶逻辑中的$k$ -团问题，即使存在任意算术谓词。它遵循Immerman的一个未发表的结果，一阶逻辑中的有界变量层次确实是严格的。然而，罗斯曼的方法来自于电路复杂性和他自己的灵敏度的新概念。有限模型理论面临的挑战仍然存在。本文利用纯模型论工具箱给出了$\fo$中有界变量族严格性的另一种证明，并对一阶逻辑完全地回答了这个问题，即在这种逻辑中确实需要$k$ -变量来描述$k$ -团.与Rossman的证明相反，我们的证明是纯构造性的。然后，我们嵌入到一个纯算术结构的主要结构，以显示一个类似的结果，任意算术谓词。最后讨论了它在电路复杂性中的应用。
2015-01-19 cs.LO
Around Dot-depth One
点深度层次是无星语言的一种分类。它与有限词上一阶逻辑的量词交替层次有关。我们考虑通过禁止指定前缀或后缀获得的点深度为1/2和点深度为1的语言片段。事实证明，这些语言类与没有最小或最大谓词的存在一阶逻辑片段一一对应。对于所有的片段，我们得到有效的代数特征。此外，我们给出了新的组合证明的可判定性的成员问题的点深度1/2和点深度1。
2011-03-07 cs.FL cs.LO
Adding modular predicates to first-order fragments
我们调查的可定义性问题的一阶逻辑片段的可判定性有限词丰富的模块谓词。我们的方法的目标是最通用的语句，我们可以实现，它成功地涵盖了量词交替层次的一阶逻辑和它的一些片段。我们得到，决定这个问题的每一个层次的交替层次的一阶逻辑和它的两个变量片段时，配备了所有的正则数值谓词是不困难的，比决定它的相应级别只配备了线性顺序和继任者。对于双变量片段，我们也处理了只包含顺序和模谓词的签名的情况。这证明了两个-在一阶逻辑的情况下，这个问题对于大于二的层次仍然是开放的。证明的主要成分也是一阶公式的句法变换作为有限范畴的代数框架。
2015-11-13 cs.FL cs.LO
On the Expressive Power of 2-Stack Visibly Pushdown Automata
可见下推自动机是输入驱动的下推自动机，它可以识别一些非正则上下文无关语言，同时保持了有限自动机的良好闭包和可判定性。具有多个堆栈的可见下推自动机最近被La Torre，Madhusudan和Parlato考虑，他们进一步利用可见性的概念来获得丰富的自动机类，甚至可以表达上下文无关语言之外的属性。同时，它们的自动机在布尔运算下是封闭的，具有可判定的空性和包含性问题，并且在具有额外嵌套结构的词上享有一元二阶逻辑的逻辑表征。这些结果需要一个限制版本的明显下推自动机与多个堆栈，其行为可以分为一个固定数量的阶段。在本文中，我们考虑2-栈可见下推自动机（即，具有两个堆栈的可视下推自动机）以其不受限制的形式。我们表明，他们是表达等价的一元二阶逻辑的存在片段。此外，我们还发现一元二阶量词交替在多重嵌套的词中形成了一个无限的层级结构。结合这些结果，我们得出结论，2-栈可见下推自动机是不封闭的补充。最后，我们讨论了Büchi 2-栈可见下推自动机运行在无限（嵌套）的话的表达能力。通过无限量词扩展逻辑，我们同样可以建立与存在一元二阶逻辑的等价。
2008-12-24 cs.LO
On Counting Propositional Logic
我们研究计数命题逻辑作为命题逻辑与计数量词的扩展。我们证明，基本的决策问题的复杂性完全匹配瓦格纳的计数层次的适当水平，而且由此产生的逻辑承认一个令人满意的证明理论治疗。从后者，一个类型系统中的概率演算的Curry-Howard对应的精神，显示了潜在的计数命题逻辑作为一个有用的工具，在几个领域的理论计算机科学。
2021-06-03 cs.CC cs.LO cs.PL
On the Complexity of Horn and Krom Fragments of Second-Order Boolean Logic
二阶布尔逻辑是QBF的推广，其常数交替片段已知对于指数时间层次的水平是完全的。我们考虑这种逻辑的两种类型的限制：1）对项构造的限制，2）对布尔矩阵的形式的限制。对于第一类，我们考虑两种限制：首先，不允许嵌套使用适当的函数变量，其次规定每个函数变量必须以固定的参数序列出现。第二种，我们考虑霍恩，克罗姆，和核心片段的布尔矩阵。我们分类的复杂性的逻辑得到这两种类型的限制相结合。我们表明，在大多数情况下，逻辑与k交替块的函数量词是完整的指数时间层次的第k或（k-1）级。此外，我们建立NL-完全的克罗姆和核心片段，当k=1和第一类的限制都有效。
2020-07-08 cs.CC cs.LO
HyperLTL Satisfiability is $Σ_1^1$-complete, HyperCTL* Satisfiability is $Σ_1^2$-complete
用于信息流属性规范的时态逻辑能够表达系统的多个执行之间的关系。两个最重要的逻辑是HyperLTL和HyperCTL*，它们通过跟踪量化来概括LTL和CTL*。众所周知，这种表达性是有代价的，即满足性对于两种逻辑都是不可判定的。在本文中，我们解决这些问题的精确复杂性，表明这两个实际上是高度不可判定的：我们证明了HyperLTL可满足性是$Σ_1^1$ -完全和HyperCTL* 可满足性是$Σ_1^2$ -完全。这些是在先前已知的下限和第一上限上的显著增加。为了证明HyperCTL* 的$Σ_1^2$ -成员资格，我们证明了每一个可满足的HyperCTL* 句子有一个模型，是equinumerous的连续，这种第一个上界。我们证明这一定是紧的。最后，我们证明了HyperLTL量词交替层次的每一层的成员问题是$Π_1^1$ -完全的。
2021-05-10 cs.LO
A Restricted Second-Order Logic for Non-deterministic Poly-Logarithmic Time
我们引入了一个有限结构的限制二阶逻辑$\mathrm{SO}^{\mathit{plog}}$，其中二阶量化的范围最多的结构的大小的多对数的大小的关系。我们通过数据库理论中的几个问题证明了这种逻辑和复杂性类的相关性。然后，我们证明了Fagin的风格定理，表明可以在$\mathrm{SO}^{\mathit{plog}}$的存在片段中表示的布尔查询恰好对应于可以由非确定性图灵机计算的决策问题的类，该图灵机对某些$k \ge 0$在时间上随机访问输入$O((\log n)^k)$，即，在非确定性多对数时间内可计算的问题。应该注意的是，与Fagin定理证明二阶逻辑的存在片段在任意有限结构上捕获NP不同，我们的结果仅在有序有限结构上成立，因为$\mathrm{SO}^{\mathit{plog}}$太弱，无法定义域的全序。然而，$\mathrm{SO}^{\mathit{plog}}$以与二阶逻辑如何在多项式空间内提供自然水平的可表达性密切相关的方式在多对数空间内提供自然水平的可表达性。事实上，我们展示了$\mathrm{SO}^{\mathit{plog}}$的量词前缀类和非确定性多对数时间层次的水平之间的精确对应，类似于二阶逻辑的量词前缀类和多项式时间层次之间的对应。我们的工作与David A. 1992年的Mix Barrington。我们将详细探讨这种关系。
2019-11-29 cs.LO math.LO
Separation of bounded arithmetic using a consistency statement
本文证明了Buss的有界算术族$S^1_2 \subseteq S^2_2 \subseteq \cdots \subseteq S^i_2 \subseteq \cdots$不完全坍缩.更准确地说，我们证明，对于一定的$D$，$S^1_2 \subsetneq S^{2D+5}_2$持有。此外，我们可以允许$S^1_2, S^2_2, \ldots$的BASIC公理的真量词自由公式的任何有限集。根据Takeuti的论点，这意味着$\mathrm{P} \neq \mathrm{NP}$。设$\mathbf{Ax}$是BASIC公理的一个特定公式。我们证明$S^1_2 \not\vdash \mathrm{Con}(\mathrm{PV}^-_1(D) + \mathbf{Ax})$足够大的$D$，而$S^{2D+7}_2 \vdash \mathrm{Con}(\mathrm{PV}^-_1(D) + \mathbf{Ax})$的系统$\mathrm{PV}^-_1(D)$，系统$\mathrm{PV}^-_1$的一个片段，诱导免费的库克的$\mathrm{PV}$，其中证明只包含公式小于$D$连接词的一阶扩展。$S^1_2 \not\vdash \mathrm{Con}(\mathrm{PV}^-_1(D) + \mathbf{Ax})$的证明是通过直接改编的$\mathrm{…
2019-10-30 cs.LO math.LO
A LOCAL View of the Polynomial Hierarchy
该研究将经典计算复杂性方法拓展至分布式LOCAL模型，构建分布式多项式谱系并推广核心复杂性定理，证明该谱系无限，还提出用量词交替衡量问题局部性的新工具。
2025-09-04 cs.CC cs.DC cs.FL
On first-order transductions of classes of graphs
本文研究图类的一阶转导拟序，证明转导的局部范式，并探讨其复杂性、极值类、路径宽度层次及弱稀疏类的作用。
2025-06-19 cs.DM cs.LO math.CO
First-Order Model Checking on Generalisations of Pushdown Graphs
我们研究了两种推广的下推图的一阶模型检验问题。第一类是嵌套下推树类。另一类是可折叠下推图。我们的主要结果如下。可达的一阶逻辑在嵌套下推树上是一致可判定的。考虑无可达性的一阶逻辑，证明了在线性多个交替的双指数交替时间中的可判定性。具有正则可达谓词的一阶逻辑在2级可折叠下推图上是一致可判定的。此外，嵌套下推树是一阶可解释的可折叠下推图的水平2。这种解释可以扩展到可折叠下推图层次结构中的高阶嵌套下推树类的解释。我们证明了这个新的层次结构的嵌套树的第二层具有可判定的一阶模型检测。我们的可折叠下推图的可判定性结果依赖于这样一个事实，即2级可折叠下推图是均匀树自动的。我们的最后一个结果涉及一般的树自动结构。证明了Ramsey量词扩展的一阶逻辑在所有树自动结构上都是可判定的。
2012-02-01 cs.FL cs.LO math.LO
Fixed-parameter tractability, definability, and model checking
本文从逻辑学的角度研究参数化复杂性理论，更具体地说，是从描述复杂性理论的角度研究参数化复杂性理论。我们建议考虑参数化模型检查问题的各种片段的一阶逻辑作为通用的参数化问题，并显示这种方法可以是有用的研究固定参数的易处理性和难处理性。例如，我们建立了存在一阶逻辑的模型检验，关系结构的同态问题，和子结构同构问题之间的等价性。我们的主要易处理性结果表明，一阶公式的模型检查是固定参数易处理时，限制到一类的输入结构与排除未成年人。在棘手的方面，对于每个t >= 0，我们证明了具有t个量词交替的一阶公式的模型检查与具有t个量词交替的交替图灵机的参数化停止问题之间的等价性。我们讨论了这种交替层次与Downey和Fellows的W-层次之间的密切联系。在一个更抽象的层次上，我们考虑两种形式的可定义性，称为Fagin可定义性和分片可定义性，这是适当的描述参数化的问题。我们给出了所有固定参数易处理问题的FPT类在有限变量最小不动点逻辑中的分片可定义性方面的一个特征，这让人想起Immerman-Vardi定理，它描述了PTIME类在最小不动点逻辑中的可定义性。
2001-02-19 cs.CC cs.LO
The amazing mixed polynomial closure and its applications to two-variable first-order logic
多项式闭包是应用于一类正则语言的标准算子。在本文中，我们研究了三个限制称为左（LPol），右（RPol）和混合多项式闭包（MPol）。前两个是已知的，而MPol是新的。我们来看两个为每个类C定义的决策问题。成员资格将一个正则语言作为输入，并询问它是否属于C。Separation将两种正则语言作为输入，并询问C中是否存在第三种语言，包括第一种语言，并且与第二种语言不相交。我们证明了LPol，RPol和MPol保持温和的假设下的输入类的成员资格的可判定性，和更强的假设下的分离的可判定性。我们将这些结果应用于自然层次结构。首先，我们来看看几个语言理论层次结构，这些层次结构是通过将LPol、RPol和MPol递归地应用于单个输入类而构建的。我们证明，这些层次结构实际上可以定义使用几乎完全MPol。我们还考虑了两变量一阶逻辑的量词交替层次结构，并证明了可以使用MPol爬上它们。结果是通用的，因为它适用于大多数标准的签名选择。我们用它来证明，对于大多数这些选择，成员资格是决定的层次结构中的所有级别。最后，我们证明了对于只具有线性序的二元一阶逻辑的层次，分离是可判定的。
2022-12-31 cs.FL cs.LO
HyperLTL Satisfiability Is Highly Undecidable, HyperCTL$^*$ is Even Harder
该研究确定了HyperLTL与HyperCTL*两种信息流时序逻辑可满足性问题的精确不可判定复杂度，给出了对应复杂度类的上下界，并证明了相关衍生问题的难度等级。
2025-01-09 cs.LO
The Covering Problem
本文提出覆盖问题作为成员资格问题的替代，以更好地研究逻辑表达能力，并通过三个论点论证其合理性，同时提供相应数学框架与方法论。
2018-07-19 cs.LO
The Logical Expressiveness of Topological Neural Networks
Aalto University（阿alto大学）；Federal Institute of Ceará（塞阿拉联邦理工学院）；YaiYai Ltd（YaiYai公司）
本文研究拓扑神经网络的逻辑表达能力，通过分析拓扑同构测试和引入拓扑计数逻辑，证明k-CCWL与TC_{k+2}及拓扑(k+2)-pebble游戏的等价性，确立了TNN的逻辑表达理论。
2026-04-21 cs.LG cs.LO
Aspects of Coherence in Dependence Logic
Leibniz Universität Hannover（汉诺威莱布尼茨大学）；University of Tartu（塔尔图大学）；University of Helsinki（赫尔辛基大学）；University of California Santa Cruz（加州大学圣克鲁兹分校）
本文研究依赖逻辑公式的k-相干性，证明无量词依赖逻辑公式的相干性等价于一阶可重写性，并分析了相干性判定问题的计算复杂性。
2026-05-29 cs.CC cs.LO
