Monadic Second Order Logic with Measure and Category Quantifiers
Matteo Mio, Michał Skrzypczak, Henryk Michalewski
本文研究了在无限词和树上，将一元二阶逻辑扩展为带有基于贝尔范畴和勒贝格测度的广义“几乎全部”量词，探讨其表达能力和性质。
我们研究了一元二阶逻辑在无限词和树上的扩展，该扩展引入了广义的“几乎全部”量词，这些量词分别基于贝尔范畴和勒贝格测度的概念进行解释。
We investigate the extension of Monadic Second Order logic, interpreted over infinite words and trees, with generalized "for almost all" quantifiers interpreted using the notions of Baire category and Lebesgue measure.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
On Second-Order Monadic Monoidal and Groupoidal Quantifiers
我们研究逻辑定义的二阶monadic monoidal和groupoidal量词。这些都是广义量词定义的幺半群和广群字的问题，等价地，由正规和上下文无关的语言。我们给出了一个计算分类的表达能力，这些逻辑字符串不同的内置谓词。特别是，我们表明，ATIME（n）可以在逻辑上的特点是在二阶monadic monoidal量词。
Model Theory of Monadic Predicate Logic with the Infinity Quantifier
本文建立了模型理论性质的$\mathrm{FOE}^{\infty}$，一元一阶逻辑的变化，具有广义量词$\exists^\infty$（“有无限多”）。我们提供了语法定义的片段$\mathrm{FOE}^{\infty}$表征四个不同的语义属性的$\mathrm{FOE}^{\infty}$ -句子：（1）是单调的和（2）（斯科特）连续在一个给定的一元谓词集;（3）有真理下保持采取子模型或（4）不变量下采取继承。在每一种情况下，我们产生一个有效定义的映射，将任意句子$φ$翻译成属于相应句法片段的句子$φ^{p}$，其属性是$φ$等同于$φ^{p}$，当它具有相关的语义属性时。我们的方法是首先提供这些结果在更简单的设置一元一阶逻辑（$\mathrm{FOE}$）和（$\mathrm{FO}$）的平等，然后移动到$\mathrm{FOE}^{\infty}$包括广义量词$\exists^\infty$到图片。作为我们的推论，我们得到了上述四个语义性质对于$\mathrm{FOE}^{\infty}$ -语句是可判定的。此外，我们的结果是直接相关的自动机和表达模bisimilirity的一元二阶逻辑的变种的特征。该应用程序是在一个配套文件中开发的。
Monadic Second-Order Logic with Path-Measure Quantifier is Undecidable
证明了用定性路测度量词扩充的无限二叉树的一元二阶逻辑（MSO）理论是不可判定的。这个量词表示树中满足某个公式的无限路径的集合具有勒贝格测度1。为此，我们证明了定性泛奇偶树自动机的空性问题是不可判定的。定性的意思是如果一个树自动机的运行中满足接受条件的路径集合具有勒贝格测度1，则该运行是接受的。
The Pseudofinite Monadic Second Order Theory of Linear Order
一元二阶逻辑是一阶逻辑在一元关系上的量词的扩展。本文利用一阶设置研究了有限线性序的共享一元二阶理论，即线性序的伪有限一元二阶理论。我们给出了明确的（和递归的）公理和剩余序列的完成。一个连接profinite代数，特别是与自由profinite幺半群上的一个发电机，建立通过扩展斯通对偶。
Monadic Decomposition in Integer Linear Arithmetic (Technical Report)
一元可分解性是变量独立性的概念，它询问一阶理论中的给定公式是否可以表示为理论中一元谓词的布尔组合。最近，Veanes等人在SMT的上下文中展示了一元可分解性的有用性（即输入公式是无量词的），并发现了各种有趣的应用，包括字符串分析。然而，检查一元可分解性通常是不可判定的。某些理论的可判定性是已知的（例如，Presburger算术，Tarski的实闭域），但关于它们的计算复杂性的结果很少。本文研究了整数线性算术在SMT下的一元可分解性。我们表明，这个决策问题是CONP-完全的，当monadically可分解，一个公式承认在最坏的情况下分解的指数大小。我们提供了一个新的应用程序，我们的结果字符串约束求解长度约束。然后，我们扩展我们的结果变元分解，谓词可以承认多个自由变量（相对于一元分解）。最后，我们给出了整数线性算术中的量词消去的一个应用，其中量词块中的变量，如果是独立的，可以用指数（而不是标准的双指数）爆破消除。
Generalised Quantifiers Based on Rabin-Mostowski Index
本文提出基于拉宾-莫斯科维茨指数的广义量词，研究其在ω-词和无限树中的表达力和可判定性，发现两者在逻辑特性上有显著差异。
Characterizing Weighted MSO for Trees by Branching Transitive Closure Logics
我们引入了分支传递闭包算子的加权一元二阶逻辑公式的分支对应于一个自然的方式在树中固有的分支。对任意交换半环，我们证明了树上的加权一元二阶逻辑等价于由下列算子之一开始的公式的可定义性：（i）分支传递闭包或（ii）存在二阶量词后接泛一阶量词;在这两种情况下，该运算符被应用于（a）通过模计数而丰富的布尔一阶逻辑或（b）布尔一元二阶逻辑上的步进公式。
Alternating Set Quantifiers in Modal Logic
我们建立了严格的几个设置量词交替层次结构的模态逻辑的基础上，评估各类有限图。这延伸到模态设置Matz，Schweikardt和Thomas（2002）的著名结果，该结果指出一元二阶逻辑的类似层次是严格的。因此，本文解决了van Bentham（1983）提出的一个问题，ten Cate（2006）重新提出了这个问题，Kuusisto（2008，2015）对此做了部分回答。
Ramsey Quantifiers over Automatic Structures: Complexity and Applications to Verification
自动结构是由同步有限状态自动机表示的无限结构。本文关注有限词和树（排名/排名）的自动结构。我们调查的“有向版本”的拉姆齐量词，它表示存在一个无限的有向集团。这包含了拉姆齐量词的标准“无向版本”。首先观察到Ramsey量词与验证中的两个问题之间的有趣联系：（1）规则模型检验中Büchi和广义Büchi条件的可达性可以看作是传递自动图上的Ramsey量化（即，其边关系是传递的），（2）检查一元可分解性（a.k.a.可识别性）可以被看作是在共传递自动图上的Ramsey量化（即，其边关系是传递的补集）。我们提供了一个全面的复杂性景观拉姆齐量词在这三种情况下（一般，传递，共传递），所有NL和EXP之间。反过来，这产生了大量具有精确复杂性的新结果，例如，子树/扁平前缀重写的验证，以及树自动关系上的一元分解。我们还获得了相当简单的证明，例如，对于词自动关系上的一元可分解性的NL复杂度（由DFA给出）。
Weak Mso with the Unbounding Quantifier
本文引入了一类新的无限词语言，称之为极大正则语言，它是对$ω$ -正则语言类的扩充.这个类有两个等价的描述：自动机（一种确定性计数器自动机）和逻辑（带有边界量词的弱一元二阶逻辑）。给出了逻辑和自动机之间的有效转换。
The pseudofinite monadic second order theory of words
我们分析了在一个固定的有限字母表的伪有限单子二阶理论的话。特别是，我们提出了一个公理化的理论，工作在一个排序的一阶框架。分析取决于这样一个事实，即串联的话很好地互动与一元二阶逻辑。更确切地说，给出一个签名，在该签名下，对于每个自然数k，关于量词深度至多为k的公式的词（的一元二阶版本）的等价性是拼接的同余。我们使用我们的分析，提出了一个定理的另一种证明，通过扩展的斯通对偶，由于格尔克，格里戈里耶夫，和引脚连接可识别的语言和生成的自由profinite幺半群。
Weak MSO+U with Path Quantifiers over Infinite Trees
本文证明了在无限树上，由无限路上的无界量词U和量化扩展的弱一元二阶逻辑的可满足性是可判定的。证明是通过对某个自动机模型进行空性化约，而自动机模型的空性是使用有限树来确定的。
Ramsey Quantifiers in Linear Arithmetics
本研究提出一种可从LIA、LRA、LIRA三种线性算术SMT理论中消除拉姆齐量词的多项式时间算法，解决了相关良基性检查、一元可分解性等开放问题，并在原型测试中取得良好效果。
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捕获的功能可识别的加权自动机。另一个证明展示了如何将形式主义从一个转换成另一个。
Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking)
REAL工具通过高效消除Ramsey量词，在LIRA中实现快速消除，应用于存活性检查和单子分解等程序验证问题。
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的一个类似的扩展的可判定性。
Flavors of Quantifiers in Hyperlogics
本文扩展超迹逻辑，引入约束与无约束两类迹量词，研究其不同模式对可满足性判定性的影响，证明若干片段等价于S1S或HyperQPTL，并给出新的可判定与不可判定结果。
On the Expressive Power of 2-Stack Visibly Pushdown Automata
可见下推自动机是输入驱动的下推自动机，它可以识别一些非正则上下文无关语言，同时保持了有限自动机的良好闭包和可判定性。具有多个堆栈的可见下推自动机最近被La Torre，Madhusudan和Parlato考虑，他们进一步利用可见性的概念来获得丰富的自动机类，甚至可以表达上下文无关语言之外的属性。同时，它们的自动机在布尔运算下是封闭的，具有可判定的空性和包含性问题，并且在具有额外嵌套结构的词上享有一元二阶逻辑的逻辑表征。这些结果需要一个限制版本的明显下推自动机与多个堆栈，其行为可以分为一个固定数量的阶段。在本文中，我们考虑2-栈可见下推自动机（即，具有两个堆栈的可视下推自动机）以其不受限制的形式。我们表明，他们是表达等价的一元二阶逻辑的存在片段。此外，我们还发现一元二阶量词交替在多重嵌套的词中形成了一个无限的层级结构。结合这些结果，我们得出结论，2-栈可见下推自动机是不封闭的补充。最后，我们讨论了Büchi 2-栈可见下推自动机运行在无限（嵌套）的话的表达能力。通过无限量词扩展逻辑，我们同样可以建立与存在一元二阶逻辑的等价。
Deciding First-Order Satisfiability when Universal and Existential Variables are Separated
本文引入了一个新的一阶逻辑等式可判定片段，它严格地推广了两个已知的一阶逻辑等式可判定片段--Bernays-Schönfinkel-Ramsey（BSR）片段和Monadic片段.定义原则是在原子水平上将普遍量化的变量与存在量化的变量句法分离。因此，我们的分类既不依赖于对量词前缀的限制（如在BSR的情况下），也不依赖于对谓词符号的arity的限制（如在一元的情况下）。我们证明了新的片段表现出有限模型的属性，并推导出一个非小学的计算时间上界所需的决定在新的片段满足。对于量词前缀为$\exists^* \forall^* \exists^*$的前趋句的子片段，可满足性问题被证明是NEXPTIME完备的。最后，我们讨论了如何自动推理程序可以利用我们的结果。
Subshifts, MSO Logic, and Collapsing Hierarchies
我们使用一元二阶逻辑来定义二维子移位，或无限平面的着色集。我们提出了一个自然的家庭的量词交替层次结构，并表明，他们都崩溃到第三级。特别是，这解决了[Jeandel & Theysier 2013]的一个开放问题。这一结果与图画语言形成了鲜明的对比，图画语言的层次结构通常是无限的。
The MSO+U theory of (N, <) is undecidable
我们考虑逻辑MSO+U，这是一元二阶逻辑与无界量词扩展。无界量词用来表示有限集合的一个性质对任意大的集合都成立。证明了该逻辑在无限词上是不可判定的，即（N，<）的MSO+U理论是不可判定的.这解决了有关逻辑的一个悬而未决的问题，并改进了之前的不可判定性结果，该结果使用了无限树和集合论中的附加公理。
Monadic Monadic Second Order Logic
正则语言与一元二阶逻辑对应的主要原因之一是正则语言类在满射字母到字母同态的象下是封闭的。这个闭包性质适用于有限字、有限树、无限字、无限树、自由群的元素等结构。在本文中，我们研究了哪些结构（通过集合范畴中的单子理解）使得正则语言（即由有限代数识别的语言）类在满射字母到字母同态的直接像下是封闭的。我们给出了单子满足这一性质的各种充分条件。我们还提出了许多单子的例子，包括不满足我们的充分条件的正面例子，以及闭包属性失败的反例。
Algebraic Logic, I Quantifier Theories and Completeness Theorems
代数逻辑研究与命题和一阶逻辑相关的代数理论。本文概述了一阶逻辑的一种新的代数方法。我们引入量词理论的概念，这是一个函子从一类单子的集合的布尔代数的范畴，连同一个唯一确定的系统的量词。这种方法的一个显著特点是，凯莱完备性定理和哥德尔完备性定理可以在量词理论中以更简单的方式陈述和证明。这两个定理是由于哈尔莫斯的polyadic代数。我们还提出了一个简单的透明的治疗超产品的模型的量词理论。
Heinrich Behmann's Contributions to Second-Order Quantifier Elimination from the View of Computational Logic
对于关系一元公式（Löwenheim类），二阶量词消去，这是密切相关的计算一致插值，投影和遗忘-操作，目前受到关注的知识处理-总是成功的。Heinrich Behmann从1922年开始对这个类的可判定性证明是通过等价保持公式重写的消元法进行的。在这里，我们重建的结果从Behmann的出版物的详细和讨论相关的问题，在现代方法的背景下，二阶量词消去在计算逻辑。此外，广泛的文件的信件和手稿在贝曼的遗赠，关注二阶量词消去，包括一个评论登记册和英文摘要的德语来源，重点是技术材料。在20世纪20年代后期，Behmann试图为谓词的元数大于1的公式开发一种基于消除的决策方法。他的手稿和与威廉·阿克曼的通信显示了今天仍然感兴趣的技术方面，并深入了解了阿克曼1935年的里程碑式论文“Untersuchungen über das Eliminationsproblem der mathematischen Logik”的起源，该论文奠定了两种流行的现代二阶量词消去方法的基础。
A Cook's tour of duality in logic: from quantifiers, through Vietoris, to measures
我们确定并强调Samson Abramsky工作中的某些里程碑式的成果，我们认为这些成果对当前的发展和未来的趋势至关重要。特别是，我们专注于使用（一）拓扑对偶方法来解决问题的逻辑和计算机科学;（二）范畴理论，更特别的是，自由（和co-free）建设;（三）这些工具，统一的“权力”和“结构”股在计算机科学。
Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness (Extended Preprint)
在Isabelle/HOL中为MSO开发三种嵌入，提出两类替换机制实现自动化忠实性，并机械化证明向下Loewenheim-Skolem定理，区分一般与标准解释，通过经典例子展示差异。
An algebraic approach to MSO-definability on countable linear orderings
我们开发了一个代数概念的可识别性语言的词索引可数线性排序。我们证明了这个概念是有效的等价于一元二阶（MSO）逻辑中的可定义性。我们还提供三个逻辑应用程序。首先，我们建立了可数线性序上MSO逻辑的量词交替的第一个已知的崩溃结果。第二，我们解决了一个公开的问题，由古列维奇和Rabinovich，关于MSO-可定义的集合的有理数使用的实数的背景。第三，我们建立了一个MSO-可定义的树集诱导的产量集的MSO-可定义性，证实了Bruy{è}re，Carton和S{é}nizergues提出的一个猜想。
Skolemization In Intermediate Logics
本文刻画了允许标准及Andrews Skolem化的中间一阶逻辑，并为其他逻辑开发新型Skolem函数，同时证明带量词移位公理的谓词直觉主义逻辑的Kripke框架不完全性，以促进非经典逻辑的消解式定理证明。
Interleaving Logic and Counting
本文研究自然语言推理中逻辑与计数的结合，通过带计数的单子一阶逻辑及其强化形式，分析可定义性、公理化与可判定性，并联系语言量词和认知科学。
Order-Invariant MSO is Stronger than Counting MSO in the Finite
我们比较了一元二阶逻辑（MSO）的两个扩展在有限结构类上的表现力。第一个是计数一元二阶逻辑（CMSO），它用一阶模计数量词扩展了MSO，允许表达像“结构中元素的数量是偶数”这样的查询。第二个扩展允许使用一个额外的二进制谓词，不包含在查询结构的签名中，必须解释为在其宇宙中的任意线性顺序，获得顺序不变的MSO。虽然每一个CMSO公式都可以直接转化为一个等价的阶不变MSO公式，但其逆命题尚未解决。Courcelle证明了对于有限类的结构，序不变的MSO和CMSO都具有同样的表达能力，但他强调，一般来说，序不变的MSO比CMSO更强。我们肯定了这一猜想，提出了一类结构，是顺序不变的定义在MSO，但不能定义在CMSO。
Connection Matrices and the Definability of Graph Parameters
本文推广并详细证明了B. Godlin，T. Kotek和J.A. Makowsky（2008）和J.A. Makowsky（2009）.我们证明了它的巨大的适用性，在简化已知的和新的不可定义的结果的图形属性，并找到新的不可定义的结果的图形参数。我们还证明了一个Feferman-Vaught定理的逻辑CFOL，一阶逻辑与模计数量词。
Refinement Modal Logic
本文提出了{ \em精化模态逻辑}。精化类似于互模拟，不同之处在于从三个关系需求中只需要满足“原子”和“返回”。我们的逻辑包含一个新的操作符“所有”除了标准的模态“框”为每个代理。运算符“all”充当给定模型的所有细化的集合上的量词。作为互模拟量词的一种变体，这个精化运算符或精化量词“all”可以被看作是对一个没有出现在它所约束的公式中的变量进行量化。这种逻辑结合了多智能体模态逻辑的简单性和一元二阶量化的一些能力。我们提出了一个健全的和完整的公理化的多智能体精化模态逻辑。我们还提出了一个扩展的逻辑模态μ演算，和公理化的单代理版本的这个逻辑。例子和应用程序也进行了讨论：软件验证和设计（一套代理也可以被看作是一套行动），并动态认知逻辑。我们进一步给出了详细的结果，可满足性的复杂性，简洁性。
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定理。
Category-theoretical Semantics of the Description Logic ALC (extended version)
范畴论可以用来陈述一阶逻辑中的公式，而不需要使用集合成员。逻辑学中的几个显著结果，如连续统假设的证明，可以在范畴论中优雅地重写。本文提出用范畴语言重新表述描述逻辑$\mathcal{ALC}$通常的集合论语义。在这种设置中，ALC概念被表示为对象，概念包含被表示为箭头，并且成员关系被表示为类别的对象和箭头上的逻辑量词。这种范畴理论语义提供了$\mathcal{ALC}$的语义的更模块化的表示和设计用于推理的算法的新方法。
Succinctness of Order-Invariant Logics on Depth-Bounded Structures
研究了一阶逻辑和一元二阶逻辑的序不变句在有界树深结构上的表达能力和简洁性。一般来说，顺序不变是不可判定的，因此，人们努力寻找具有与顺序不变句子相同的表达能力的可判定语法的逻辑。我们表明，在有界树深度的结构，顺序不变的FO具有相同的表达能力FO。我们的证明技术允许对这种翻译的简洁性进行细粒度的分析。我们证明了，对于每一个顺序不变的FO句子存在一个FO句子，其大小是小学的原始句子的大小，其数量的交替是线性的树深度。我们得到类似的结果MSO。MSO和FO的表达能力在有界树深结构上是一致的。我们提供了一个翻译MSO FO，我们表明，这种翻译基本上是最佳的公式大小。作为进一步的结果，我们表明，顺序不变的MSO具有相同的表达能力，FO与有界树深度结构上的模计数量词。
Algebraic semantics for one-variable lattice-valued logics
任何一阶逻辑的单变量片段都可以被认为是模态逻辑，其中全称量词和存在量词分别被盒模态和菱形模态所取代。在一些情况下，这些逻辑的代数语义的公理化已经得到：最值得注意的是，分别为一阶经典逻辑和直觉主义逻辑的单变量片段的模态对应物S5和MIPC。然而，在一阶中间逻辑的设置之外，缺乏一种通用的方法。本文提供了这样一种方法的基础上设置的一阶格值逻辑，其中公式解释的代数结构与格约简。特别是，公理化得到的模态对应的一个广泛的家庭这些逻辑的一个变量片段通过推广的功能表示定理Bezhanishvili和哈丁一元Heyting代数。一个替代的证明理论的证明也提供了一个变量片段的一阶子结构逻辑，有一个切自由的插值演算，并承认一定的有界插值性质。
Weak MSO: Automata and Expressiveness Modulo Bisimilarity
证明了弱一元二阶逻辑的互模拟不变片段等价于模态$μ$ -演算的片段，其中最小不动点算子$μp.φ$的应用仅限于在$p$中连续的公式$φ$.我们的证明是自动机理论的性质，特别是，我们引入了一类自动机的特点的表达能力的WMSO树模型的任意分支度。这些自动机的转换映射是根据逻辑$\mathrm{FOE}_1^\infty$定义的，该逻辑是具有广义量词$\exists^\infty$的一阶逻辑的扩展，其中$\exists^\infty x. ϕ$意味着有无限多个对象满足$ϕ$。我们的工作的一个重要组成部分是$\mathrm{FOE}_1^\infty$的模型理论分析。
Structure and Power: an emerging landscape
本文综述了范畴论工具在有限模型论、描述复杂性、约束满足和组合学中的应用，通过资源索引伴随族展开关系结构，恢复多种逻辑片段和组合参数，并揭示结构与逻辑计算可处理性之间的新兴景观。
One-dimensional fragment of first-order logic
本文提出了一种新的一阶逻辑的可判定片段。片段是一维的，在这个意义上，量化是有限的存在（通用）量词块的应用程序，使最多一个变量保持自由的量化公式。片段在布尔运算下是封闭的，但额外的限制（称为一致性条件）适用于具有两个或更多变量的原子公式的组合。我们认为，一维性和一致性的概念一起提供了一个新的视角的鲁棒判定的模态逻辑。我们还建立了轻微的修改的限制的语法的一维片段导致不可判定的形式主义。也就是说，二维和非均匀的一维碎片被证明是不可判定的。最后，我们证明了在表达性方面，一维片段与守护否定片段和带计数的二元逻辑是不可比拟的。我们证明的一维片段的可判定性是基于一种技术，涉及直接减少到一元类的一阶逻辑。新技术本身是一个独立的数学兴趣。
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]，并得到一元二阶逻辑的简洁性结果。
Flavours of Sequential Information Flow
信息流策略规定了哪些信息可用于给定的用户或子系统。我们研究的问题，指定这些属性的反应系统，这可能需要动态变化的信息流之间的限制状态。我们形式化的顺序信息流，其中包括不同的假设系统的多个观察之间的语义关系的几种口味。信息流规范属于超属性的范畴。我们定义了不同的变种顺序信息流规范使用一阶逻辑与跟踪量词和时间量词称为超跟踪逻辑。我们证明了HyperLTL，相当于超跟踪逻辑的一个子集，限制量词前缀，不能指定大多数的研究两个状态的独立变量。对于我们的结果，我们引入了一个概念，不能区分某些类的公式在超迹逻辑的轨迹集之间的等价。这提供了一种新的方法来证明诸如HyperLTL之类的逻辑的不可表达性结果。
Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA
模态公式表示Kripke框架上的一元二阶性质，但在许多重要情况下，它们具有一阶等价物。计算这样的等价物对于逻辑和计算原因都是重要的。另一方面，模态公式的规范性也很重要，因为它意味着用规范公式公理化的逻辑的框架完备性。计算一个模态公式的一阶等价等价物相当于消除二阶量词。二阶量词消去有两种算法：基于约束消解的SCAN算法和基于Ackermann建立的逻辑等价的DLS算法。在本文中，我们介绍了一种新的算法，SQEMA，计算一阶等价物（使用阿克曼引理的模态版本），而且，用于证明规范的模态公式。与SCAN和DLS不同，它直接作用于模态公式，从而避免了Skolemization和随后的unskolemization问题。我们提出的核心算法，并说明它与一些例子。然后，我们证明了它的正确性和规范的所有公式上的算法成功。我们表明，它不仅成功的所有Sahlqvist公式，但也对更大的类的归纳公式，在我们以前的论文中介绍。因此，我们开发了一种纯粹的算法方法来证明模态逻辑中的规范完备性，特别是，建立了模态逻辑中迄今为止最普遍的完备性结果之一。
Reasoning in the Description Logic ALC under Category Semantics
本文提出了一种用范畴语言用一般的T盒重新表述描述逻辑$\mathcal{ALC}$的通常的集合论语义。在此设置中，$\mathcal{ALC}$概念表示为对象，概念包含表示为箭头，成员关系表示为类别的对象和箭头上的逻辑量词。这种基于类别的语义提供了$\mathcal{ALC}$的语义的更模块化的表示。这个特性允许我们通过去掉存在性和普遍性限制之间的相互作用来定义$\mathcal{ALC}$的子逻辑，这将导致空间中的指数复杂度。这样一个子逻辑是不可定义的，在通常的集合论语义，我们表明，这个子逻辑是{ \sc{PSPACE} }，提出了一个确定性的算法检查概念可满足性，它运行在多项式空间。
Ultraproducts in abstract categorical logic
本文在抽象范畴逻辑框架下推广经典模型论中的超积方法，并证明了与具体量化词选择尽可能无关的 Łoś 基本定理。
Bundled fragments of first-order modal logic: (un)decidability
量化模态逻辑为模态态度的推理提供了一种自然的逻辑语言，即使在保留量化的丰富性的同时，也可以引用域上的谓词。但是，在许多模型类上，逻辑的大多数片段都是不可判定的。多年来，只有少数片段（例如单声部）被证明是可判定的。在本文中，我们研究的片段，捆绑量词和模态在一起，知识/为什么/什么的认知逻辑的早期工作的启发。与量化模态逻辑一样，域是否在世界上保持相同会产生重大差异。特别是，我们表明，束$\forall \Box$是不可判定的恒定域的解释，即使只有一元谓词，而$\exists \Box$束是可判定的。另一方面，在增加域解释，我们得到的可判定性与$\forall \Box$和$\exists \Box$束与不受限制的谓词。在这些情况下，我们还获得了在\PSPACE中运行的基于tableau的过程。我们进一步表明，$\exists \Box$束不能区分恒定域和增加域的解释。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。