Model Checking Positive Equality-free FO: Boolean Structures and Digraphs of Size Three
本文研究了正无等式一阶逻辑上固定结构A的模型检验问题--非一致量化约束满足问题QCSP（A）的自然推广.我们证明了这个问题的一个完整的复杂性分类时，A的范围超过1。布尔结构和2.）有向图的大小（小于或等于）3。前者表现为对数空间与P空间完全的二分法，后者表现为对数空间、NP完全、co-NP完全和P空间完全的四分性。
2008-08-05 cs.CC cs.LO
Doctrinal Semantics of Directed First-Order Logic
Tallinn University of Technology（塔林科技大学）
本文提出一种带有非对称有向等价关系的一阶逻辑，通过类型作为预序的解释，利用极性系统描述有向等价作为相对左伴随，证明了该逻辑的范畴语义及其变体的正确性。
2026-05-11 cs.LO math.CT
Algebraic Semantics of Datalog with Equality
讨论了关系Horn逻辑（RHL）和部分Horn逻辑（PHL）的语法和语义. RHL是Datasheet程序设计语言的扩展，它允许在结论中引入和等同变量。PHL是RHL通过部分函数的句法扩展，并且是本质代数理论的许多等价概念之一。我们的主要贡献是构建了一个新的自由模型。我们关联到RHL和PHL序列分类态射，这使我们能够使用提升特性来表征逻辑满意度。然后，我们得到自由和弱自由模型使用小对象参数。小对象参数可以被理解为Datasheet评估的抽象概括。它支持Eqlog Datlog引擎的实现，该引擎计算PHL理论的自由模型。
2023-02-22 cs.LO
Matching Logic
本文提出了匹配逻辑，一个一阶逻辑（FOL）的变种，通过模式和模式匹配来指定和推理结构。它的句子，模式，是由变量，符号，连接词和量词构成的，但功能和谓词符号之间没有区别。在模型中，模式计算到幂集域（与之匹配的一组值），而FOL中的函数和谓词映射到常规域。匹配逻辑统一地概括了几个对程序分析很重要的逻辑框架，例如：命题逻辑、代数规范、具有等式的FOL、模态逻辑和分离逻辑。模式可以在任何程序配置中的任何级别指定分离要求，而不仅仅是在堆或存储中，而不需要任何特殊的逻辑结构：模式匹配的本质是，如果两个结构作为模式的一部分进行匹配，那么它们只能在空间上分离。与FOL一样，匹配逻辑也可以被转化为具有相等性的纯谓词逻辑，同时承认它自己的健全和完整的证明系统。匹配逻辑的一个实际方面是，具有等式的FOL推理仍然是合理的，因此现成的证明器和SMT求解器可以用于匹配逻辑推理。匹配逻辑特别适合于对具有操作语义的程序设计语言中的程序进行推理，但不限于此。
2017-12-17 cs.LO
Model-checking positive equality free logic on a fixed structure (direttissima)
本文为以模型为参数的正无等词逻辑模型检测问题的四类复杂度分类提供了仅基于关系的新直接证明，并开发了新算法解决无限结构中NP和co-NP成员资格问题。
2024-08-25 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
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
The decision problem of modal product logics with a diagonal, and faulty counter machines
在二变量一阶逻辑的命题模态（和代数）处理中，等式由“对角”常数建模，在通用框架的平方积中解释为恒等（也称为“对角”）关系。在这里，我们研究的决定问题的产品的两个任意模态逻辑配备这样的对角线。由于二元一阶逻辑中等式的存在或不存在并不影响其可满足性问题的复杂性，因此人们可能会认为，在一般的乘积逻辑中添加对角线也是无害的。我们证明，情况远非如此，复杂性可能会有相当大的跳跃，甚至从可判定到高度不可判定。我们的不可判定逻辑也可以被看作是一阶逻辑的新片段，其中添加等式将可判定片段改变为不可判定。我们证明了我们的结果的一个新的应用计数器机的问题。虽然我们的形式主义显然不能直接强制可靠的计数器机器计算，但模型中唯一对角线的存在使得有可能对相同指令序列的有损和插入错误计算进行编码。我们表明，给定这样一对错误的计算，就有可能根据它们重建可靠的运行。
2015-09-07 cs.LO
Combining Deduction Modulo and Logics of Fixed-Point Definitions
归纳和共归纳规范在计算系统的形式化中有着广泛的应用。这样的规范在支持定点定义的逻辑中有一个自然的再现。另一个有用的形式化手段是递归规范。这些规范不直接由定点推理技术补充，相应地，不必满足强单调性限制。我们将展示如何将重写功能到逻辑的定点定义对另外支持递归规范。特别是，我们描述了一个自然的演绎演算，增加了一种形式的“封闭世界”的平等-一个关键的成分，以支持定点定义-演绎模，一个框架，用于扩展一个逻辑与重写层操作公式。我们表明，我们的演算具有很强的规范化时，重写系统满足一般属性，我们证明了它的有用性，在指定和推理基于语法的描述。将封闭世界等式整合到演绎模中，使我们重新配置了这种形式的等式的消除原理，第一次解决了关于归约下有限证明的稳定性问题。
2012-04-27 cs.LO
Complexity and Expressivity of Uniform One-Dimensional Fragment with Equality
均匀一维片段UF 1 ^=是从一阶逻辑中获得的一种形式，通过将量化限制在存在（全称）量词块的应用中，使得在量化公式中最多有一个变量保持自由。片段在布尔运算下是闭合的，但附加的限制（称为一致性条件）适用于具有两个或多个变量的原子公式的组合。这个片段可以被看作是二元逻辑的规范化推广，定义它是为了能够处理任意的关系。最近引入了分片的概念，并证明了UF 1 ^=的无等式分片的可满足性问题是可判定的.本文证明了UF 1 ^=的可满足性和有限可满足性问题是NEXPTIME-完全的。我们还证明了具有计数量词的扩展UF ^=的相应问题是不可判定的。除了可判定性问题，我们还比较了UF ^=和二元逻辑与计数量词FOC^2的表达性。我们表明，虽然逻辑一般来说是不可比较的，但当注意力仅限于元数界为二的词汇时，UF 1 ^=严格包含在FOC^2中。
2014-09-02 cs.LO math.LO
Discussion Graph Semantics of First-Order Logic with Equality for Reasoning about Discussion and Argumentation
Department of Informatics, Kyoto University, Japan（信息学系，京都大学，日本）
本文针对现有AI论证推理缺乏通用形式框架的问题，提出带等词一阶逻辑的讨论图语义，推广Dung外延概念并证明其相关可刻画性结论。
2025-11-13 cs.AI cs.LO
The complexity of the first-order theory of pure equality
该研究通过编码图灵机计算为布尔公式，证明纯相等一阶理论的计算复杂度下界，从而得出P是PSPACE的真子类。
2021-07-04 cs.CC cs.LO math.LO
Blocked Clauses in First-Order Logic
阻塞子句为SAT、QBF和DQBF求解中使用的强大推理技术提供了基础。它们的定义依赖于一个简单的语法标准，保证了它们是冗余的并且容易找到。本文将阻塞子句的概念提升到一阶逻辑中。我们引入了两种类型的阻塞子句，一种用于一阶逻辑的等式和另一种用于一阶逻辑的不等式，并证明了它们的冗余性。此外，我们给出了一个多项式算法来检查一个子句是否被阻塞。基于我们新的阻塞概念，我们实现了一个新的一阶预处理工具。实验表明，TPTP库中的许多一阶问题都包含大量的阻塞子句。此外，我们观察到，它们的消除可以提高现代定理证明器的性能，特别是在可满足的问题实例上。
2017-02-02 cs.LO
The Complexity of Temporal Logic over the Reals
本文证明了实数时间上具有until和since连接词的时态逻辑的判定问题是PSPACE完全的。
1999-10-13 cs.CC cs.LO
Fixed-Points for Quantitative Equational Logics
我们发展了定量方程逻辑的一个不动点扩展，并给出了有界完备定量代数的语义。与以前关于度量空间中不动点的相关工作不同，我们使用近似相等而不是精确相等的概念。其结果是一个新的理论的不动点，它不仅可以提供解决传统的不动点方程，但我们也可以定义收敛到不动点的速度。我们表明，这样一个理论是定量模拟的康威理论，也是迭代理论，它反映了度量coinduction原则。我们研究了Bellman方程的马尔可夫决策过程作为一个说明性的例子。
2021-06-30 cs.LO
Functional Answer Set Programming
University of Corunna（科鲁尼亚大学）
在本文中，我们提出了一个扩展的答案集编程（ASP），特别是其最一般的逻辑对应，量化平衡逻辑（QEL），以处理部分功能。虽然平等的治疗QEL可以建立在不同的方式，我们首先分析了选择可判定的平等与完整的功能和Herbrand模型，最近提出的文献。我们认为，这种选择产生一些违反直觉的效果，从逻辑编程和知识表示的观点。然后，我们提出了一个变种称为QELF的功能集被划分为部分和Herbrand功能（我们也称之为构造函数）。在本文的其余部分，我们展示了一个直接连接到斯科特的存在逻辑，并提出了一个实际的应用，提出了一个扩展的正常逻辑程序处理部分功能和平等，使他们可以被翻译成功能免费正常的程序，有可能以这种方式计算其答案集与任何标准的ASP求解器。
2010-06-18 cs.AI cs.LO
The complete classification for quantified equality constraints
Jagiellonian University（雅盖隆大学）
该研究证明了QCSP(ℕ;x=y→y=z)是PSpace完全问题，解决了一个存在十余年未解的问题，完成了关于等价语言上QCSP的复杂性分类，同时还解决了有限交替QCSP(Γ)的分类问题。
2026-05-21 cs.CC cs.LO math.LO
Complexity of validity for propositional dependence logics
研究了命题依赖逻辑、模态依赖逻辑和扩展模态依赖逻辑的有效性问题。我们证明了命题依赖逻辑的有效性问题是NEXPTIME-完全的。此外，我们建立了相应的问题的模态依赖逻辑和扩展的模态依赖逻辑是NEXPTIME困难的，在NEXPTIME^NP。
2014-08-26 cs.CC cs.LO
The Epsilon Calculus with Equality and Herbrand Complexity
希尔伯特微积分是初等或谓词演算的扩展，通过形成项的算子$\varepsilon$和包含这些项的初始公式。关于微积分的基本结果是所谓的微积分定理，这些定理已经用微积分消元法证明。它是通过去掉初始公式，将微积分中的证明转化为初等或谓词演算中的证明的过程。一个显着的后果是证明Herbrand的定理由于伯奈斯和希尔伯特来作为一个推论的扩展第一定理。本文的主要贡献是对推广的等式积分第一定理中Herbrand析取长度的上界和下界进行了分析。我们还表明，Herbrand的定理与平等的复杂性分析是一个简单的后果之一，扩展的第一个定理，由于莫泽和扎克没有平等。
2019-04-25 cs.LO math.LO
A New Game Equivalence and its Modal Logic
我们重新审视自然游戏等价的关键问题，以及基于这些的游戏逻辑的语义。我们提出的原因，调查更精细的概念，游戏等价比平等的标准权力，虽然停留短的模态互模拟。具体地说，我们提出了一个更细粒度的概念平等的“基本权力”，记录什么球员可以强迫加上他们留给别人做，互动的一个重要特征。正如我们详细解释的那样，这个概念更接近于博弈论的战略形式，同时仍然符合逻辑分析。我们通过一个新的表示定理确定基本权力的属性，找到一个匹配的“即时邻居博弈逻辑”，并展示了我们的分析可以扩展到一个新的博弈代数和动态博弈逻辑。
2017-07-27 cs.GT cs.LO
Extending Logical Neural Networks using First-Order Theories
Yale University（耶鲁大学）
逻辑神经网络（LNN）是一种结合了神经网络的学习能力和形式逻辑系统的符号推理能力的体系结构。LLN为程序员提供了通过逻辑公式隐式修改神经网络底层结构的能力。在本文中，我们利用这种抽象来扩展LNN，通过一阶理论来支持等式和函数符号。这种扩展通过显著增加LNN可以处理的问题类型来提高LNN的能力。作为概念的证明，我们增加了对一阶理论的平等IBM的LNN库的支持，并演示了如何引入这允许LNN库现在的原因表达式，而不需要作出唯一的名称假设。
2022-08-11 cs.AI cs.LO
Context Semantics, Linear Logic and Computational Complexity
我们表明，上下文语义可以卓有成效地应用于线性逻辑的证明规范化的定量分析。特别是，上下文语义让我们定义一个证明网的权重作为其内在复杂性的度量：它既是规范化时间的上限（模多项式开销，独立于约简策略），也是范式步骤数的下限（对于某些约简策略）。然后利用权证明强可靠性定理的各种子系统的线性逻辑，即初等线性逻辑，软线性逻辑和轻线性逻辑。
2006-10-04 cs.CC cs.LO
Parameterised Complexity of Propositional Inclusion and Independence Logic
本文系统研究命题包含逻辑与独立性逻辑中模型检查和可满足性的参数化复杂性，表明多数参数化下问题处于 FPT 或为 paraNP 完全。
2023-07-13 cs.CC cs.LO
The Complexity of Reasoning for Fragments of Autoepistemic Logic
自认知逻辑通过模态算子L扩展命题逻辑。前面有L的公式被称为“相信”。该逻辑由Moore在1985年引入，用于对理想理性主体的行为和对自己信念的推理进行建模。本文分析了自认知逻辑中所有布尔片断的三个最常见的决策问题--扩展存在、勇敢推理和谨慎推理的计算复杂性。作为第二个贡献，我们分类的计算复杂性计数的数量稳定的扩展一个给定的知识库。据我们所知，这是第一篇分析自认知逻辑计数问题的论文。
2010-06-01 cs.CC cs.LO
On the Complexity of Elementary Modal Logics
模态逻辑在计算机科学中有着广泛的应用。自20世纪70年代以来，模态可满足性问题的复杂性一直在研究，通常是在逐个案例的基础上证明结果。我们证明了一个非常普遍的分类广泛的一类相关的逻辑：模态逻辑的许多重要的子类可以通过限制允许的模型与一阶霍恩公式。我们证明了这些逻辑的可满足性问题是NP完全的或PSPACE困难的，并展示了一个简单的分类标准。此外，我们证明了许多PSPACE硬逻辑匹配的PSPACE上界。
2008-02-13 cs.CC cs.LO
The Complexity of Satisfiability in Non-Iterated and Iterated Probabilistic Logics
设L是经典命题逻辑的某种扩展。L上的非迭代概率逻辑是通过在L语言中添加非嵌套概率算子而定义的逻辑PL。例如，在PL中，我们可以表达这样的陈述“A的真实性概率为0.3”，其中A是L的公式。L上的迭代概率逻辑是逻辑PPL，其中概率运算符可以迭代（嵌套）。例如，在PPL中，我们可以表达这样的语句“这枚硬币是伪造的概率为0.6”。本文研究了概率算子对PL和PPL中可满足性复杂性的影响，得到了上述可满足性问题的复杂性界，该复杂性界是以既没有概率算子也没有经典算子作为顶连接符的正负公式的合取可满足性复杂性为参数的.作为我们的结果的应用，我们得到了紧的复杂性界的可满足性问题在PL和PPL时，L是经典的命题逻辑或理由逻辑。
2019-02-10 cs.CC cs.LO
Computational Complexity of Deciding Provability in Linear Logic and its Fragments
线性逻辑由Girard于1987年提出，与经典逻辑不同，它限制了弱化和收缩的结构推理规则的使用。这样，逻辑的原子就不再被解释为真理，而是被解释为信息或资源。这种解释使得线性逻辑成为数学和计算机科学中形式化的有用工具。例如，线性逻辑在证明论、量子逻辑和程序设计语言理论中得到了应用。逻辑的一个中心问题是一个给定的公式列表是否可以用微积分证明。在对这一问题复杂性的研究中，取得了一定的成果，但也存在一些问题。为了提出这些问题，并给出新的观点，本文由三个主要部分组成，它们相互建立：我们提出了语法，证明理论，和各种方法的语义线性逻辑。在这里，我们将遇到一些开放的研究问题。我们目前的状态复杂性理论表征的最重要的片段的线性逻辑。在这里，提出了进一步的研究问题，很明显，到目前为止，结果都使用了不同的方法。我们证明了一个原始的复杂性表征的逻辑片段，并提出了一个新的，结构性的方法来检查线性逻辑的可证明性的想法。
2021-09-28 cs.CC cs.LO
Complexity of two-variable Dependence Logic and IF-Logic
我们研究了依赖逻辑和独立友好逻辑的双变量片段D^2和IF^2。我们考虑了这些逻辑的可满足性和有限可满足性问题，并证明了对于D^2，这两个问题都是NEXPTIME-完全的，而对于IF^2，这两个问题是不可判定的。我们还证明了D^2的表达性严格低于IF^2，并且在D^2中已经可以表达两个一元谓词的等价性和无穷大（后者在存在常数符号的情况下）。这是第26届IEEE计算机科学逻辑研讨会（LICS 2011）会议录中出版物的扩展版本。
2011-04-15 cs.CC cs.LO
Quirky Quantifiers: Optimal Models and Complexity of Computation Tree Logic
从计算复杂性的角度研究了分支时间逻辑CTL的可满足性问题。严格的上限和下限提供了每个时间操作符片段。在平行，最小模型的大小进行了研究，一个合适的概念极小。第三，研究了平坦的CTL，即，时态运算符嵌套深度非常低的公式。在复杂性和最小模型方面显示出尖锐的二分法：时间深度1具有低表达能力，而时间深度2相当于完整的CTL。
2017-02-24 cs.CC cs.LO
Closing a Gap in the Complexity of Refinement Modal Logic
精化模态逻辑（Refinement Modal Logic，RML），最近由Bozzelli等人提出，模态逻辑是经典模态逻辑的扩展，它允许人们对变化的模型进行推理。在本文中，我们研究与此逻辑相关的计算复杂性问题，解决了许多悬而未决的问题。具体来说，我们研究的复杂性，满足性的存在片段的RML，Bozzelli，范Ditmarsch和Pinchinat提出的问题。我们的主要结果是一个紧PSPACE上界这个问题，我们通过引入一个新的表系统实现。作为一个直接的后果，我们得到了严格的表征的复杂性RML可满足的任何固定数量的交替的细化量词。此外，通过一个简单的减少，我们建立RML的模型检验问题是PSPACE完全的，即使是一个单一的量词的公式。
2013-09-20 cs.CC cs.LO
The Complexity of Reasoning for Fragments of Default Logic
缺省逻辑是由Reiter在1980年提出的。1992年Gottlob将命题缺省逻辑的延拓存在问题的复杂性分类为$\SigmaPtwo$ -完全问题，将轻信和怀疑推理问题的复杂性分类为SigmaP 2-完全问题。PiP 2-完成。此外，他还研究了默认规则的限制，即，半正常默认规则。Selman在1992年提出了类似的方法，使用了无析取和一元缺省规则。本文系统地限定了允许命题连接词的集合。我们给出了一个完整的复杂性分类的所有集合的布尔函数的Post格的意义上的所有三个常见的决策问题的命题缺省逻辑。我们表明，复杂性是一个hexachotomy（SigmaP 2-，DeltaP 2-，NP-，P-，NL-完全，平凡）的扩展存在问题，而对于轻信和怀疑推理问题，我们得到类似的分类没有平凡的情况。
2010-08-23 cs.CC cs.LO
The Fluted Fragment with Transitive Relations
本文研究扩展传递关系的 fluted 片段可满足性，证明单传递关系加等词仍可判定，而三传递关系或两传递关系加等词在二变量片段中已不可判定。
2020-06-19 cs.LO
Nested Sequents for Horn-Characterizable Quantified Modal Logics with Equality via Reachability Rules
Technische Universität Dresden（德累斯顿工业大学）；University of Bologna（博洛尼亚大学）
本文提出了一种无割的嵌套序列系统，用于处理具有内外域的量模态逻辑，通过可达规则实现域条件的自然定义，并证明了系统的完备性和证明论性质。
2026-04-20 cs.LO math.LO
Expressiveness of SHACL Features and Extensions for Full Equality and Disjointness Tests
本文研究 SHACL 中相等性测试、不相交性测试、闭包约束及 targets 限制的表达力，证明四个特性均为原始特性，并证明加入完全相等性或不相交性测试可严格增强语言能力。
2024-02-20 cs.LO
Abstraction Logic: A New Foundation for (Computer) Mathematics
抽象逻辑是一种新的逻辑，是数学的基础。它结合了谓词逻辑和高阶逻辑的特征：抽象逻辑既可以被看作是高阶逻辑减去静态类型，也可以被看作是谓词逻辑加上运算符和变量绑定。我们认为，抽象逻辑是最好的基础逻辑可能，因为它最大限度地提高了简单性和实际的表达能力。这一论点得到了以下观察的支持：抽象逻辑比所有其他一般逻辑具有更简单的术语和更简单的证明概念。同时，抽象逻辑可以形式化直觉主义的和经典的抽象逻辑，并且对于这些逻辑和所有其他用等式扩展演绎逻辑的逻辑都是可靠和完备的。
2022-07-12 cs.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
Axiomatizations for downward XPath on Data Trees
我们用“相等”或“不等”的数据检验，并包含单一的“孩子”轴，给出了合理的和完整的公理化。这种数据感知逻辑对数据树进行预测，数据树是类似树的结构，其每个节点都包含来自有限字母表的标签和来自无限域的数据值。该语言允许我们比较两个节点的数据值，但不能访问数据值本身（即没有常量比较）。我们的公理是在方程逻辑的风格，扩展的公理化的数据不经意的推理，由B。10凯特，T. Litak和M.马克思我们公理化了完整的逻辑与测试的“平等”和“不平等”，也是一个简单的片段与“平等”的测试。我们的公理化适用于节点表达式和路径表达式。完备性的证明依赖于一个新的范式定理，用于数据测试的可重构性。
2017-03-13 cs.DB cs.LO math.LO
Undecidability of Equality in the Free Locally Cartesian Closed Category (Extended version)
我们证明了一个具有外延单位型I、单位型N1、Sigma型、Pi型和基型的马丁-洛夫类型论是一个自由范畴，它具有1范畴和2范畴意义上的族（支持这些类型型）。它遵循的基础范畴的背景是一个自由的局部carbohydrate闭范畴在2范畴的意义，因为以前证明的双等价。我们表明，在这个范畴中的平等是不可判定的，通过减少它的不可判定性的组合逻辑中的可转换性。本质上，同样的构造也显示了结果的一种稍微加强的形式，即在具有一个宇宙的延拓马丁-勒夫类型论中相等是不可判定的。
2017-11-28 cs.LO
Logic Column 17: A Rendezvous of Logic, Complexity, and Algebra
本文综述了最近的进展，应用代数技术的约束满足问题。
2006-11-03 cs.LO
Model checking memoryful linear-time logics over one-counter automata
我们研究的复杂性的LTL与寄存器（也称为冻结LTL）和一阶逻辑的数据相等性测试在一个计数器自动机的模型检查问题。我们考虑几类一计数器自动机（主要是确定性与非确定性）和几个逻辑片段（限制寄存器或变量的数量和使用命题变量的控制位置）。逻辑能够存储计数器值，并在以后根据当前计数器值对其进行测试。我们证明了在确定性单计数器自动机上的模型检验是PSPACE完备的，具有无限和有限的接受运行。通过对非确定单计数器自动机的分析，证明了在不确定单计数器自动机上，直到算子仅限于最终算子的模型检验冻结LTL是不可判定的，即使只使用一个寄存器且不使用命题变量.作为我们证明的推论，这也适用于数据相等性测试仅限于两个变量的一阶逻辑。这使得一个事实，即一计数器自动机的几个验证问题是已知的相对较低的复杂性是可判定的，并且两个逻辑的有限可满足性是可判定的。我们的研究结果铺平了道路，模型检查记忆（线性时间）逻辑在其他类别的操作模型，如反向有界计数器机。
2010-01-18 cs.LO
Real-Time Model-Checking: Parameters everywhere
本文研究离散时间自动机上逻辑TCTL的模型检验和参数综合问题，其中参数在模型（时间自动机）和属性（时态公式）中都允许.我们的结果如下。在消极的一面，我们表明，模型检验问题的TCTL扩展参数是不可判定的离散时间自动机只有一个参数时钟。不可判定性结果需要逻辑上的等价性。在积极的一面，我们表明，模型检验和参数合成问题成为可判定的一个片段的逻辑是不允许的平等。我们的方法是基于自动机理论的原则和扩展我们的方法来表示时间自动机使用Presburger算法的运行持续时间。
2007-02-27 cs.LO
Complexity Thresholds in Inclusion Logic
具有团队语义的逻辑为复杂性类的逻辑表征提供了替代手段。依赖和独立逻辑都被认为可以捕获非确定性的多项式时间，并且这些逻辑中的易处理性的边界被相对较好地理解。包含逻辑类似于这些基于团队的逻辑形式主义，除了它对应于有序模型中的确定性多项式时间。在这篇文章中，我们研究包含逻辑的语法片段和不同的复杂性类之间的连接，在两个计算问题：最大的子组成员和模型检验问题的一个固定的包含逻辑公式。我们发现，非常简单的量词免费公式与一个或两个包含原子产生的这些问题是完整的（非确定性）对数空间和多项式时间的实例。此外，我们提出了一个片段的包含逻辑，捕捉非确定性的对数空间有序模型。
2019-03-26 cs.CC cs.DB cs.LO
Complexity of Propositional Logics in Team Semantics
我们分类的可满足性，有效性和模型检测问题的命题独立性，包含性和团队逻辑的计算复杂性。我们的主要结果表明，命题组逻辑的可满足性和有效性问题是完全的交替指数时间与多项式多交替。
2017-01-05 cs.CC cs.LO math.LO
Cubical Syntax for Reflection-Free Extensional Equality
我们贡献XTT，观察类型论的立体重建，扩展马丁-洛夫的内涵类型论与依赖的平等类型，享有功能扩展性和判断版本的唯一性的身份类型原则（UIP）：任何两个元素相同的平等类型是判断平等的。此外，我们推测，类型关系可以决定在一个实用的方式。在本文中，我们建立了一个代数规范性定理，使用一个新的立方扩展（独立提出的Awodey）的逻辑家庭或范畴胶合参数的启发Coquand和Shulman：每一个封闭的布尔类型的元素是可导等于要么“真”或“假”。
2019-06-06 cs.LO math.LO
A Parameterized Complexity View on Description Logic Reasoning
Institute for Logic, Language and Computation（逻辑、语言与计算研究所）；University of Amsterdam（阿姆斯特丹大学）
描述逻辑是一种知识表示语言，它被设计成在表达性和计算易处理性之间取得平衡。许多不同的描述逻辑已经被开发出来，并且这些逻辑的许多计算问题由于它们的计算复杂性而被研究。然而，基本上所有的复杂性分析的推理问题的描述逻辑使用的经典复杂性理论的一维框架。参数化复杂性理论的多维框架能够提供推理问题复杂性的更详细的图像。在本文中，我们认为，参数化复杂性的框架有很多可以提供的描述逻辑推理问题的复杂性分析-当一个人需要一个渐进的和前瞻性的观点参数化的复杂性工具。我们通过三个案例研究来证实我们的论点。第一个案例研究的问题是概念可满足的逻辑ALC关于近无环的TBox。第二个案例研究关注ALC概念的可满足性，其参数由联合算子的出现次数和完全存在量化的出现次数来确定。第三个案例研究从参数化复杂性的角度对数据复杂性结果进行了批判性的审视。这三个案例研究代表了描述逻辑问题的参数化复杂性方法的广泛应用。
2018-08-11 cs.AI cs.CC cs.LO
Alternating Quantifiers in Uniform One-Dimensional Fragments with an Excursion into Three-Variable Logic
本文研究一致一维逻辑中在量词块内交替使用全称与存在量词，给出两种无等式限制，证明其具有有限指数模型性质且可满足性为 NExpTime 完全，并扩展到三变量逻辑的丰富子片段。
2025-03-14 cs.LO
Data Complexity and Rewritability of Ontology-Mediated Queries in Metric Temporal Logic under the Event-Based Semantics (Full Version)
Birkbeck, University of London（伦敦大学伯贝克学院）；University of Oxford（牛津大学）；University of Warsaw（华沙大学）
我们调查的数据复杂性的基于事件的语义下，假设数据实例是有限时间的字时间戳与二进制分数的度量时态逻辑本体介导的回答查询。我们确定类的本体介导的查询回答，可以在AC0，NC1，L，NL，P，和coNP的数据复杂性，提供他们的重写一阶逻辑及其扩展与原始递归，传递闭包或databases，并建立较低的复杂性界限。
2019-07-01 cs.AI cs.CC cs.LO
Automata for two-variable logic over trees with ordered data values
数据树是其中每个节点除了携带来自有限字母表的标签之外，还携带来自无限域的数据值的树。它们已被用作{XML}推理任务和验证的抽象模型。然而，大多数现有的方法考虑的情况下，只有平等测试可以对数据值进行。本文研究了数据值来自线性有序域的数据树，除了相等性检验外，还可以检验一个节点上的数据值是否大于另一个节点上的数据值。我们引入了一个自动机模型，我们称之为有序数据树自动机（ODTA），提供了它的逻辑特征，并证明了它的非空性问题是可判定的3-NEXPTIME。我们还表明，两个变量逻辑上的无秩树，研究Bojanczyk，Muscholl，Schwentik和Segoufin在2009年，正好对应于一个特殊的子类，这个自动机模型。然后，我们定义了一个稍微弱的版本的ODTA，我们称之为弱ODTA，并提供其逻辑特性。非空性问题的复杂性下降到NP。然而，一些现有的形式主义和模型的研究文献中可以捕获已经弱ODTA。我们还表明，ODTA的定义可以很容易地修改，的情况下，数据值来自一个树状偏序域，如字符串。
2013-10-04 cs.LO
The Complexity of Probabilistic Justification Logic
概率证明逻辑是一种有两种模态的模态逻辑：概率测度和显式证明项。我们提出了一个表程序，可以用来决定满足性问题，这种逻辑在多项式空间。我们证明了这个复杂性上界是紧的。
2017-08-14 cs.LO
The Complexity of Non-Iterated Probabilistic Justification Logic
逻辑PJ是一个概率逻辑，通过添加（非迭代）的概率运算符的基本理由逻辑J。在本文中，我们建立了上界和下界的逻辑PJ的可导性问题的复杂性。本文的主要结果是PJ中的可导性问题的复杂性与底层逻辑J中的可导性问题的复杂性保持相同，这是PJ中的可导性问题的复杂性，是PJ中的可导性问题的复杂性是PJ中的可导性是PJ中这意味着，概率运算符不会增加逻辑的复杂性，尽管它们可以说丰富了语言的表达能力。
2018-07-05 cs.LO
An Application of the Feferman-Vaught Theorem to Automata and Logics for<br> Words over an Infinite Alphabet
我们表明，一个特殊的情况下，Feferman-Vaught组合定理产生了一个自然的概念，自动机的有限字在一个无限的字母表，具有良好的封闭性和可判定性，以及一些逻辑刻画。我们还考虑了一个轻微的扩展的Feferman-Vaught形式主义，它允许表达更多的组件值之间的关系（如平等），并证明相关的可判定性结果。从这个结果，我们得到了新的类的可判定逻辑的词在一个无限的字母表。
2008-03-25 cs.LO
On the Existential Fragments of Local First-Order Logics with Data
我们研究无序结构上的一阶逻辑，无序结构的元素携带来自无限域的有限数量的数据值，这些数据值可以被比较。平等的由于这种逻辑的可满足性问题一般是不可判定的，在以前的工作中，我们已经引入了一个家庭的本地片段，限制量化到一个给定的参考点的邻域。我们在这里提供的精确的复杂性表征的可满足性问题的存在性片段的本地逻辑取决于每个元素所携带的数据值的数量和所考虑的邻域的半径。
2022-09-21 cs.LO
SCL with Theory Constraints
我们提升了SCL演算的一阶逻辑没有等式的SCL（T）演算的一阶逻辑没有等式模的背景理论。简而言之，SCL（T）演算描述了一种通过部分模型假设而不是先验固定顺序来指导分层分辨率推断的新方法，例如在分层叠加中所做的。模型表示由地面背景理论文字和地面前景一阶文字组成。模型引导方法的一个主要优点是SCL（T）生成的子句具有非冗余特性，这使得对重言式和前向包含的昂贵测试完全过时。SCL（T）是一个用于纯子句集的半判定过程，纯子句集是没有一阶函数符号的子句集，其范围为背景理论排序。此外，SCL（T）可以变成一个决策过程，如果所考虑的组合的一阶逻辑模的背景理论享有一个抽象的有限模型属性。
2020-10-22 cs.LO
The complexity of admissible rules of Łukasiewicz logic
研究了无穷值命题逻辑中推理规则的可容许性的计算复杂性。在[13]中，证明了在PSPACE中可检验的是在PSPACE中的可容许性。我们确定这个结果是最优的，即，可容许规则是PSPACE完备的。与此相反，可导出的规则是coNP-完全的。
2012-02-28 cs.CC cs.LO math.LO
