Expressivity within second-order transitive-closure logic
二阶传递闭包逻辑SO（TC）是一种表达性声明语言，它捕获了复杂性类PSPACE。它的一元片段MSO（TC）已经允许以自然和优雅的方式表达各种NP困难甚至PSPACE困难的问题。由于SO（TC）提供了一个有吸引力的框架，用于在声明式指定的计算方面表达属性，因此理解语言的不同特征的表达性是很有趣的。本文重点讨论片段MSO（TC），以及纯存在片段SO（2 TC）（E）;在2 TC中，TC算子仅绑定关系变量的元组。我们建立，关于表达能力，SO（2 TC）（E）崩溃到存在一阶逻辑。此外，我们还研究了MSO（TC）与具有计数特征的MSO（TC）的扩展（CMSO（TC））以及与阶不变MSO的关系。我们发现CMSO（TC）和MSO（TC）的表达能力是一致的。此外，我们建立，在一元词汇表，MSO（TC）严格包含顺序不变的MSO。
2018-04-16 cs.LO
Characterizing Weighted MSO for Trees by Branching Transitive Closure Logics
我们引入了分支传递闭包算子的加权一元二阶逻辑公式的分支对应于一个自然的方式在树中固有的分支。对任意交换半环，我们证明了树上的加权一元二阶逻辑等价于由下列算子之一开始的公式的可定义性：（i）分支传递闭包或（ii）存在二阶量词后接泛一阶量词;在这两种情况下，该运算符被应用于（a）通过模计数而丰富的布尔一阶逻辑或（b）布尔一元二阶逻辑上的步进公式。
2015-04-29 cs.FL cs.LO
The Finite Model Property of Quasi-transitive Modal Logic
建立了准传递模态逻辑$\mathsf{K}_2^3=\mathsf{K}\oplus \Box\Box p\rightarrow \Box\Box\Box p$的有限模型性质。这种模态逻辑被保守地扩展到时态逻辑$\mathsf{Kt}_2^3$。本文提出了一个求解$\mathsf{Kt}_2^3$的Gentzen微积分$\mathsf{G}$。该演算$\mathsf{G}$通过有限的句法结构而具有有限代数性质。因此，$\mathsf{Kt}_2^3$和$\mathsf{K}_2^3$具有有限模型性质。
2019-02-22 cs.LO
Size matters in the modal $μ$-calculus
我们讨论和比较复杂性措施的模态$μ$演算，专注于大小和交替深度。作为一个尺度，我们采取威尔克的交替树自动机，我们将呼吁奇偶公式在文本中。在Bruse，Friedmann和Lange的工作基础上，我们比较了$μ$ -演算公式的两种大小度量：子公式大小，即给定公式的子公式的数量，和闭包大小。这些概念对应于公式的表示，即分别基于其子公式dag和闭包图的奇偶公式。我们的方法的区别在于，我们明确了α等价的作用，因为天真地重命名绑定变量可能导致指数爆破。此外，我们匹配公式的交替深度与奇偶公式的索引。我们从一个没有阿尔法等价的环境开始。定义了子公式大小和闭包大小，并指出$μ$ -演算公式可以转化为大小线性的奇偶公式，给出了将$μ$ -演算公式转化为等价的奇偶公式的构造.相反，有一个标准的转换产生一个指数子公式的$μ$ -演算公式-但根据原始奇偶公式的大小，闭包大小是线性的。我们确定所谓的无扭奇偶公式的子公式的大小存在的变换线性。然后，我们引入大小的概念是完全不变的阿尔法等价。我们转移Bruse等人的结果，表明在我们的设置中，闭包大小也可以指数小于子公式大小。我们还展示了如何重命名绑定变量，使阿尔法等价成为语法上的封闭集的身份。最后，我们回顾了保护变换的复杂性。
2020-10-27 cs.LO
Reaching Classicality through Transitive Closure
本文通过传递闭包及其对偶运算，将基于不同三值方案和标准的逻辑组合，证明经典逻辑可由亚完备与亚一致逻辑的并集经传递闭包获得，并刻画了逻辑间的格结构关系。
2025-03-28 cs.LO math.LO
Tableaux for multi-modal hybrid logic with binders, transitive relations and relation hierarchies
在以前的文件中，已经提出了一个表演算，它构成了一个决策过程的混合逻辑与逆向和全球的模态和限制使用的粘合剂。这项工作扩展了这样的演算多模态逻辑与传递关系和关系包含断言。单独添加传递关系或关系层次到所考虑的可判定片段的多模态混合逻辑可以很容易地保持可判定的，通过诉诸已经在文献中证明的结果。然而，这样的结果并不直接允许得出结论，包括这两个功能的逻辑是否仍然是可判定的。所考虑的逻辑的终止，声音和完整的演算的存在证明，除了传递关系和关系层次，这样一个表达的可判定的片段的混合逻辑产生可判定的逻辑。
2013-12-10 cs.LO math.LO
AC Simplifications and Closure Redundancies in the Superposition Calculus
结合性和交换性（AC）的存在下的推理是众所周知的挑战，由于这些公理的多产性。AC公理的专业化处理主要是由基于Knuth-Benzynn完备的单位等式证明器支持的。在这些验证器中处理AC的主要成分是适用于AC的地面可连接性标准。本文将AC可连接性从单位等式和Knuth-Beneficiary完备化推广到叠加演算和全一阶逻辑。我们的方法是基于扩展的Bachmair-Ganzinger模型建设和一个新的冗余标准，其中包括地面可连接性。我们的方法的一个副产品是一个新的标准，适用性的解调，我们称之为解调器解调。这个标准是有用的，在任何叠加定理证明，独立的AC理论，我们证明，它使解调在更多的情况下，相比标准标准。
2021-07-18 cs.LO
Guarded Negation Transitive Closure Logic
Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800（波尔多大学）；University of Buenos Aires（布宜诺斯艾利斯大学）；CONICET（阿根廷国家科学研究委员会）；Chiba University（千叶大学）
本文研究了guarded negation fragment of transitive closure logic (GNTC) 的可满足性问题，证明其为2ExpTime-完全，并展示了该逻辑的模型检查问题在组合复杂度下为P^NP[O(log^2 n)]-完全。
2026-07-21 cs.DB cs.LO
Undecidability of the Emptiness Problem of Deterministic Propositional While Programs with Graph Loop: Hypothesis Elimination Using Loops
本文证明带图循环的确定性命题while程序的空性问题不可判定且为 $\mathrmΠ^{0}_{1}$-完全，通过引入基于循环的假设消除方法从周期多米诺问题补问题进行归约，并进一步得出正关系演算等式理论的不可判定性及存在关系演算空性问题的 PSPACE-完全性。
2025-04-29 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
The Topological Mu-Calculus: completeness and decidability
我们研究了拓扑$μ$ -演算，基于Cantor导数和闭包模态，证明了在一般拓扑空间上，以及在$T_0$和$T_D$空间上的完备性、可判定性和FMP.我们还调查关系$μ$ -演算，提供一般完整性结果的所有自然片段的$μ$ -演算在许多不同类别的关系框架。与大多数其他这样的证明$μ$演算，我们是模型理论，使一个创新的使用已知的模态逻辑方法（-“最终”子模型的规范模型），具有极大的一般性和本质上的简单性的双重优势。
2021-05-18 cs.LO
A Cut-Free Sequent Calculus for the Analysis of Finite-Trace Properties in Concurrent Systems
University of Urbino Carlo Bo（乌尔比诺卡洛博大学）
本文提出了一种无切割的序数演算LMC，用于分析并发系统中有限迹性质，通过闭包ℓ-单形的代数抽象实现逻辑系统的正确性和完备性。
2025-12-05 cs.LO math.LO
Formal Small-step Verification of a Call-by-value Lambda Calculus Machine
我们正式验证一个抽象的机器调用的值的alcuda演算与de Bruijn条款，简单的替代，和小步语义。我们遵循逐步改进的方法，从一个带有替换的朴素堆栈机器开始。然后，我们细化到一个具有闭包的机器，最后是一个具有为闭包提供结构共享的堆的机器。我们证明了三个细化步骤的正确性与组成小步自下而上的模拟。有一个附带的Coq开发验证所有结果。
2019-01-02 cs.LO cs.PL
A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies (extended version)
在以前的作品中，已经定义了一个表演算，它构成了一个决策过程的混合逻辑与逆向和全球的模态和限制使用的粘合剂。这项工作展示了如何扩展这样的演算多模态逻辑丰富的功能主要用于描述逻辑：传递性和关系包含断言。单独添加传递关系或关系层次到所考虑的可判定片段的多模态混合逻辑可以很容易地保持可判定的，通过诉诸已经在文献中证明的结果。然而，这样的结果并不直接允许得出结论，包括这两个功能的逻辑是否仍然是可判定的。终止的存在，健全的和完整的演算所考虑的逻辑证明，除了传递关系和关系层次，这样一个表达的可判定的片段的混合逻辑不危及可判定性。在这项工作中证明的一个进一步的结果是，逻辑扩展所考虑的片段，除了分级模态（模态对应的数量限制的描述逻辑）有一个不可判定的可满足性问题，除非进一步的语法限制放置在通用分级模态。
2013-12-10 cs.LO
Query Answering with Transitive and Linear-Ordered Data
我们考虑蕴涵问题，涉及强大的约束语言，如守卫存在的规则，其中额外的语义限制放在一组杰出的关系。我们考虑限制一个关系是传递的，限制一个关系是另一个关系的传递闭包，限制一个关系是线性序。我们给出了一些自然的概括的guardedness，允许推断在每种情况下是可判定的，并隔离相应的决策问题的复杂性。最后，我们表明，轻微的变化，我们的条件导致不可判定性。
2016-07-04 cs.DB cs.LO
Spatial logic of modal mu-calculus and tangled closure operators
该研究将McKinsey和Tarski的拓扑模态逻辑成果拓展至模态μ演算与缠结算子逻辑，证明二者在拓扑空间上表达力等价，建立了相关逻辑的有限模型性质，拓展了剖分引理，得到多种语言在自稠密度量空间上的完备性与可靠性结果。
2016-03-05 cs.LO math.LO
On the enumeration of closures and environments with an application to random generation
本文研究λ-演算中环境和闭包的渐近计数与随机生成，针对朴素与封闭两类结构，利用生成函数构造有效采样器，并讨论封闭类的相关问题。
2019-10-16 cs.LO math.CO
Six Birds: Foundations of Emergence Calculus
Automorph Inc.（Automorph公司）
本文提出了一种跨学科的涌现演算，通过六个闭包变换原语统一序理论和动力学诱导的内射映射，并证明了在粗粒化下时间箭头函数的单调性及反饱和机制。
2026-01-28 cs.LO
The Limit of Recursion in State-based Systems
University of Gothenburg（哥德堡大学）
本文证明了ω^2严格界定模态可定义函数在可数结构上达到不动点所需的迭代次数，纠正并扩展了先前关于无交替μ-演算闭包序数的结论，通过引入保守良注释理论实现了直接且清晰的泵过程。
2025-11-04 cs.LO
$\aleph_1$ and the modal $μ$-calculus
本文研究模态 μ-演算公式的 κ-连续性，定义片段 C_ℵ₁(x)，证明其所有公式 ℵ₁-连续，并给出判定准则，进而刻画闭包序数，证明 ω₁ 是闭包序数且闭包序数对加法封闭。
2019-10-03 cs.LO math.LO
Query Answering with Transitive and Linear-Ordered Data
Télécom ParisTech（巴黎高等电信学院）；Université Paris-Saclay（巴黎萨克雷大学）；University of Oxford（牛津大学）；CNRS（法国国家科学研究中心）；Université Lille 1（里尔第一大学）；INRIA Lille（法国国家信息与自动化研究所里尔分部）
我们认为蕴涵问题涉及强大的约束语言，如边境守卫的存在规则，我们施加额外的语义限制一组杰出的关系。我们考虑限制一个关系是传递的，限制一个关系是另一个关系的传递闭包，限制一个关系是线性序。我们给出了一些自然的变体的guardedness，使推理在每种情况下是可判定的，并隔离相应的决策问题的复杂性。最后，我们表明，在这些条件的轻微变化导致不可判定性。
2022-02-17 cs.AI cs.DB cs.LO
Relational reasoning in the region connection calculus
本文主要研究著名的区域联络演算（RCC）的关系代数性质。我们证明了某些RCC模型的接触关系代数（CRA）不是原子完备的，因此是无限的。因此，一般情况下，RCC的延伸组成表不能通过简单地细化RCC8关系来获得。在证明了每个RCC模型都是RCC11 CT的一致模型之后，我们对RCC11 CT的外延解释进行了详尽的研究。更重要的是，我们证明了补闭圆盘代数是由RCC11表确定的关系代数的表示。这个代数的定义域包含两类区域，实平面中的闭圆盘和它们的补的闭包。
2005-05-14 cs.AI cs.LO
Combinatorics of explicit substitutions
$λ\upsilon$是$λ$ -演算的扩展，它内化了替换演算。在当前的文件中，我们调查的组合性质的$λ\upsilon$专注于定量方面的替代决议。我们表现出一个意想不到的计数序列之间的对应关系$λ\upsilon$ -条款和著名的加泰罗尼亚数字。作为一个副产品，我们建立了有效的随机$λ\upsilon$ -条款的抽样计划。我们表明，典型的$λ\upsilon$ -条款表示，在很强的意义上，在经典的$λ$ -演算的非严格计算。此外，典型地，几乎所有的替换实际上都在闭包下被暂停，即未被评估。因此，我们认为，$λ\upsilon$是一个内在的非严格演算的显式替换。最后，我们研究了$λ\upsilon$中控制替代分辨率的各种赎回权的分布，并研究了各种替代原语的定量贡献。
2018-04-11 cs.LO math.CO
Automated Synthesis of Tableau Calculi
本文提出了一种合成声音和完整画面的方法。给定逻辑的形式语义的规范，该方法生成一组可用于在逻辑内推理的tableau推理规则。该方法保证生成的规则形成一个演算，这是健全的和建设性的完整。如果逻辑可以被证明允许有限过滤相对于一个定义良好的一阶语义，然后添加一个通用的阻塞机制提供了一个终止表演算。生成tableau规则的过程可以完全自动化，并且与阻塞机制一起产生用于生成tableau决策过程的自动化过程。为了说明，我们显示的描述逻辑与传递角色和命题直觉逻辑的方法的可行性。
2012-04-23 cs.LO cs.SC
