Monadic second order finite satisfiability and unbounded tree-width
Seese（1991）的经典结果证明了一元二阶逻辑的有限可满足性问题只能在有界树宽的结构类上判定。本文证明了以下问题是可判定的：输入：（i）一元二阶逻辑语句$α$，（ii）一个语句$β$，该语句在一阶逻辑的两变量片段中扩展为计数量词. $α$和$β$的词汇表可以相交。输出量：是否存在满足$α\landβ$的有限结构，使得该结构对$α$的词汇表的限制具有有界树宽？(The所需结构的树宽度不受限制）。因此，我们证明了可满足性问题的可判定性的有限结构的有界树宽度的逻辑扩展一元二阶逻辑的线性基数约束的形式$|X_{1}|+\cdots+|X_{r}|<|Y_{1}|+\cdots+|Y_{s}|$，其中$X_{i}$和$Y_{j}$是一元二阶变量。我们证明了WS1S的一个类似的扩展的可判定性。
2016-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 Pseudofinite Monadic Second Order Theory of Linear Order
一元二阶逻辑是一阶逻辑在一元关系上的量词的扩展。本文利用一阶设置研究了有限线性序的共享一元二阶理论，即线性序的伪有限一元二阶理论。我们给出了明确的（和递归的）公理和剩余序列的完成。一个连接profinite代数，特别是与自由profinite幺半群上的一个发电机，建立通过扩展斯通对偶。
2021-05-25 cs.FL cs.LO math.LO
Weak Mso with the Unbounding Quantifier
本文引入了一类新的无限词语言，称之为极大正则语言，它是对$ω$ -正则语言类的扩充.这个类有两个等价的描述：自动机（一种确定性计数器自动机）和逻辑（带有边界量词的弱一元二阶逻辑）。给出了逻辑和自动机之间的有效转换。
2009-02-06 cs.FL cs.LO
The pseudofinite monadic second order theory of words
我们分析了在一个固定的有限字母表的伪有限单子二阶理论的话。特别是，我们提出了一个公理化的理论，工作在一个排序的一阶框架。分析取决于这样一个事实，即串联的话很好地互动与一元二阶逻辑。更确切地说，给出一个签名，在该签名下，对于每个自然数k，关于量词深度至多为k的公式的词（的一元二阶版本）的等价性是拼接的同余。我们使用我们的分析，提出了一个定理的另一种证明，通过扩展的斯通对偶，由于格尔克，格里戈里耶夫，和引脚连接可识别的语言和生成的自由profinite幺半群。
2022-03-11 cs.LO math.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
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
The MSO+U theory of (N, <) is undecidable
我们考虑逻辑MSO+U，这是一元二阶逻辑与无界量词扩展。无界量词用来表示有限集合的一个性质对任意大的集合都成立。证明了该逻辑在无限词上是不可判定的，即（N，<）的MSO+U理论是不可判定的.这解决了有关逻辑的一个悬而未决的问题，并改进了之前的不可判定性结果，该结果使用了无限树和集合论中的附加公理。
2015-02-17 cs.LO
Ramsey Quantifiers in Linear Arithmetics
本研究提出一种可从LIA、LRA、LIRA三种线性算术SMT理论中消除拉姆齐量词的多项式时间算法，解决了相关良基性检查、一元可分解性等开放问题，并在原型测试中取得良好效果。
2023-11-07 cs.FL cs.LO
Alternating Set Quantifiers in Modal Logic
我们建立了严格的几个设置量词交替层次结构的模态逻辑的基础上，评估各类有限图。这延伸到模态设置Matz，Schweikardt和Thomas（2002）的著名结果，该结果指出一元二阶逻辑的类似层次是严格的。因此，本文解决了van Bentham（1983）提出的一个问题，ten Cate（2006）重新提出了这个问题，Kuusisto（2008，2015）对此做了部分回答。
2016-02-29 cs.FL cs.LO math.LO
Weighted Automata and Monadic Second Order Logic
设S是交换半环。M. Droste和P.Gastin在2005年引入了加权一元二阶逻辑WMSOL，其权在S。他们使用WMSOL的语法片段RMSOL来表征加权自动机可识别的词函数（幂级数），其中量词的语义既用作算术运算，又在布尔情况下用作量化。早在2001年，B. Courcelle、J.Makowsky和U. Rotics已经引入了一种形式主义，用于在Monadic二阶逻辑中定义的图参数，这里称为MSOLEVAL，其值在环R中。它们的框架可以很容易地适应于半环S。这种形式主义清楚地将逻辑部分与算术部分分开，并且也适用于词函数。本文给出了两个证明：值在S中的RMSOL和MSOLEVAL对词具有相同的表达能力。一个证明直接表明，MSOLEVAL捕获的功能可识别的加权自动机。另一个证明展示了如何将形式主义从一个转换成另一个。
2013-07-17 cs.FL cs.LO
Heinrich Behmann's Contributions to Second-Order Quantifier Elimination from the View of Computational Logic
Technische Universität Dresden（德累斯顿工业大学）
对于关系一元公式（Löwenheim类），二阶量词消去，这是密切相关的计算一致插值，投影和遗忘-操作，目前受到关注的知识处理-总是成功的。Heinrich Behmann从1922年开始对这个类的可判定性证明是通过等价保持公式重写的消元法进行的。在这里，我们重建的结果从Behmann的出版物的详细和讨论相关的问题，在现代方法的背景下，二阶量词消去在计算逻辑。此外，广泛的文件的信件和手稿在贝曼的遗赠，关注二阶量词消去，包括一个评论登记册和英文摘要的德语来源，重点是技术材料。在20世纪20年代后期，Behmann试图为谓词的元数大于1的公式开发一种基于消除的决策方法。他的手稿和与威廉·阿克曼的通信显示了今天仍然感兴趣的技术方面，并深入了解了阿克曼1935年的里程碑式论文“Untersuchungen über das Eliminationsproblem der mathematischen Logik”的起源，该论文奠定了两种流行的现代二阶量词消去方法的基础。
2017-12-19 cs.AI cs.LO
Flavors of Quantifiers in Hyperlogics
本文扩展超迹逻辑，引入约束与无约束两类迹量词，研究其不同模式对可满足性判定性的影响，证明若干片段等价于S1S或HyperQPTL，并给出新的可判定与不可判定结果。
2025-10-14 cs.FL cs.LO
Order-Invariant MSO is Stronger than Counting MSO in the Finite
我们比较了一元二阶逻辑（MSO）的两个扩展在有限结构类上的表现力。第一个是计数一元二阶逻辑（CMSO），它用一阶模计数量词扩展了MSO，允许表达像“结构中元素的数量是偶数”这样的查询。第二个扩展允许使用一个额外的二进制谓词，不包含在查询结构的签名中，必须解释为在其宇宙中的任意线性顺序，获得顺序不变的MSO。虽然每一个CMSO公式都可以直接转化为一个等价的阶不变MSO公式，但其逆命题尚未解决。Courcelle证明了对于有限类的结构，序不变的MSO和CMSO都具有同样的表达能力，但他强调，一般来说，序不变的MSO比CMSO更强。我们肯定了这一猜想，提出了一类结构，是顺序不变的定义在MSO，但不能定义在CMSO。
2008-03-20 cs.LO
Succinctness of Order-Invariant Logics on Depth-Bounded Structures
研究了一阶逻辑和一元二阶逻辑的序不变句在有界树深结构上的表达能力和简洁性。一般来说，顺序不变是不可判定的，因此，人们努力寻找具有与顺序不变句子相同的表达能力的可判定语法的逻辑。我们表明，在有界树深度的结构，顺序不变的FO具有相同的表达能力FO。我们的证明技术允许对这种翻译的简洁性进行细粒度的分析。我们证明了，对于每一个顺序不变的FO句子存在一个FO句子，其大小是小学的原始句子的大小，其数量的交替是线性的树深度。我们得到类似的结果MSO。MSO和FO的表达能力在有界树深结构上是一致的。我们提供了一个翻译MSO FO，我们表明，这种翻译基本上是最佳的公式大小。作为进一步的结果，我们表明，顺序不变的MSO具有相同的表达能力，FO与有界树深度结构上的模计数量词。
2016-03-30 cs.LO
Weak MSO: Automata and Expressiveness Modulo Bisimilarity
证明了弱一元二阶逻辑的互模拟不变片段等价于模态$μ$ -演算的片段，其中最小不动点算子$μp.φ$的应用仅限于在$p$中连续的公式$φ$.我们的证明是自动机理论的性质，特别是，我们引入了一类自动机的特点的表达能力的WMSO树模型的任意分支度。这些自动机的转换映射是根据逻辑$\mathrm{FOE}_1^\infty$定义的，该逻辑是具有广义量词$\exists^\infty$的一阶逻辑的扩展，其中$\exists^\infty x. ϕ$意味着有无限多个对象满足$ϕ$。我们的工作的一个重要组成部分是$\mathrm{FOE}_1^\infty$的模型理论分析。
2014-01-22 cs.LO
Subshifts, MSO Logic, and Collapsing Hierarchies
我们使用一元二阶逻辑来定义二维子移位，或无限平面的着色集。我们提出了一个自然的家庭的量词交替层次结构，并表明，他们都崩溃到第三级。特别是，这解决了[Jeandel & Theysier 2013]的一个开放问题。这一结果与图画语言形成了鲜明的对比，图画语言的层次结构通常是无限的。
2014-06-27 cs.FL cs.LO math.DS
Connection Matrices and the Definability of Graph Parameters
本文推广并详细证明了B. Godlin，T. Kotek和J.A. Makowsky（2008）和J.A. Makowsky（2009）.我们证明了它的巨大的适用性，在简化已知的和新的不可定义的结果的图形属性，并找到新的不可定义的结果的图形参数。我们还证明了一个Feferman-Vaught定理的逻辑CFOL，一阶逻辑与模计数量词。
2014-10-27 cs.LO math.CO
Refinement Modal Logic
Universidad Politécnica de Madrid（马德里理工大学）；LORIA, CNRS – Université de Lorraine（洛林计算机科学与应用数学实验室（法国国家科学研究中心-洛林大学））；University of Western Australia（西澳大利亚大学）；IRISA, University of Rennes（雷恩大学计算机科学与随机系统研究所）
本文提出了{ \em精化模态逻辑}。精化类似于互模拟，不同之处在于从三个关系需求中只需要满足“原子”和“返回”。我们的逻辑包含一个新的操作符“所有”除了标准的模态“框”为每个代理。运算符“all”充当给定模型的所有细化的集合上的量词。作为互模拟量词的一种变体，这个精化运算符或精化量词“all”可以被看作是对一个没有出现在它所约束的公式中的变量进行量化。这种逻辑结合了多智能体模态逻辑的简单性和一元二阶量化的一些能力。我们提出了一个健全的和完整的公理化的多智能体精化模态逻辑。我们还提出了一个扩展的逻辑模态μ演算，和公理化的单代理版本的这个逻辑。例子和应用程序也进行了讨论：软件验证和设计（一套代理也可以被看作是一套行动），并动态认知逻辑。我们进一步给出了详细的结果，可满足性的复杂性，简洁性。
2013-12-25 cs.AI cs.LO
Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA
模态公式表示Kripke框架上的一元二阶性质，但在许多重要情况下，它们具有一阶等价物。计算这样的等价物对于逻辑和计算原因都是重要的。另一方面，模态公式的规范性也很重要，因为它意味着用规范公式公理化的逻辑的框架完备性。计算一个模态公式的一阶等价等价物相当于消除二阶量词。二阶量词消去有两种算法：基于约束消解的SCAN算法和基于Ackermann建立的逻辑等价的DLS算法。在本文中，我们介绍了一种新的算法，SQEMA，计算一阶等价物（使用阿克曼引理的模态版本），而且，用于证明规范的模态公式。与SCAN和DLS不同，它直接作用于模态公式，从而避免了Skolemization和随后的unskolemization问题。我们提出的核心算法，并说明它与一些例子。然后，我们证明了它的正确性和规范的所有公式上的算法成功。我们表明，它不仅成功的所有Sahlqvist公式，但也对更大的类的归纳公式，在我们以前的论文中介绍。因此，我们开发了一种纯粹的算法方法来证明模态逻辑中的规范完备性，特别是，建立了模态逻辑中迄今为止最普遍的完备性结果之一。
2006-03-08 cs.LO
Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness (Extended Preprint)
University of Bamberg（班贝格大学）；Freie Universität Berlin（柏林自由大学）
在Isabelle/HOL中为MSO开发三种嵌入，提出两类替换机制实现自动化忠实性，并机械化证明向下Loewenheim-Skolem定理，区分一般与标准解释，通过经典例子展示差异。
2026-09-23 cs.AI cs.LO math.LO
An algebraic approach to MSO-definability on countable linear orderings
我们开发了一个代数概念的可识别性语言的词索引可数线性排序。我们证明了这个概念是有效的等价于一元二阶（MSO）逻辑中的可定义性。我们还提供三个逻辑应用程序。首先，我们建立了可数线性序上MSO逻辑的量词交替的第一个已知的崩溃结果。第二，我们解决了一个公开的问题，由古列维奇和Rabinovich，关于MSO-可定义的集合的有理数使用的实数的背景。第三，我们建立了一个MSO-可定义的树集诱导的产量集的MSO-可定义性，证实了Bruy{è}re，Carton和S{é}nizergues提出的一个猜想。
2018-05-29 cs.FL cs.LO
Interleaving Logic and Counting
本文研究自然语言推理中逻辑与计数的结合，通过带计数的单子一阶逻辑及其强化形式，分析可定义性、公理化与可判定性，并联系语言量词和认知科学。
2025-07-07 cs.CL cs.LO math.LO
On the First-Order Complexity of Induced Subgraph Isomorphism
本文研究诱导子图同构的一阶复杂度参数W[F]，证明爪图W[K_3+e]=3，4顶点图除爪图及其补图外W[F]=4，并给出W[F]>(1/2-o(1))t的一般下界，同时展示W*[F]可严格小于W[F]，并得到一元二阶逻辑的简洁性结果。
2019-03-05 cs.CC 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
Algebraic semantics for one-variable lattice-valued logics
任何一阶逻辑的单变量片段都可以被认为是模态逻辑，其中全称量词和存在量词分别被盒模态和菱形模态所取代。在一些情况下，这些逻辑的代数语义的公理化已经得到：最值得注意的是，分别为一阶经典逻辑和直觉主义逻辑的单变量片段的模态对应物S5和MIPC。然而，在一阶中间逻辑的设置之外，缺乏一种通用的方法。本文提供了这样一种方法的基础上设置的一阶格值逻辑，其中公式解释的代数结构与格约简。特别是，公理化得到的模态对应的一个广泛的家庭这些逻辑的一个变量片段通过推广的功能表示定理Bezhanishvili和哈丁一元Heyting代数。一个替代的证明理论的证明也提供了一个变量片段的一阶子结构逻辑，有一个切自由的插值演算，并承认一定的有界插值性质。
2022-09-18 cs.LO math.LO
One-dimensional fragment of first-order logic
本文提出了一种新的一阶逻辑的可判定片段。片段是一维的，在这个意义上，量化是有限的存在（通用）量词块的应用程序，使最多一个变量保持自由的量化公式。片段在布尔运算下是封闭的，但额外的限制（称为一致性条件）适用于具有两个或更多变量的原子公式的组合。我们认为，一维性和一致性的概念一起提供了一个新的视角的鲁棒判定的模态逻辑。我们还建立了轻微的修改的限制的语法的一维片段导致不可判定的形式主义。也就是说，二维和非均匀的一维碎片被证明是不可判定的。最后，我们证明了在表达性方面，一维片段与守护否定片段和带计数的二元逻辑是不可比拟的。我们证明的一维片段的可判定性是基于一种技术，涉及直接减少到一元类的一阶逻辑。新技术本身是一个独立的数学兴趣。
2014-04-15 cs.LO math.LO
Undecidable propositional bimodal logics and one-variable first-order linear temporal logics with counting
一阶时态逻辑因其糟糕的计算行为而臭名昭著。众所周知，即使是两个变量的一元片段在各种线性时间线上也是高度不可判定的，并且在分支时间上，即使是一个变量的片段也可能是不可判定的。然而，已经有几个试图找到良好的一阶时序逻辑和相关的时序描述逻辑的片段，主要是通过限制可用的量词模式，或考虑子布尔语言。在这里，我们分析看似“温和”的扩展可判定的一个变量的片段与计数能力，解释模型与恒定，减少，扩大一阶域。我们表明，在大多数类的线性订单，这些逻辑是（有时高度）不可判定的，即使没有常数和函数符号，并与唯一的时间运营商“最终”。我们建立连接与双峰逻辑在二维产品结构具有线性和“差异”（不等式）组件的关系，并证明我们的结果在此双峰设置。我们给出了一个普遍的结果，即许多具有可交换线性和差分关系的双峰模型的可满足性是不可判定的。作为一个副产品，我们还获得了新的例子，但Kripke不完全双峰逻辑的axiomatisable。我们的结果推广了双峰逻辑在两个线性关系的乘积上的类似下界，并且我们的证明方法与这些结果的证明有很大的不同。与以前的证明，第一个“对角编码”的无限网格，然后使用减少平铺或图灵机的问题，在这里，我们直接使用的网格状结构的产品框架，并获得undecidability减少计数器（明斯基）机的问题。
2015-06-08 cs.LO
Bundled fragments of first-order modal logic: (un)decidability
Institute of Mathematical Sciences, Homi Bhabha National Institute（数学科学研究所，霍米·巴巴国家研究所）；Peking University（北京大学）
量化模态逻辑为模态态度的推理提供了一种自然的逻辑语言，即使在保留量化的丰富性的同时，也可以引用域上的谓词。但是，在许多模型类上，逻辑的大多数片段都是不可判定的。多年来，只有少数片段（例如单声部）被证明是可判定的。在本文中，我们研究的片段，捆绑量词和模态在一起，知识/为什么/什么的认知逻辑的早期工作的启发。与量化模态逻辑一样，域是否在世界上保持相同会产生重大差异。特别是，我们表明，束$\forall \Box$是不可判定的恒定域的解释，即使只有一元谓词，而$\exists \Box$束是可判定的。另一方面，在增加域解释，我们得到的可判定性与$\forall \Box$和$\exists \Box$束与不受限制的谓词。在这些情况下，我们还获得了在\PSPACE中运行的基于tableau的过程。我们进一步表明，$\exists \Box$束不能区分恒定域和增加域的解释。
2018-03-28 cs.AI cs.LO math.LO
Existential Second-Order Logic Over Graphs: A Complete Complexity-Theoretic Classification
描述复杂性理论旨在从问题描述的句法复杂性推断问题的计算复杂性。这个理论的一个基石是费金定理，通过这个定理，一个图的性质在存在二阶逻辑（ESO逻辑）中是可表达的，当且仅当它是NP。从理论的观点来看，一个自然的问题是ESO逻辑的哪些句法片段仍然表征NP。Gottlob、Kolatis和Schwentik对这个问题的研究最终得出了一个二分法的结果：对于ESO公式的每个可能的量词前缀，所得到的前缀类要么包含NP完全问题，要么包含在P中。在本文中，我们通过证明对于ESO逻辑的每个前缀类，其在一阶约简下的约简闭包是FO，L，NL或NP来澄清这一情况。对于无向无环图，两个包含结果特别具有挑战性：包含在L中的前缀$\exists R_1 \cdots \exists R_n \forall x \exists y$和包含在FO中的前缀$\exists M \forall x \exists y$的一元$M$。Gottlob、Kolatis和Schwentick关于多项式时间的复杂论证需要仔细地重新审视，或者与Courcelle定理的对数空间版本相结合，或者直接改进为一阶计算。一个不同的挑战是由前缀$\exists M \forall x\forall y$的公式：我们表明，他们表示特殊的约束满足问题，位于L。
2014-12-19 cs.CC cs.LO
