Modeling and Verification of Infinite Systems with Resources
我们考虑资源消耗递归程序的形式化验证。我们引入前缀替换系统与非负整数计数器，可以增加和重置为零，作为一个正式的模型，这样的程序。在这些系统中，我们调查的可达性问题的资源消耗的界限。基于这个问题，我们引入了具有资源的关系结构和这些结构上的定量一阶逻辑。我们定义了资源自动结构作为这些结构的子类，并提供了一种有效的方法来计算这个子类上的逻辑的语义。随后，我们使用这个框架来解决资源前缀替换系统的有界可达性问题。我们实现了这一结果，通过扩展著名的饱和度的方法来注释前缀替换系统。最后，我们提供了一个连接到逻辑成本的研究-WMSO。
2013-12-14 cs.LO
A Generalization of the Łoś-Tarski Preservation Theorem
本文对每个自然数$k$，给出了一阶逻辑句子的前缀类$\exists^k \forall^*$和前缀类$\forall^k \exists^*$在所有有限和无限结构上的语义刻画。这个结果，我们称之为 * 广义的柯罗-塔斯基定理 *，缩写为$\mathsf{GLT}(k)$，当$k$等于0时，得到经典的柯罗-塔斯基保持定理。它还提供了新的表征的$Σ^0_2$和$Π^0_2$前缀类，这是比所有这些类在文献中的特征。此外，我们的语义概念是有限的性质，在文献中所包含的特征。在有限结构的背景下，我们制定了一个抽象的组合性质的结构，当满足一类，确保$\mathsf{GLT}(k)$持有类。这个性质，我们称之为 * 等价有界子结构性质 *，缩写为$\mathsf{EBSP}$，直观地说，一个大的结构包含一个小的“逻辑相似”的子结构。事实证明，这个简单陈述的属性被计算机科学中的各种感兴趣的类别所享有：例子包括单词，树（无序，有序或排名），嵌套单词，有界树深度/灌木深度的图形类，以及$m$ -partite上图。此外，$\mathsf{EBSP}$仍然保存在各种良好的研究操作，如互补，转置，线图操作，不相交的联盟，carnival和张量积等，这使得构建一个广泛的类，满足$\mathsf{EBSP}$，因此$\mathsf{GLT}(k)$。值得注意的是，$\mathsf{EBSP}$可以被视为经典向下…
2016-09-20 cs.LO
Reasoning in the Bernays-Schoenfinkel-Ramsey Fragment of Separation Logic
分离逻辑（SL）是一种众所周知的断言语言，用于具有动态分配的数据结构的程序的霍尔式模块化证明系统中。在本文中，我们研究的片段限制到Bernays-Schoenfinkel-Ramsey量词前缀$\exists^*\forall^*$，其中的量化变量的范围内的一组内存位置的一阶SL。当这个集合是未解释的（没有相关的理论）时，片段是PSPACE完备的，这与无量词片段的复杂性相匹配。然而，当量词前缀属于$\exists^*\forall^*\exists^*$时，或者当存储器位置被解释为具有线性算术约束的整数时，SL变得不可判定，从而为SL内的可判定性设置了清晰的边界。我们已经实现了一个决策程序的可判定片段的$\exists^*\forall^*$ SL作为一个专门的求解器内的DPLL（$T$）架构，在CVC 4 SMT求解器。我们的实现进行了评估，使用两组验证条件，产生（i）展开归纳谓词，和（ii）最弱的基于前置条件的验证条件生成器。实验数据表明，自动化的量词实例化具有很小的开销相比，手动基于模型的实例化。
2016-11-23 cs.LO
Semantics for Linear-time Temporal Logic with Finite Observations
本文通过确定性前缀集族为运行时验证逻辑 LTL3 建立完整的基于模型的归纳语义，证明其与传统 LTL 语义直接对应，并在 Isabelle/HOL 中形式化了公式进展求值技术及其在有限迹上的可靠性与完备性。
2024-11-21 cs.LO
A Generalization of the Łoś-Tarski Preservation Theorem - Dissertation Summary
本文简要介绍了作者的博士学位。论文（arXiv：1609.06297）。除了概述的概念和结果，它还提供了各种证明和简化介绍的论文，涉及树表示的结构的某些抽象结果的草图。此外，本文的一些结果的推广。其中包括论文中引入的模型理论概念与稀疏图类结构理论中的固定参数易处理性和概念之间的联系。论文的模型理论结果的证明的建设性方面被用来获得（算法）元内核的各种密集的图形，如有界的树的宽度和子类的这些像$m$ -particular上图和图形类的有界的灌木深度的图。最后，本文给出了关于逻辑分形概念的更新定义和结果，逻辑分形是本文中等价有界子结构性质的推广。特别是，我们的研究结果表明，（自然有限适应）的向上和向下版本的Löwenheim-Skolem定理从经典模型理论可以恢复在各种算法有趣的设置，并进一步在大多数情况下，在有效的形式，甚至超过一阶逻辑。
2018-11-02 cs.LO
Tree Languages Defined in First-Order Logic with One Quantifier Alternation
我们研究了可以在Δ_2中定义的树语言。这些是树型语言，可由一阶公式定义，其量词前缀为forall exists，同时也可由一阶公式定义，其量词前缀为。对于量词自由部分，我们考虑两个签名，要么后代关系单独或连同字典序关系在节点上。本文给出了在Δ_2中可定义的树语言和森林语言的一个有效刻画。这个特征是用代数方程表示的。在词上，可定义在Δ_2中的词语言类构成了鲁棒类，Pin和Weil给出了鲁棒类的一个有效的代数刻画。
2010-10-20 cs.FL cs.LO
Hereditary First-Order Logic: the tractable quantifier prefix classes
本文完整刻画了使遗传模型检测问题 Her$(ϕ)$ 属于 P 的一阶公式量词前缀类，并证明其余前缀类均为 coNP 完全，且该性质不可判定。
2025-07-03 cs.CC cs.DM cs.LO
Preservation theorems on sparse classes revisited
该研究重新审视稀疏结构类上一阶逻辑的同态保持定理，指出原有证明中可加性假设强度不足，构造了有界树宽的反例并证明平面图类不满足该性质，同时提出用瓶颈合并条件替代可加性以恢复证明有效性。
2024-05-20 cs.LO math.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
A Generalization of the Łoś-Tarski Preservation Theorem over Classes of Finite Structures
我们通过\emph{preservation under substructures modulo $k$-sized cores}的语义概念研究了一个推广的K-Tarski保持定理。前面已经指出，在任意结构上，一阶逻辑的这个语义概念对应于$\exists^k\forall^*$语句的可定义性。在本文中，我们确定了两个性质的类有限结构，确保上述对应关系。第一种是基于嵌入关系下的良拟序。第二个是一个基于逻辑的组合性质，严格概括了第一个。我们表明，从满足任何这些属性的类开始，通过应用不相交的工会，carnival和张量积等操作，或通过在类上形成单词和树，获得的类继承相同的属性。作为一个余波，我们得到有趣的类的结构，其中一个有效的版本，Tarski定理持有。
2014-01-23 cs.LO math.LO
Proofs and Refutations for Intuitionistic and Second-Order Logic (Extended Version)
证明演算是一种类型化的证明演算，它利用证明和反驳概念之间的对偶性为经典命题逻辑提供计算解释。在这项工作中，我们将扩展Euda-Euda，以包括经典的二阶逻辑，通过将参数多态性和存在类型。该系统具有良好的计算性能，如类型保持，汇合，和强规范化，这是建立在通过reductionalargument。我们确定了一个句法限制的证明，其特点正是直观的片段的二阶dupda-dupta，我们研究规范的结果。
2022-10-13 cs.LO
The Complexity of Prenex Separation Logic with One Selector
我们首先证明了具有$k\geq1$选择器域的分离逻辑（$\seplogk{k}$）的所有前向列公式的无限可满足性都可以化为有限可满足性。第二，我们表明，这需要的可判定性的有限和无限的可满足性问题的类前向公式的$\seplogk{1}$，减少到一阶理论的一元函数符号和一元谓词符号。我们还证明了复杂性不是初等的，通过减少从一元函数符号的一阶理论。最后证明了$\exists^*\forall^*$语言中带量词前缀的前趋$\seplogk{1}$公式的Bernays-Schönfinkel-Ramsey片段是\pspace -完全的.一个完整的（层次）分类的复杂性前束$\seplogk{1}$的定义，根据量词交替深度是一个悬而未决的问题。
2018-04-30 cs.LO
On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic
本文研究了$\exists^*\forall^*$语言中带有量词前缀的前向公式的分离合取和蕴涵无限制嵌套的分离逻辑在可能位置论域为可数无限或有限的情况下的可满足性问题.与带有未解释谓词和等式的一阶逻辑类似，我们称这个片段为伯奈斯-舍恩芬克尔-拉姆齐分离逻辑[BSR（SLk）]。我们表明，不同于在一阶逻辑中，（在）有限可满足性问题是不可判定的BSR（SLk），我们定义了两个非平凡的子集，这是可判定的有限和无限的可满足性，分别通过控制的范围内的普遍量化变量的出现分离的影响，以及后者的出现的极性。可判定性结果是通过分离连接词的受控消除获得的，描述为（i）将前束形式分离逻辑公式有效地翻译成少量\emph{test formulae}的组合，仅使用一阶连接词，随后（ii）将后者翻译成可均衡满足的一阶公式。
2018-02-16 cs.LO
Modal Logic via Global Consequence
在模态逻辑中，语义结果通常由所有模型中所有世界的真值保持局部定义（关于一类框架）。它也可以通过在所有模型中保持真值来全局定义（相对于一类框架）。后者被称为整体后果，这是远远低于标准的局部研究。本文首先研究了局部推论和整体推论之间的关系。然后给出了整体结果的一些对应结果。最后，结合形式语义学中的信息推理和更新推理，给出了全局推理的两个应用。本文中的一些结果是已知的，为了完整起见，将其收集在本文中。其他人似乎是新的。我们认为，整体结果不仅在理论上是有趣的，而且在应用上也是有用的。
2019-10-06 cs.LO math.LO
Finite model theory for pseudovarieties and universal algebra: preservation, definability and complexity
University of Melbourne（墨尔本大学）；La Trobe University（拉筹伯大学）
本文研究了有限模型理论与伪变种及普遍代数之间的关系，揭示了有限代数在公理化和可定义性方面的复杂性。
2026-02-10 cs.CC cs.LO math.LO
Proofs as Execution Trees for the π-Calculus
本研究基于演绎即计算范式，为π演算构建新型逻辑框架，通过扩展一阶乘法加法线性逻辑的无切割矢列式演算，将进程对应为公式、证明对应为计算，并设计证明网给出推导的典范表示。
2025-01-16 cs.LO
Lindstrom theorems for fragments of first-order logic
林斯特伦定理用模型论的条件来描述逻辑，如紧性和Löwenheim-Skolem性质。大多数现有的这类刻画关注一阶逻辑的扩展。但另一方面，与计算机科学相关的许多逻辑是一阶逻辑的片段或片段的扩展，例如，k变量逻辑和各种模态逻辑。寻找这些语言的Lindström定理可能具有挑战性，因为大多数已知的技术依赖于编码参数，这些参数似乎需要一阶逻辑的全部表达能力。本文给出了一阶逻辑的几个片段的Lindström定理，包括k>2的k-变量片段，Tarski关系代数，分次模态逻辑和二元保护片段。我们使用两种不同的证明技术。一个是对原始林斯特龙证明的修改。另一个涉及互模拟，树解开，有限深度的模态概念。我们的研究结果也暗示语义保持定理。
2009-08-04 cs.LO
Classical Higher-Order Processes
经典过程（CP）是一种演算，其中经典线性逻辑类型的证明理论与移动通道通信过程，一个la pi演算。它的结构建立在最近的命题作为类型之间的会话类型和线性逻辑命题的对应关系。期望的属性，如在约简和进展下的类型保持，来自线性逻辑的元理论。我们有助于这一研究线扩展CP代码的流动性。我们概括了经典的线性逻辑，以捕捉高阶（线性）推理的证明，这产生了一个逻辑重建（变种）的高阶π演算（HOPI）。由此产生的演算被称为经典高阶过程（CHOP）。我们探讨CHOP的元理论，证明其语义享有类型保护和进步（条款不卡住）。我们还说明了CHOP的表现力，通过例子，派生的语法糖，并扩展到多方会议。最后，我们定义了一个从CHOP到CP的翻译，它将进程代码的移动性编码为引用传递。
2018-02-08 cs.LO cs.PL
Parameterized Complexity of Elimination Distance to First-Order Logic Properties
到目标图性质P的消除距离是Bulian和Dawar提出的一个通用的图修改参数。我们开始研究消除距离的图形属性表示在一阶逻辑。我们划定问题的固定参数的易处理性，确定充分和必要条件的前缀结构的一阶逻辑公式。我们的主要结果是下面的元定理：- 对于可由一阶逻辑公式\in x_3表示的每个图形属性P，即，具有以下形式的图形属性P：\exists x_1 \exists x_2 \cdots \exists x_r \forall y_1 \forall y_2 \cdots \forall y_s \exists z_1 \exists z_2 \cdots \exists z_t，其中，x_1是无量词的一阶公式，检验一个图到P的消去距离是否不超过k，是用k参数化的固定参数易处理的。图的性质可以用图3中的公式表示，包括度有界、不包含禁止子图或包含有界支配集。我们通过证明这样的一般陈述不适用于具有稍微更有表现力的前缀结构的公式来补充这个定理：存在公式\in <$_3，其计算消除距离是W[2]-困难的。
2021-04-07 cs.CC cs.DM cs.DS
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
First-order Temporal Logic on Finite Traces: Semantic Properties, Decidable Fragments, and Applications
基于有限严格线性顺序的时态逻辑的形式主义，在文献中称为有限迹，已被用于自动规划，过程建模，（运行时）验证和程序合成中的时态规范，以及知识表示和推理。本文主要研究有限迹上的一阶时态逻辑。我们首先调查保存有限和无限的痕迹之间的公式的等价性和可满足性，通过提供一组语义和句法条件，以保证在这两种情况下推理之间的区别可以模糊。此外，我们表明，满足性问题的有限迹几个可判定的片段的一阶时序逻辑是ExpSpace完全的，在无限迹的情况下，而它减少到NExpTime有限迹有界的时刻数被认为是。这也导致了新的复杂性结果的时间描述逻辑在有限的痕迹。最后，我们调查应用程序的规划和验证，特别是通过建立连接的概念不敏感的无限性和安全性的文献。
2022-02-01 cs.LO
Positive first-order logic on words
我们研究FO+，一个片段的一阶逻辑有限的话，一元谓词只能出现积极的。我们表明，有一个FO-定义的语言，是单调的一元谓词，但不能定义FO+。这提供了一个简单的证明，林登的保存定理失败的有限结构。我们还表明，给定一个正则语言，它是不可判定的，它是否是在FO+定义。
2021-10-11 cs.FL cs.LO math.LO
Deciding First-Order Satisfiability when Universal and Existential Variables are Separated
本文引入了一个新的一阶逻辑等式可判定片段，它严格地推广了两个已知的一阶逻辑等式可判定片段--Bernays-Schönfinkel-Ramsey（BSR）片段和Monadic片段.定义原则是在原子水平上将普遍量化的变量与存在量化的变量句法分离。因此，我们的分类既不依赖于对量词前缀的限制（如在BSR的情况下），也不依赖于对谓词符号的arity的限制（如在一元的情况下）。我们证明了新的片段表现出有限模型的属性，并推导出一个非小学的计算时间上界所需的决定在新的片段满足。对于量词前缀为$\exists^* \forall^* \exists^*$的前趋句的子片段，可满足性问题被证明是NEXPTIME完备的。最后，我们讨论了如何自动推理程序可以利用我们的结果。
2016-06-20 cs.LO
Fusions of One-Variable First-Order Modal Logics
Birkbeck, University of London（伦敦大学伯贝克学院）；University of the Witwatersrand（威特沃特斯兰德大学）；University of Liverpool（利物浦大学）
研究单变量一阶模态逻辑独立融合的保持性，证明无等式时克里普克完全性和可判定性在全局与局部后承下保持，有等式时则不保持，并给出共享S5模态的充分条件。
2026-07-01 cs.LO
Existential and positive games: a comonadic and axiomatic view
本文将共单子方法从一阶逻辑扩展到存在性与正性片段，用路径嵌入刻画存在性片段保持性，并引入正互模拟刻画正性片段，从而给出多模态逻辑等资源 Lyndon 正性定理的新证明。
2025-05-06 cs.LO math.LO
Some Model Theory of Guarded Negation
保护否定片段（GNFO）是一阶逻辑的片段，包含所有的正存在公式，可以表达基本模态逻辑和许多描述逻辑的一阶翻译，以及数据库中出现的许多句子。它已被证明GNFO的语法是限制性的，使计算问题，如有效性和可满足性仍然是可判定的。这表明，尽管GNFO公式的表达能力很强，但它可以进行新的优化。本文研究GNFO公式的模型理论。我们的研究结果包括有效的保存定理GNFO，有效的克雷格插值和贝丝可定义性的结果，并能够表达一定的答案查询的一个大类的GNFO句子在非常有限的逻辑。这个版本的文件包含精简和更正版本的结果有关蕴涵的一个合取查询从一组地面事实和理论组成的GNFO句子的一种特殊形式（“依赖关系”）。
2020-05-14 cs.LO
An invitation to game comonads
本文概述博弈余单子框架，用范畴论方法统一刻画模型比较博弈与资源受限逻辑的保持性，并介绍其在同态计数、等资源保持定理及同伦论中的应用。
2024-06-30 cs.LO math.CT
Generalized Strong Preservation by Abstract Interpretation
标准的抽象模型检验依赖于抽象Kripke结构，该结构通过将不可区分的状态粘合在一起来近似具体模型，即通过具体状态空间的划分。规约语言L的强保持性描述了L中公式的具体和抽象模型检验的等价性。我们展示了如何抽象的解释可以用来设计抽象模型，更一般的抽象Kripke结构。相应地，强保持被推广到基于抽象解释的模型，并与抽象解释中的完整性概念精确相关。最小化精化抽象模型以使其对某种语言L强保持的问题可以表述为抽象解释中的最小域精化以获得w.r.t. L的逻辑/时态运算符。结果表明，这个精炼的强保持抽象模型总是存在的，并且可以被刻画为一个最大不动点。因此，一些著名的行为等价，如互模拟，模拟和口吃，以及它们相应的分区细化算法可以优雅地在抽象解释为完整性属性和细化。
2006-03-14 cs.LO cs.PL
Around Dot-depth One
点深度层次是无星语言的一种分类。它与有限词上一阶逻辑的量词交替层次有关。我们考虑通过禁止指定前缀或后缀获得的点深度为1/2和点深度为1的语言片段。事实证明，这些语言类与没有最小或最大谓词的存在一阶逻辑片段一一对应。对于所有的片段，我们得到有效的代数特征。此外，我们给出了新的组合证明的可判定性的成员问题的点深度1/2和点深度1。
2011-03-07 cs.FL cs.LO
Constructive Game Logic
游戏逻辑是一个很好的环境，通过将这些证明解释为程序来研究关于程序的证明，因为游戏的建设性证明对应于有效的获胜策略，以响应对手的行动。因此，我们开发的建设性的游戏逻辑扩展Parikh的游戏逻辑（GL）与建设性和一阶程序一个la普拉特的一阶动态逻辑（DL）。我们的主要贡献包括：1）一种新颖的可实现性语义，捕捉游戏的对抗动态，2）自然演绎演算和操作语义，通过证明术语描述策略的计算意义，以及3）理论结果，包括证明演算的合理性wrt可实现性语义、证明的操作语义的进展和保持、以及支持从游戏证明中提取计算工件的存在性属性。总之，这些结果提供了迄今为止任何程序逻辑的Curry-Howard解释的最一般的帐户，并且是游戏逻辑的第一个。
2020-07-22 cs.LO cs.PL
A Decidable Fragment of Second Order Logic With Applications to Synthesis
我们提出了一个片段的多排序的二阶逻辑称为EQSMT，并证明了在这个片段中的句子的可满足性检查是可判定的。EQSMT公式有一个$\exists^*\forall^*$量词前缀（在变量、函数和关系上），使EQSMT有利于建模综合问题。此外，EQSMT允许使用背景理论的组合进行推理，只要它们具有用于$\exists^*\forall^*$ FO片段的可判定可满足性问题（例如，线性算术）。我们的决策过程减少了EQSMT公式的可满足性查询的$\exists^*\forall^*$公式的每个单独的背景理论，使我们能够使用现有的高效SMT求解器支持$\exists^*\forall^*$推理这些理论，因此我们的程序可以被视为有效的量化SMT（EQSMT）推理。勘误表：我们修改了转换步骤-2（第9页），以纠正一个轻微的错误。此外，上述定理10的描述与公开版本不同。
2018-09-27 cs.LO cs.PL
The temporal logic of coalitional goal assignments in concurrent multi-player games
我们介绍和研究交替时间时序逻辑ATL的自然扩展，称为联盟目标的时序逻辑（TLCGA）。它的特点是只有一个，但很有表现力，联盟战略运营商，即联盟目标分配运营商，这是基于映射分配给游戏中的每组球员的联盟目标，形式化的TLCGA语言的路径公式，即一个公式前缀与时间运营商X，U，或G，代表相应的联盟的时间目标，描述满足该目标的策略的属性。建立了TLCGA的μ-演算扩展中时间目标分配的不动点刻画，讨论了它的表达性并举例说明，证明了它相对于适当定义的互模拟概念的互模拟不变性和Hennessy-Milner性质，构造了TLCGA的一个完善的公理系统，并通过有限模型性质得到了它的可判定性.
2022-02-22 cs.GT cs.LO cs.MA
Grafting Hypersequents onto Nested Sequents
本文提出结合嵌套序列与超序列的嫁接超序列框架，为K5、KD5等模态逻辑提供具备语法切消和最优复杂度证明搜索的新型演算。
2015-08-10 cs.LO math.LO
Unified Foundations of Team Semantics via Semirings
一阶逻辑的半环语义提供了一种跟踪模型表示的事实如何用于推导公式满足的方法。团队语义学是一个框架，用于研究在数据库、量子力学和统计学等不同背景下的依赖和独立逻辑，通过用描述变量之间依赖关系的原子扩展一阶逻辑。结合这两个，我们提出了一个统一的方法，通过一个新的半环团队语义，它包含了所有以前考虑的一阶团队语义的变体的依赖和独立的概念进行分析。特别地，我们研究了不同半环之间依赖关系和公式满足的保持性。此外，我们还创建了推理任务的链接，如出处，计数和修复。
2023-03-14 cs.DB cs.LO
Positive First-order Logic on Words and Graphs
本文研究有限词上一阶逻辑片段 FO+，证明存在单调但无法用 FO+ 定义的 FO 可定义语言，借此说明 Lyndon 保持定理在有限结构上失效，并将该结论推广至有限图，同时证明判断正则语言是否 FO+ 可定义的问题不可判定。
2023-07-24 cs.FL cs.LO math.LO
Presentation of a Game Semantics for First-Order Propositional Logic
博弈语义学的目的是通过将公式解释为博弈来描述证明的交互行为，在博弈中，证明诱导策略。在这篇文章中，我们介绍了一个一阶命题逻辑片段的博弈语义。在构建这样的语义时，必须面对的主要困难之一是通过描述可定义的策略（即实际上表现得像证明的策略）来使它们精确。这种表征通常是通过将模型限制为满足微妙组合条件（如无罪）的策略来完成的，这些条件在组合下的保留通常很难证明。在这里，我们提出了一个原始的方法来实现这一任务，需要结合游戏语义，重写理论和范畴代数的工具。我们介绍了一个图形表示的可定义的策略的发电机和关系的手段：这些战略可以产生从一个有限的一组“原子”的战略和平等的战略之间产生的这种方式承认有限的公理化。这些生成元满足双代数定律的一种变体，从而以一种干净和意想不到的方式桥接了代数和指称语义。
2008-05-07 cs.LO math.CT math.LO
On Testability of First-Order Properties in Bounded-Degree Graphs
我们研究属性测试的属性是可定义的一阶逻辑（FO）中的有界度图和关系结构模型。我们证明了任何由具有量词前缀$\exists^*\forall^*$的公式定义的FO属性都是可测试的（即，具有恒定查询复杂度的可测试），而存在可由具有不可测试的量词前缀$\forall^*\exists^*$的公式表示的FO属性。在稠密图模型中，一个类似的画面是众所周知的（阿隆，菲舍尔，Krivelevich，Szegedy，Combinatorica 2000），尽管这两个模型的性质非常不同。特别是，我们得到我们的下界的一阶公式，定义了一类有界度扩展，基于锯齿形产品的图形。我们希望这是独立的利益。然后，我们证明了一些一阶属性的可测性，讲同构类型的邻域，包括可测性的$1$ -邻域自由度，和$r$ -邻域自由度下一个温和的假设。
2021-01-07 cs.CC cs.DM cs.DS
