The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable
自然数上的加法的一阶理论，被称为Presburger算术，在双指数时间内是可判定的。在语言中添加一个不可解释的一元谓词会导致一个不可判定的理论。我们锐化已知的边界之间的判定和不可判定的，我们表明，纯粹的普遍的片段扩展理论已经是不可判定的。我们的证明是基于减少停机问题的两个计数器的机器的不满足的句子在扩展语言的Presburger算法，不使用存在量化。另一方面，我们认为，一个单一的$\forall\exists$量词交替把扩展语言的可满足的句子集变成一个$Σ^1_1$-完全集。其中的一些结果可以推广到有序实数上的线性算术领域。这涉及到纯通用片段的不可判定性和至少有一个量词交替的句子的$Σ^1_1$-硬度。最后，我们讨论了我们的结果验证的相关性。特别是，我们得出不可判定性的结果量化的片段的分离逻辑，理论的数组，并结合理论的平等的未解释的功能与限制形式的整数算术。在某些情况下，我们的结果甚至意味着缺乏健全和完整的演绎演算。
2017-03-03 cs.LO
Languages ordered by the subword order
我们把语言与子词关系、覆盖关系和正则谓词放在一起考虑。对于这样的结构，我们考虑扩展的一阶逻辑的阈值和模计数量词。根据语言，使用的谓词，和逻辑的片段，我们确定四个新的组合，产生可判定的理论。这些结果扩展了早期的只考虑语言的所有字没有覆盖关系和片段的一阶逻辑。
2019-01-08 cs.FL cs.LO
Duality for the existential fragment of first-order logic on words with numerical predicates of a fixed arity
这篇文章适合于研究拓扑对偶方法在理论计算机科学中的应用。这种方法的最终目标之一是通过研究表征它们的适当拓扑对象来推导计算复杂性理论的结果。把这两个看似分离的领域联系起来的纽带是逻辑，更确切地说，是有限模型理论的一个子域，称为词的逻辑。它允许将复杂性类描述为有限字母表上的某些语言家族，可能是非正则的。很少有人知道的对偶理论相对于片段的一阶逻辑的话，这是范围以外的正则语言。我们的工作的贡献是这样一个片段的详细研究。固定一个整数$k \geq 1$，我们考虑布尔代数$\mathcal{B}Σ_1[\mathcal{N}^{u}_k]$。它对应于由句子的布尔组合组成的词的逻辑片段，所述句子通过使用至多$k$存在量词、字母谓词和arity $l \in \{1,...,k\}$的统一数值谓词的块来定义。本文对任意$k \geq 1$的布尔代数的对偶空间进行了详细的研究，并给出了它的点的几个刻画。在$k=1$的特殊情况下，我们能够构造一族超滤子方程，它们刻画了布尔代数$\mathcal{B} Σ_1[\mathcal{N}^{u}_1]$。我们使用拓扑方法，以证明这些方程是健全的和完整的关于我们提到的布尔代数。
2022-01-03 cs.LO
Positive and monotone fragments of FO and LTL
本文研究有限字上正逻辑FO+及其片段，证明其与LTL+等逻辑的等价性，并给出一个FO可定义但非FO+可定义的单调语言反例，且该反例不可由FO2定义。
2024-06-25 cs.FL cs.LO
Tractable and Intractable Entailment Problems in Separation Logic with Inductively Defined Predicates
本文研究分离逻辑中带归纳定义谓词的蕴涵问题，针对P规则和loc-deterministic归纳规则片段给出多项式时间的可靠完备循环证明过程，并证明条件放宽后问题不可处理。
2025-07-11 cs.LO
Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates
研究了带未解释一元谓词的差分逻辑的可判定性，证明实数上带单个未解释一元谓词的量化差分逻辑不可判定，而整数差分逻辑结合实数序与未解释一元谓词仍可判定。
2023-05-24 cs.LO
The Bernays-Schönfinkel-Ramsey Fragment with Bounded Difference Constraints over the Reals is Decidable
一阶线性实算术丰富的未解释的谓词符号产生一个有趣的建模语言。然而，这样的公式的可满足性是不可判定的，即使我们限制未解释的谓词符号为arity 1。为了找到这种语言的可判定片段，有必要限制算术部分的表达能力。一种可能的途径是将算术表达式限制为$x - y \mathrel{\#} c$形式的差异约束，其中$\#$的范围在标准关系$<, \leq, =, \neq, \geq, >$和$x,y$上，并且是通用量化的。然而，它是已知的，结合差异约束与未解释的谓词符号产生一个不可判定的可满足性问题。在本文中，证明了可满足性成为可判定的，如果我们另外限制泛量化变量的范围。由于实数上的有界区间仍然包含无穷多个值，平凡的实例化过程不足以解决这个问题。
2017-06-26 cs.LO
An Efficient Cyclic Entailment Procedure in a Fragment of Separation Logic
一个有效的蕴涵证明系统对于使用分离逻辑的组合验证是必不可少的。不幸的是，现有的决策程序要么缺乏表达能力，要么效率低下。例如，Smallfoot是一个有效的过程，但只适用于硬连接的列表和树。其他可以支持一般归纳谓词的过程在时间上呈指数级运行，因为它们的证明搜索需要回溯来处理结果中的析取。本文给出了一个在多项式时间内推导一般归纳谓词循环蕴涵证明的判定过程。我们的程序是高效的，不需要回溯;它使用规范化规则，有助于避免在后果中引入析取。此外，我们的可判定片段是足够的表达：它是基于组合谓词，可以捕获广泛的数据结构，包括排序和嵌套的列表段，跳跃列表与快速前进指针，和二叉搜索树。我们已经实现了一个原型工具的建议，并评估它的挑战性问题，从最近的分离逻辑竞争。实验结果证实了所提出的系统的效率。
2022-10-02 cs.LO
Adding Path-Functional Dependencies to the Guarded Two-Variable Fragment with Counting
研究带计数量词的二变量受保护片段在加入路径函数依赖后的可满足性与有限可满足性问题，证明两者均为ExpTime完全。
2017-10-27 cs.LO
On existential Büchi arithmetic in two coprime bases
University of Oxford（牛津大学）
该研究解决了互素基下Presburger算术扩展Büchi谓词的存在片段的可判定性问题，通过量词消去论证证明其可判定。
2026-08-26 cs.FL 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
Undecidability of first-order modal and intuitionistic logics with two variables and one monadic predicate letter
本文证明了一阶直觉逻辑的正片段在具有两个变量和一个一元谓词字母的语言中是不可判定的，没有常数和等式。无论我们考虑的是扩展域还是常量域的语义，这都是正确的。然后，我们将这一结果推广到区间[QBL，QKC]和[QBL，QFL]，其中QKC是弱排中律的逻辑和QBL和QFL是一阶对应的维塞尔的基本和形式逻辑，分别。我们还表明，对于大多数“自然”的一阶模态逻辑，两个变量片段与一个单一的一元谓词字母，没有常数和平等，是不可判定的，无论我们是否考虑语义与扩展或常数域。这些包括QKTB、QGL和QGrz的所有子逻辑，其中包括QK、QT、QKB、QD、QK4和QS4。
2022-06-12 cs.LO math.LO
A Decision Procedure for Guarded Separation Logic: Complete Entailment Checking for Separation Logic with Inductive Definitions
我们开发了一个双指数决策过程的可满足性问题的保护分离逻辑-一个新的片段的分离逻辑具有用户提供的归纳谓词，布尔连接词，分离连接词，包括限制（保护）版本的否定，魔术棒，和septraction。此外，我们表明，上述任何连接词的警卫下降导致一个不可判定的片段。我们进一步应用我们的决策过程的原因蕴涵在流行的符号堆片段的分离逻辑。特别是，我们获得了一个双指数决策过程之间的蕴涵（无量词）符号堆与有界树宽（SLIDbtw）的归纳谓词定义-分离逻辑的最具表现力的可判定片段之一。再加上最近显示的2 ExpTime-hardness在所述片段中的蕴涵，我们得出结论，SLIDbtw的蕴涵问题是2 ExpTime-complete-从而关闭了以前开放的复杂性差距。
2021-04-20 cs.LO
The Guarded Fragment with Nested Equivalences
Institute of Computer Science, University of Wrocław（弗罗茨瓦夫大学计算机研究所）
本文研究了在守卫片段中引入嵌套等价关系的扩展，证明了无等价的GF具有有限模型性质和可判定的可满足性问题，并建立了紧致复杂度界限。
2026-05-14 cs.LO
Monadic Second-Order Logic with Arbitrary Monadic Predicates
我们研究一元二阶逻辑（MSO）有限字，扩展（非均匀任意）一元谓词。我们表明，它定义了一类语言，具有代数，自动机理论和机器独立的特征。我们考虑正则性问题：给定这门课中的一种语言，它什么时候是正则的？为了回答这个问题，我们展示了一个替换属性和一个句法谓词的存在。我们提出三个应用。前两个是给非常简单的证明，斯特劳宾猜想成立的所有片段的MSO与monadic谓词，并认为起重机海滩猜想成立的MSO与monadic谓词。第三，证明了由带有态谓词的MSO公式定义的语言是否正则是可判定的。
2017-09-10 cs.LO
Around Dot-depth One
点深度层次是无星语言的一种分类。它与有限词上一阶逻辑的量词交替层次有关。我们考虑通过禁止指定前缀或后缀获得的点深度为1/2和点深度为1的语言片段。事实证明，这些语言类与没有最小或最大谓词的存在一阶逻辑片段一一对应。对于所有的片段，我们得到有效的代数特征。此外，我们给出了新的组合证明的可判定性的成员问题的点深度1/2和点深度1。
2011-03-07 cs.FL cs.LO
Positive first-order logic on words
我们研究FO+，一个片段的一阶逻辑有限的话，一元谓词只能出现积极的。我们表明，有一个FO-定义的语言，是单调的一元谓词，但不能定义FO+。这提供了一个简单的证明，林登的保存定理失败的有限结构。我们还表明，给定一个正则语言，它是不可判定的，它是否是在FO+定义。
2021-10-11 cs.FL cs.LO math.LO
Automata Theory Approach to Predicate Intuitionistic Logic
谓词直觉逻辑是依赖类型的一个很好的片段。根据Curry-Howard同构证明，逻辑中的构造与给定公式类型的程序综合有很好的对应。我们提出了一个模型的自动机，可以处理证明建设全直觉一阶逻辑。自动机是以这样一种方式构造的，即任何成功的运行都直接对应于逻辑中的正常证明。这使得讨论证明或程序的形式语言、自动机的闭包性质及其与传统逻辑连接词的联系成为可能。
2016-08-19 cs.LO
Towards a more efficient approach for the satisfiability of two-variable logic
我们重新审视二元逻辑的可满足性问题，记为SAT（FO 2），这是已知的NEXP-完全的。上限通常来自其众所周知的指数尺寸模型（ESM）属性。能否有效地确定它仍然是一个悬而未决的问题。在本文中，我们提出了一种不同的方法，减少它到一个新的图论问题，我们称之为条件独立集（CIS）。我们证明了CIS是NP完全的，并给出了两个简单的算法，其运行时间分别为O（1.4423 ^n）和O（1.6181 ^n），其中n是图中的顶点数。我们还表明，除非“强指数时间假设”（SETH）失败，有没有算法的CIS具有运行时间O（1.4141 ^n）。我们表明，没有相等谓词SAT（FO 2）实际上是等同于CIS的简洁表示。这产生了两个不带相等谓词的SAT（FO 2）算法，运行时间为O（1.4423^{2^n}）和O（1.6181^{2^n}），其中n是谓词的数量。据我们所知，这些是NEXP完全可判定逻辑的第一个精确算法，其运行时间显著低于O（2^{2^n}）。我们还确定了一些较低的复杂性片段的FO 2对应于易于处理的片段的CIS。与CIS类似，除非SETH失败，否则SAT（FO 2）没有运行时间为O（1.4141^{2^n}）的算法。对于带有相等谓词的片段，我们提出了一个线性时间多-一约简。减少产生等可满足的公式与一个小的常数爆破的谓词的数量。最后，我们还进行了一些小实验，表明我们的方法确实比现有方法（基于ES…
2021-11-29 cs.CC cs.LO
Eigenvariables, bracketing and the decidability of positive minimal predicate logic
本文通过括号化机制替代特征变量条件，给出正最小谓词逻辑可判定性的新证明，并推广至简单类型论、二阶命题逻辑及系统F正类型居留问题。
2023-05-15 cs.LO
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的一元二阶逻辑的变种的特征。该应用程序是在一个配套文件中开发的。
2018-09-10 cs.LO math.LO
Enhancing Predicate Pairing with Abstraction for Relational Verification
关系验证是一种旨在证明两个不同程序片段或两个不同程序运行相关属性的技术。它已被证明，受约束的霍恩子句（CHC）可以有效地用于关系验证，通过应用CHC转换，称为谓词配对，它允许CHC求解器推断不同谓词的参数之间的关系。在本文中，我们研究了如何通过使用基于线性算术的各种抽象域（即，凸多面体的域和它的一些子域）。在提出了一个算法与抽象谓词配对，我们报告的实验，我们已经进行了一百多个关系验证问题，通过使用各种抽象域。实验已经进行了使用VeriMAP转换和验证系统，连同帕尔马多面体库（PPL）和Z3求解器的CHCs。
2017-09-14 cs.LO cs.SE
The Triguarded Fragment
University of Wrocław（弗罗茨瓦夫大学）；TU Dresden（德累斯顿工业大学）；ScaDS.AI Dresden/Leipzig（德累斯顿/莱比锡数据科学与工程中心）；TU Wien（维也纳工业大学）
该研究结合一阶谓词逻辑的守卫片段与两变量片段，提出三元守卫片段TGF，证明其可满足性问题在特定条件下的复杂度，且具有有限模型性质，为相关逻辑研究提供新的可判定片段。
2026-08-04 cs.LO
"Most of" leads to undecidability: Failure of adding frequencies to LTL
有限迹上的线性时态逻辑是形式化验证中常用的一种健壮的规范框架。然而，尽管近年来对逻辑的兴趣很高，但其定量扩展的主题尚未得到充分探讨。这项工作的主要目标是研究添加弱形式的百分比约束（例如，大多数的位置在过去满足给定的条件，或sigma是最频繁的字母发生在过去）的LTL片段的效果。这种扩展可能用于验证影响网络或统计推理。不幸的是，正如我们在论文中证明的那样，事实证明，即使是很小的LTL片段的百分比扩展也具有不可判定的可满足性和模型检查问题。我们的不可判定性证明，不仅锐化了大多数的不可判定性结果的逻辑与算术解释的话从文献中已知的，但也是相当简单的。我们还证明了通过限制否定的允许使用可以避免不可判定性，并简要讨论了不可判定性结果如何转移到一阶词逻辑。
2021-01-03 cs.FL cs.LO
The Finite Satisfiability Problem for Two-Variable, First-Order Logic with one Transitive Relation is Decidable
本文研究带一个传递关系的双变量一阶逻辑，证明其有限可满足性问题可判定，复杂度为三重指数非确定性时间，若约束为偏序则降至双重指数。
2017-07-18 cs.LO
A van Benthem Theorem for Fuzzy Modal Logic
我们提出了一个模糊（或定量）版本的范本特姆定理，其特点是命题模态逻辑作为一阶逻辑的互模拟不变片段。具体来说，我们考虑一阶模糊谓词逻辑及其模态片段，并表明，模糊一阶公式是非扩张的w.r.t.互模拟距离的自然概念正好是那些可以通过模糊模态公式来近似的概念。
2018-02-05 cs.LO
First-order Fragments with Successor over Infinite Words
我们考虑片段的一阶逻辑和模型，我们允许有限和无限的话同时。除了相等之外，唯一的二元关系是顺序比较<和后继谓词+1。我们给出了片段Sigma 2 = Sigma 2 [<，+1]和FO 2 = FO 2 [<，+1]的代数和拓扑性质的刻画.为此，我们引入无限词的因子拓扑。事实证明，语言L是FO 2和Sigma 2的交集，当且仅当L是FO 2语言的内部。对称地，一种语言是FO 2和Pi 2的交集，当且仅当它是FO 2语言的拓扑闭包。片段Delta 2，根据定义是Sigma 2和Pi 2的交集，包含FO 2中的Clopen语言。特别地，在无限单词上Delta 2是FO 2的严格子类。我们的刻画产生的可判定性的成员资格问题，所有这些片段在有限和无限的话，作为一个必然的结果，我们也获得了无限的话的可判定性。此外，我们给出了有限字上点深3/2的一个新的可判定代数刻画。点深度3/2在有限词上的可判定性首先由Glaßer和Schmitz在STACS 2000中给出，而FO 2在无限词上的成员问题的可判定性则由Wilke在1998年的论文中给出，而Sigma 2在无限词上的可判定性以前是未知的。
2010-12-30 cs.FL cs.LO
Adding Circumscription to Decidable Fragments of First-Order Logic: A Complexity Rollercoaster
Leipzig University（莱比锡大学）；Center for Scalable Data Analytics and Artificial Intelligence (ScaDS.AI)（可扩展数据分析与人工智能中心（ScaDS.AI））
本文研究一阶逻辑可判定片段（FO$^2$、C$^2$、GF）添加限制算子后的逻辑后承可判定性与复杂度，并探究了受限知识库查询的复杂度边界。
2024-07-30 cs.AI cs.LO
Formalization of Fragments of the Theory of Hereditarily Finite Sets
Institute of Computer Science of the Czech Academy of Sciences（捷克科学院计算机科学研究所）；Faculty of Mathematics and Physics, Charles University, Prague（布拉格查理大学数学与物理学院）
该研究在Isabelle/HOL中形式化遗传有穷集理论片段，采用locale层级结构对应不同公理片段，用一阶可定义谓词的归纳定义处理公理模式，分析等价的有穷性与正则性公理，并通过模型形式化公理独立性结论。
2026-09-28 cs.LO
A Decidable Bundled Fragment of First-Order Modal Logic Without Finite Model Property
本文证明了一阶模态逻辑捆绑片段中不满足有限模型性质的组合在递增域模型下是可判定的，将原有三分法坍缩为二分法。
2025-06-02 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
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
Existential Definability over the Subword Ordering
本文研究子字序上一阶逻辑的存在片段表达能力，证明当字母表大小至少为3时，带常量存在片段可定义的关系恰为递归可枚举关系，并据此完整刻画了所有量词交替片段的表达能力。
2023-12-20 cs.FL cs.LO
Strong-Separation Logic
大多数分离逻辑的自动验证器都以符号堆碎片为目标，不允许魔术棒运算符和经典布尔运算符应用于空间公式。这并不奇怪，因为对魔杖的支持很快导致了不可判定性，特别是当与归纳谓词结合用于数据结构的推理时。为了规避这些不可判定性的结果，我们建议分配一个更严格的语义分离合取。我们认为，由此产生的逻辑，强分离逻辑，可用于组合程序验证和双溯静态分析就像“标准”的分离逻辑，同时保持可判定的，即使在魔术棒和列表段谓词的存在下-功能的组合，导致undecidability假设标准的语义。
2021-03-11 cs.LO
First-Order Logic with Connectivity Operators
一阶逻辑（FO）可以在图上表达许多算法问题，例如独立集和支配集问题，并通过解大小进行参数化。另一方面，FO不能表达两个顶点是否连通的非常简单的算法问题。我们丰富FO与连接谓词，是专门用来表达算法图的属性，通常在参数化算法研究。通过添加原子谓词$conn_k (x, y, z_1 ,\ldots, z_k)$，如果在$z_1,\ldots,z_k$的（赋值）被删除后，$x$（的赋值）和$y$之间存在路径，则在图中保持为真，我们获得分隔符逻辑$FO + conn$。我们表明，分离器逻辑可以表示许多有趣的问题，如反馈顶点集问题和消除距离问题的一阶可定义类。然后，我们研究了分离器逻辑的局限性，并证明它不能表示平面性，特别是，不相交的路径问题。我们通过添加原子谓词$disjoint-paths_k [(x_1, y_1 ),\ldots , (x_k , y_k )]$来获得更强的不相交路径逻辑$FO + DP$，如果对于所有$1 \le i \le k$，$x_i$和$y_i$（的赋值）之间存在内部顶点不相交路径，则这些原子谓词的求值为真。不相交路径逻辑可以表示不相交路径问题、（拓扑）子包含问题、命中（拓扑）子问题等等。最后，我们比较了新逻辑与传递闭包逻辑和一元二阶逻辑的表达能力。
2021-11-09 cs.LO
Completeness for a First-order Abstract Separation Logic
分离逻辑（SL）断言语言的定理证明的现有工作要么集中在抽象语义上，这在大多数程序验证应用中是不容易获得的，要么集中在具体模型上，这是不可能的。具体SL中的一个重要元素是指向谓词，它表示单例堆。带有指向谓词的SL已被证明是不可递归的。在本文中，我们开发了一个一阶SL，称为FOASL，与抽象版本的指向谓词。我们证明了FOASL是健全的和完整的抽象语义，其中标准SL语义是一个实例。我们还表明，一些推理原则，涉及点到谓词可以近似为FOASL理论，从而使我们的逻辑用于推理具体的程序验证问题。我们给出了一些例子理论，是健全的分离逻辑从文献中的不同变体，包括那些与雷诺兹的语义不兼容。在实验中，我们展示了我们的FOASL为基础的定理证明，这是能够处理大量的分离逻辑与堆语义，以及非标准的语义片段。
2016-08-24 cs.LO
Temporal Stream Logic modulo Theories (Full Version)
时态流逻辑（TSL）在任意函数项上通过更新和谓词扩展LTL。这允许指定LTL表达能力不足的数据密集型系统。在TSL的语义中，函数和谓词是不解释的。在本文中，我们扩展TSL与一阶理论，使我们能够指定系统使用解释功能和谓词，如增量或相等。我们调查的可满足性问题TSL模的标准基础理论的未解释的功能，以及相对于Presburger算法和理论的平等：对于所有这三个理论，TSL可满足性是高度不可判定的。然而，我们确定了三个片段的TSL的可满足性问题是（半）不可判定的理论解释的功能。尽管高的不可判定性，我们提出了一种算法-这是不保证终止-用于检查可满足性的TSL公式在理论的未解释的功能和评估：它的规模以及能够验证假设在现实世界中的系统设计。
2022-01-25 cs.LO
Finite Satisfiability of the Two-Variable Guarded Fragment with Transitive Guards and Related Variants
本文研究 GF2 在传递、等价、预序或偏序守卫下的有限可满足性，通过柱面多维网格构造与整数规划给出最小模型规模及最优复杂性界。
2018-01-02 cs.LO
Bounded Model Checking of Pointer Programs Revisited
指针程序的有界模型检验是一种调试技术，用于操作堆上动态分配的指针结构的程序。它基于以下四点意见。第一，错误条件（如悬空指针的解引用）可以用双变量一阶逻辑的~片段来表示。其次，片段在最弱的前提条件wrt下是封闭的。有限路径第三，数据结构，如树、列表等，可以通过在数据库片段中定义的归纳谓词来表达。最后，双变量逻辑和数据库的两个片段的组合是可判定的。在本文中，我们通过扩展底层逻辑的表达能力来改进这种技术。在~序列的例子中，我们证明了新的逻辑是能够建模更复杂的数据结构与更复杂的依赖堆和更复杂的分析。
2016-02-29 cs.LO cs.PL
On Logics and Homomorphism Closure
谓词逻辑是指定关系结构类的首选。同态是描述关系结构之间的对应关系的关键。关于这两种表征（类）结构的方法之间的相互依赖性的问题具有根本的意义，并且可以是非常不容易回答的。本文研究了关于逻辑句子的所有（有限或任意）模型类的同态闭包（homclosure）的几个问题：句子的homclosure中结构的成员关系;句子的homclosedness;逻辑中的homclosure的可刻画性;某些逻辑中homclosed句子的范式。对于一阶和二阶谓词逻辑的各种各样的片段，我们澄清这些问题的计算性质。
2021-06-29 cs.CC cs.LO math.LO
Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic
Nagasaki University（长崎大学）；Toho University（东邦大学）
本文通过将皮亚诺算术中的Pi-0-1公式翻译为仅包含直觉主义指向谓词、0和后继函数的分离逻辑小片段，证明了标准模型下算术公式的有效性等价于该片段中翻译公式的有效性，并由此得出该片段不可判定的新证明。
2026-05-22 cs.LO
Predicate Logic as a Modelling Language: The IDP System
随着当时的技术，Kowalski在1974年的开创性论文{ \em Predicate Logic as a程序设计语言}是逻辑在计算机科学中应用的突破。它引入了两个基本思想：在声明方面，使用经典逻辑的Horn子句逻辑片段，很快就扩展了否定失败，在程序方面，程序解释使得有可能在形式主义中编写算法。从那时起，在逻辑编程形式主义的声明性理解和自动推理技术方面都取得了很大的进展，特别是在SAT求解，约束编程和答案集编程方面。这为逻辑编程的扩展的发展铺平了道路，该扩展体现了逻辑作为建模语言及其在解决问题中的作用的更纯粹的观点。本文介绍了\idp语言和系统。该语言本质上是经典逻辑的扩展，逻辑编程对知识表示的最重要贡献之一：将复杂定义表示为基于良好语义的规则集。该系统是一个知识库系统：一个系统，其中复杂的声明性信息存储在知识库中，可以用来解决不同的计算问题，通过应用多种形式的推理。在这种观点中，理论是陈述性的模型，信息袋，对可能的事态的描述。它们既不是计算问题的过程，也不是计算问题的描述。因此，\idp语言和系统保留了逻辑程序的声明性读取的基本思想，而它们与逻辑程序的过程性解释的基本思想决裂。
2018-03-13 cs.LO
Languages of Dot-depth One over Infinite Words
在有限字上，点深度为1的语言对于无交替的一阶逻辑是表达完备的。这个片段也被称为存在一阶逻辑的布尔闭包。这里，原子公式包括顺序、后继、最小和最大谓词。Knast（1983）证明了一种语言是否具有点深度是可判定的。我们将Knast的结果推广到无限词。特别是，我们描述了类的语言定义的交替自由的一阶逻辑在无限的话，我们给出了一个有效的表征这个片段。这一特征有两个组成部分。第一个组成部分是相同的Knast的代数属性有限的话，第二个组成部分是一个拓扑属性，即是一个布尔组合康托集。作为一个中间步骤，我们同时考虑有限和无限的话。然后，我们得到的结果，无限的话，以及有限的话作为特殊情况。特别地，我们给出了有限字上点深为1的语言的Knast定理的一个新证明。
2011-04-01 cs.FL cs.LO
Polynomial Rewritings from Expressive Description Logics with Closed Predicates to Variants of Datalog
TU Wien（维也纳技术大学）
在许多情况下，完整和不完整的信息并存。出于这个原因，知识表示和数据库社区长期以来一直对在推理逻辑理论时同时支持封闭世界和开放世界的观点感兴趣。在这里，我们考虑使用逻辑理论查询可能不完整的数据的设置，形式化的本体介导的查询（OMQ），对查询与理论，有时称为本体，表达背景知识的评价。这可以通过从理论中指定一组封闭谓词来进一步丰富，这些谓词将在封闭世界假设下解释，而其余的则用开放世界观点来解释。通过这种方式，我们可以利用数据的部分完整性来检索更精确的查询答案。本文的中心目标是理解OMQ语言的相对表达能力，其中本体是用表达性描述逻辑（DL）ALCHOI编写的，并且包括一组封闭谓词。我们考虑一类有限的合取查询。我们的主要结果是表明，这种非单调查询语言中的每一个查询都可以在多项式时间内被翻译成稳定模型语义下的带否定的数据库。为了克服挑战，数据库没有直接的手段来表达存在的量化ALCHOI，我们定义了一个两个玩家的游戏，其特征在于本体的满意度，并设计了一个数据库查询，可以决定存在的获胜策略的游戏。如果没有封闭的谓词，也就是在查询一个普通的ALCHOI知识库的情况下，我们的翻译产生一个多项式大小的正析取数据库程序。据我们所知，不像以前的翻译相关片段表达（非霍恩）DL，这些是第一个多项式时间翻译。
2019-12-16 cs.AI cs.LO
Positive First-order Logic on Words and Graphs
本文研究有限词上一阶逻辑片段 FO+，证明存在单调但无法用 FO+ 定义的 FO 可定义语言，借此说明 Lyndon 保持定理在有限结构上失效，并将该结论推广至有限图，同时证明判断正则语言是否 FO+ 可定义的问题不可判定。
2023-07-24 cs.FL cs.LO math.LO
On the Complexity of the Numerically Definite Syllogistic and Related Fragments
本文研究了添加数值量词等构造的三段论逻辑的可满足性复杂性，并证明了相关证明系统的不完备性。
2007-01-06 cs.AI cs.CC cs.LO
Model Checking for Low Monodimensionality Fragments of CMSO on Topological-Minor-Free Graph Classes
LIRMM, Univ Montpellier, CNRS（法国国家科学研究中心蒙彼利埃计算机科学与随机力学实验室）；University of Bremen（不来梅大学）；Université Paris Cité, CNRS, IRIF（巴黎西岱大学法国国家科学研究中心信息研究所）；LIMOS, Univ Clermont Auvergne（克莱蒙奥弗涅大学 LIMOS 实验室）
本文提出了一种基于低单维性的CMSO碎片，证明其在拓扑极小图类上具有固定参数可解性，扩展了逻辑元定理到拓扑极小图类。
2026-04-30 cs.LO math.CO
Towards Weak Stratification for Logics of Definitions
本文探讨了定义逻辑中弱分层条件的兼容性，证明其与通用量化和归纳兼容，并旨在扩展Abella证明助手以支持此类定义。
2026-02-03 cs.LO
Extending Two-Variable Logic on Trees
最近证明了在树上解释的一阶逻辑的两个变量片段的有限可满足性问题是ExpSpace完备的。我们考虑这个逻辑的两个扩展。我们发现，添加额外的二进制符号或计数量词的逻辑不影响有限可满足性问题的复杂性。然而，结合两个扩展并添加二进制符号和计数量词会导致这种复杂性的爆炸。我们还比较了两个变量的片段的表达能力，其扩展与计数量词的树木。事实证明，这两种逻辑具有同样的表达能力，尽管在无序树的限制情况下，计数量词确实增加了表达能力。
2016-11-24 cs.LO
Towards a Model Theory of Ordered Logics: Expressivity and Interpolation (Extended version)
我们考虑家庭的保护和无保护有序逻辑，构成一个最近重新发现的家庭的可判定的片段的一阶逻辑（FO），其中的顺序量化的变量一致的顺序，这些变量出现作为参数的谓词。虽然他们的可满足性问题的复杂性现在已经很好地建立起来，但是他们的模型理论却知之甚少。本文的目的是提供一些见解。我们首先提供了合适的概念，有序逻辑的互模拟。接下来，我们采用互模拟来比较有序逻辑的相对表达能力，并将我们的逻辑描述为FO a la van Bentham的互模拟不变片段。然后研究了Craig插值性质~（CIP）。我们驳斥了另一个说法，从臭名昭著的工作珀迪，通过显示，长笛和向前的碎片不享受CIP。我们补充这一结果表明，有序片段和保护有序逻辑享有CIP。这些积极的结果依赖于新的和相当复杂的模型结构，充分利用了我们的逻辑的“forwardness”。
2022-06-23 cs.LO
The Complexity of Circumscription in DLs
University of Naples Federico II（那不勒斯费德里科二世大学）；University of Bremen（不来梅大学）；University of Liverpool（利物浦大学）
作为一阶逻辑的一部分，描述逻辑不具有可废止继承和缺省规则等非单调特性。由于许多应用程序将受益于这些功能的可用性，已经开发了几个家庭的非单调DL，主要是基于默认逻辑和自认知逻辑。在本文中，我们认为限制作为一个有趣的替代方法，非单调的DL，特别是，支持可废止的继承在一个自然的方式。我们研究了在不同的语言限制和不同的约束条件下扩展的DLs的最小化，固定和变化的谓词集，并查明确切的计算复杂性的推理DLs范围从ALC ALCIO和ALCQO。当最小化谓词和固定谓词只包括概念名称但不包括角色名称时，则NExpTime^NP的推理完成。对于NP^NExpTime，当最小化谓词和固定谓词的数量由一个常数限制时，它就成为完备的。如果角色可以被最小化或固定，那么复杂性范围从NExpTime^NP到不可判定性。
2014-01-15 cs.AI cs.LO
Adding the Relation Meets to the Temporal Logic of Prefixes and Infixes makes it EXPSPACE-Complete
在表达性和复杂性之间选择正确的折衷是区间时态逻辑的主要问题。在他们的开创性论文中，Halpern和Shoham表明HS（艾伦关系的时序逻辑）的可满足性问题在任何合理的线性序类上都是高度不可判定的。为了恢复可判定性，可以限制时间模态的集合和/或模型的类别。在下文中，我们专注于HS片段在同质性假设下的可满足性问题，根据该假设，任何命题字母在区间上成立，如果它在所有点上成立。具有齐次性的完全HS问题已经被证明是非初等可判定的，但它唯一已知的下界是EXPSPACE（事实上，对于前缀和后缀BE的逻辑已经证明了EXPSPACE-困难，这是它的一个非常小的片段。本文证明了将Allen关系Meets加到BD上使BD成为EXPSPACE完备的。
2021-09-17 cs.LO
Deciding Boolean Separation Logic via Small Models (Technical Report)
本文提出一种基于小模型边界优化和SMT翻译的分离逻辑判定过程，支持复杂布尔结构与常见链表变体，在符号堆片段上具有竞争力并能处理此前无判定过程的公式。
2024-03-27 cs.LO
On Role Logic
我们提出的角色逻辑，一个符号的关系结构的形状分析，数据库和知识库中描述的属性。我们使用de Bruijn的λ演算符号的思想来构造角色逻辑，在λ演算中编码一阶逻辑，以及一元和二元谓词的隐式参数的简单规则。角色逻辑的无限制版本具有传递闭包的一阶逻辑的表达能力。通过对角色逻辑公式的句法限制，我们识别出角色逻辑的一个自然片段RL ^2。我们证明了RL^2片段与计数C^2的二元逻辑具有相同的表达能力，因此是可判定的。我们提出了一个翻译的命令式语言到可判定的片段RL ^[2]，它允许组合验证的程序，操纵关系结构。此外，我们展示了RL^2如何编码布尔形状分析约束和一个富有表现力的描述逻辑。
2004-08-05 cs.LO cs.PL
