Multi-Structural Games and Beyond
本文分析多结构博弈与EF博弈的差异，提出量词-变量树博弈及句法博弈族，以同时刻画一阶逻辑的量词数、变量数等句法度量。
2024-12-21 cs.CC cs.LO
On the Number of Quantifiers Needed to Define Boolean Functions
本研究借助多结构博弈分析带序二进制串的一阶量词需求，提出并行对局技术，给出定义不同布尔函数所需量词的紧上界，含稀疏函数的优化结果，类似Lupanov上界。
2025-07-31 cs.CC cs.LO
A Double Team Semantics for Generalized Quantifiers
我们定义了基于双队的广义量词一阶逻辑的语义。我们还定义和研究了广义原子的概念。这样的原子可以用来定义具有基于团队的语义的一阶逻辑的扩展。我们还定义了一个游戏语义，并将其与双队语义进行了比较。
2017-08-31 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
A Higher-order Framework for Decision Problems and Games
我们引入了一个新的统一框架，决策问题和有限的游戏量化器和选择功能的基础上建模。我们表明，规范的效用最大化是一个量词的一个特殊情况下，我们更抽象的框架提供了几个额外的自由度建模。特别是，不完整的偏好，非最大化的竞争力，和上下文相关的动机时，可以考虑到描述一个代理的目标。我们介绍了一个合适的概括的纳什均衡的量词和选择功能的游戏。此外，我们引入了一个改进的纳什，捕捉上下文依赖的目标。在我们的框架中建模是组合的，因为游戏的各个部分是模块化的，可以很容易地交换。我们提供了一个扩展的例子，我们说明了概念，并强调了我们的替代建模方法的好处。
2014-09-25 cs.GT cs.LO math.LO
Prophecy Variables for Hyperproperty Verification
像HyperLTL这样的超属性的时态逻辑使用跟踪量词来表达与多个系统运行相关的属性。在实践中，这种规范的验证大多限于没有量词交替的公式，其中验证可以减少到检查系统的自组成上的跟踪属性。像$\forall π. \exists π'. ϕ$这样的量词替换可以通过互补来解决，也可以解释为$\forall$ -玩家和$\exists$-玩家之间的双人游戏，$\forall$ -玩家递增地构建轨迹$π$，$\exists$ -玩家以这样的方式构建$π'$，即$π$和$π'$一起满足$ϕ$。基于游戏的方法明显便宜但不完整，因为$\exists$玩家不知道$\forall$玩家的未来移动。在本文中，我们建立了游戏为基础的方法，可以通过添加（$ω$定期）时间预言完成。我们的证明是建设性的，产生一个有效的算法生成一套完整的预言。
2022-06-03 cs.CR cs.LO
A Sound, Complete and Effective Second Order Game Semantics
我们定义了一个游戏语义的二阶经典算术PA2（与量词谓词上的整数和充分的理解公理）。我们的语义是有效的：移动是由有限的信息量描述的，并且无论何时对于玩家而言存在某种获胜策略来捍卫公式的真实性，则存在某种原始递归获胜策略。然后，我们表明，我们的游戏语义是健全的和完整的真值分配的PA2公式。在我们的博弈模型中，谓词变量的值是某个“通用”博弈家族。这个值在游戏中是“未知的”，但在游戏结束时，它被“游戏裁判”用来决定谁是赢家。
2016-10-27 cs.LO
How to Win First-Order Safety Games
最近，一阶（FO）转换系统已经引起了人们的注意，用于验证参数系统，如网络协议，软件定义的网络或多代理工作流，如会议管理系统。这些系统的理想特性，如功能正确性或不干扰性，已方便地用公式表示为安全特性。为了自动合成策略，强制执行安全或不干涉，我们推广FO转换系统FO安全游戏。证明了有限对策中安全局中人获胜策略的存在性实际上等价于二阶量词消去。对于只包含一元谓词的FO游戏的重要情况，我们提供了可判定和不可判定情况的完整分类。对于非一元谓词的游戏，我们集中在通用的一阶不变量，因为这些都足以表达一大类的非干扰属性。基于一般技术的二阶量词消去，我们提供了抽象和细化技术，以综合FO战略，加强安全。我们证明了我们的方法的有用性，通过推断非平凡的FO规格的领导人选举协议，以及在会议管理系统中的文件分配，以排除不受欢迎的报告披露。
2019-11-14 cs.LO cs.MA
Existential and positive games: a comonadic and axiomatic view
本文将共单子方法从一阶逻辑扩展到存在性与正性片段，用路径嵌入刻画存在性片段保持性，并引入正互模拟刻画正性片段，从而给出多模态逻辑等资源 Lyndon 正性定理的新证明。
2025-05-06 cs.LO math.LO
Structure and Power: an emerging landscape
本文综述了范畴论工具在有限模型论、描述复杂性、约束满足和组合学中的应用，通过资源索引伴随族展开关系结构，恢复多种逻辑片段和组合参数，并揭示结构与逻辑计算可处理性之间的新兴景观。
2022-10-03 cs.LO
Who Wins the Multi-Structural Game?
本文研究多结构博弈的获胜判定问题，证明其为PSPACE难且属于NEXPTIME，同时解决了EF博弈难度与模式元数相关性的开放问题，结合了多种技术方法。
2025-07-31 cs.LO
A game comonadic account of Courcelle and Feferman-Vaught-Mostowski theorems
由Abramsky、Dawar和Wang提出，并由Abramsky和Shah发展的游戏comonads给出了模型比较游戏的范畴语义。我们提出了一个公理化的帐户Feferman-Vaught-Mostowski（FVM）组成定理的游戏comonad框架内，参数化的模型比较游戏。在一个统一的方式，我们产生的逻辑问题，其积极的存在和计数量词变体的组合性结果。其次，我们将游戏comonads扩展到二阶设置，特别是在一元二阶（MSO）逻辑的情况下。然后，我们推广我们的FVM定理的二阶情况。我们的结论与抽象的制定Courcelle的算法的元定理，利用我们早期的发展。这是实例化，以恢复著名的有界树宽度和有界cancelle宽度图上的MSO定理。
2022-05-11 cs.LO math.CT math.LO
Courcelle's Theorem - A Game-Theoretic Approach
库塞勒定理指出，在一元二阶逻辑中定义的每个问题都可以在线性时间内在有界树宽的结构上得到解决，例如，通过构造一个树自动机来识别或拒绝结构的树分解。现有的优化软件（如MONA工具）可以用来构建相应的树自动机，对于有界树宽，树自动机的大小是恒定的。不幸的是，所涉及的常数可能会变得非常大-每个量词交替都需要为自动机构造幂集。这里，所需的空间在实际应用中可能成为问题。在本文中，我们提出了一种新的，直接的方法基于模型检验游戏，它避免了昂贵的权力集的建设。实现的实验是有希望的，我们可以解决自动机理论方法在实践中失败的图上的问题。
2011-04-19 cs.DS cs.GT cs.LO
Upper Bounds on the Quantifier Depth for Graph Differentiation in First-Order Logic
该论文证明二维 Weisfeiler-Leman 算法在 n 顶点图上稳定所需迭代次数为 O(n^2/log(n))，改进了平凡上界，并由此导出 C3 与 L3 逻辑中量词深度的对应上界。
2019-05-26 cs.CC cs.LO math.CO
The pebbling comonad in finite model theory
Pebble博弈是有限模型理论、约束满足和数据库理论研究的有力工具。单子和共单子是范畴论的基本概念，广泛应用于计算语义学和现代函数式程序设计中。我们证明了存在的k-pebble游戏有一个自然的共单因子公式。在k-卵石博弈中，复制者在结构A和B上的获胜策略等价于在coKleisli范畴中从A到B的态射。这导致了有限模型理论中一些中心概念的共单特征：-共Kleisli范畴中的同构特征了k变量逻辑中的初等等价与计数量词。- 对称游戏对应的等价全k-变量逻辑的特点。- 一个结构A的树宽的特征在于它的余代数数：最小的k，其中有一个余代数结构的A上的k-卵石comonad。- Co-Kleisli态射被用来刻画强一致性，并给出一个Cai-Fürer-Immerman结构的解释。- k-pebbling comonad也被用来给一个新的模态算子的语义。这些结果为计算机科学逻辑中的两个领域之间一些新的且有前途的联系奠定了基础，这两个领域在很大程度上是不相交的：（1）有限和算法模型理论，以及（2）计算的语义和范畴结构。
2017-04-17 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
On Finding a First-Order Sentence Consistent with a Sample of Strings
我们研究以下问题：给定一个分类字符串的样本，找到一个与样本一致的最小量词秩的一阶句子。我们将字符串表示为后继字符串结构，即用一元谓词表示字母表中的符号的有限结构和后继关系。我们使用的结果Escherichfeucht-Fraïssé游戏的后续字符串结构，以设计一个算法来找到这样的句子。我们使用的条件特征的获胜策略的剧透继承字符串结构，以定义公式区分两个字符串。我们的算法返回这样的公式的布尔组合。
2018-09-10 cs.LO
On the Theory of Structural Subtyping
我们证明了非递归类型的结构子类型的一阶理论是可判定的。设$Σ$是一种由函数符号（表示类型构造函数）组成的语言，$C$是关系语言$L$中包含二元关系$\leq$的可判定结构。$C$表示基本类型; $\leq$表示子类型排序。我们引入了$Σ$-$C$的项幂的概念，它概括了结构子类型中出现的结构。$C$的$Σ$ -项-幂的域是$C$的元素集合上的$Σ$ -项的集合。我们证明了$C$的一阶理论的可判定性意味着$C$的$Σ$ -项-幂的一阶理论的可判定性。我们的决策过程中使用的量词消去的项代数和Feferman-Vaught定理。我们的结果暗示了非递归类型的结构子类型的一阶理论的可判定性。
2004-08-05 cs.LO cs.PL cs.SE
A duality theoretic view on limits of finite structures
Nesetril和Ossona de Mendez发展了有限模型结构极限的系统理论。它是基于这样的见解，即有限结构的集合可以通过他们称为Stone配对的映射嵌入到测量空间中，在那里可以计算出所需的限制。我们表明，一个密切相关的，但更细粒度的措施空间出现--通过斯通-普里斯特利对偶和模型理论的类型的概念--通过丰富的表达能力的一阶逻辑与某些“概率算子”。我们提供了一个健全的和完整的演算，这个扩展的逻辑，并揭示了这个建设的函子性质。其后果是双重的。一方面，我们确定了结构极限理论的逻辑依据。另一方面，我们的建设表明，二重性理论的斯通配对的变体捕获添加一层量词，从而使一个强有力的链接到最近的工作半环量词在逻辑上的话。在这个过程中，我们将类型的模型论概念确定为这一联系背后的统一概念。这些结果有助于弥合链的逻辑在计算机科学侧重于语义和算法和复杂性相关的领域，分别。
2020-01-07 cs.FL cs.LO math.LO
Ehrenfeucht-Fraïssé Games in Semiring Semantics
本文研究半环语义下Ehrenfeucht-Fraïssé博弈的可靠性与完备性，分析其在特定半环上的适用条件，并提出基于同态到布尔半环的新型同态博弈，证明其对有限和无限格半环上的逻辑等价是可靠且完备的。
2023-08-09 cs.DB cs.LO math.LO
The Structure of First-Order Causality
博弈语义学通过将公式解释为博弈来描述证明的交互行为，在博弈中，证明诱导策略。这样的语义在这里引入捕获的依赖关系引起的量化一阶命题逻辑。在阐述这种语义时必须面临的主要困难之一是描述可定义策略的特征，即实际上表现得像证据的策略。这通常是通过将模型限制为满足微妙组合条件的策略来实现的，这些条件在组合下的保持性通常很难表现出来。在这里，我们提出了一个原始的方法来实现这一任务，这需要结合先进的工具，从游戏语义，重写理论和范畴代数。我们介绍了一个图表表示的monoidal类别的可定义的战略，我们的模型，通过发电机和关系：这些战略可以产生从一个有限的原子战略和战略之间的平等承认有限的公理化，这个方程结构对应的极化变化的概念双代数。因此，这项工作的桥梁代数和指称语义，以揭示一阶量词诱导的依赖关系的结构，并奠定了基础，在程序设计语言的因果关系的机械化分析。
2009-08-27 cs.LO math.CT math.LO
A Logic that Captures $β$P on Ordered Structures
我们扩展了膨胀不动点逻辑，IFP，与一种新的二阶量词有（多）对数界。我们证明，在有序结构的新逻辑$\exists^{\log^ω}\text{IFP}$捕获有限的非确定性类$β\text{P}$。为了研究它的表达能力，我们还设计了一个新的Escherichfeucht-Fraïssé博弈，并证明了我们的捕获结果在一般情况下，即在所有有限结构上都不成立.
2022-09-06 cs.CC cs.LO math.LO
The Structure of First-Order Causality (extended version)
博弈语义学通过将公式解释为博弈来描述证明的交互行为，在博弈中，证明诱导策略。这样的语义在这里引入捕获的依赖关系引起的量化一阶命题逻辑。在阐述这种语义学的过程中，必须面对的主要困难之一是描述可定义的策略，即实际上表现得像证明的策略。这通常是通过将模型限制为满足微妙组合条件的策略来实现的，这些条件在组合下的保持性通常很难表现出来。在这里，我们提出了一个原始的方法来实现这一任务，这需要结合先进的工具，从游戏语义，重写理论和范畴代数。我们介绍了一个图表表示的monoidal类别的可定义的战略，我们的模型，通过发电机和关系：这些战略可以产生从一个有限的原子战略和战略之间的平等承认有限的公理化，这个方程结构对应的极化变化的概念双代数。因此，这项工作的桥梁代数和指称语义，以揭示一阶量词诱导的依赖关系的结构，并奠定了基础，在程序设计语言的因果关系的机械化分析。
2011-01-25 cs.GT cs.LO math.CT
A duality theoretic view on limits of finite structures: Extended version
本文通过Stone-Priestley对偶和概率算子扩展一阶逻辑，构建更细粒度测度空间，揭示结构极限理论的逻辑本质，并连接半环量词研究。
2022-01-17 cs.LO math.LO
A categorical account of composition methods in logic
本文扩展博弈余单子语义，建立有限模型理论复合方法的统一范畴论框架，参数化导出 FVM 型定理并恢复、改进多项经典结果。
2023-04-24 cs.LO math.CT
