Logic programs with monotone abstract constraint atoms
本文介绍并研究了子句由单调约束原子构成的逻辑程序。我们表明，一步证明算子的操作概念推广到单调约束原子的程序，但推广涉及非确定性。我们的主要结果表明，我们的形式化是一个共同的推广（1）正常的逻辑编程与其语义的模型，支持的模型和稳定的模型，（2）逻辑程序与重量原子（lparse程序）的语义的稳定模型，定义的Niemela，Simons和Soininen，（3）析取逻辑编程与可能的模型语义的Sakama和井上。
2006-08-25 cs.AI cs.LO
A Logic for Non-Monotone Inductive Definitions
著名的归纳法原理包括单调归纳法和各种非单调归纳法，如膨胀归纳法、良基集上的归纳法和迭代归纳法。在这项工作中，我们定义了一个逻辑形式化归纳良好的基础集和单调和迭代归纳。正如正归纳原理已在FO（LFP）中形式化，膨胀归纳原理已在FO（IFP）中形式化一样，本文在一种新的非单调归纳定义逻辑（ID-逻辑）中形式化了迭代归纳原理。逻辑的语义受到逻辑编程的良基语义的强烈影响。我们的主要结果是关于ID逻辑中归纳定义的模性质。具体而言，我们制定的条件下，同时定义$\D$的几个关系是逻辑上等同于一个连接的较小的定义$\D_1 \land ... \land \D_n$与不相交的定义谓词。这个结果的困难来自这样一个事实，即分别在$\D_i$和$\D_j$中定义的谓词$P_i$和$P_j$可以通过同时归纳相互连接。由于良基语义下的逻辑程序设计和溯因逻辑程序设计是我们的逻辑的适当片段，我们的模块性结果也适用于那里。
2005-01-13 cs.AI cs.LO
Parity Games and Automata for Game Logic (Extended Version)
Parikh的游戏逻辑是一个类似PDL的不动点逻辑，它在单调邻域框架上解释，表示玩家在确定的两人游戏中的战略力量。博弈逻辑转化为单调$μ$ -演算的一个片段，而单调模式自动机又在表达上等价于单调模式自动机。奇偶博弈和自动机是处理模态不动点逻辑（如模态$μ$ -演算）中嵌套不动点的组合复杂性的重要工具。本文（1）讨论了邻域结构上博弈逻辑的奇偶博弈语义a，（2）利用这些博弈得到了对应于博弈逻辑的单调$μ$ -演算片段的自动机理论刻画。我们的证明广泛使用的结构，我们称之为语法图，结合了易于使用的语法树的公式与自动机的灵活性和简洁性。它们本质上是一个基于图的观点的交替树自动机，介绍了威尔克在研究模态$μ$ -演算。
2017-09-03 cs.LO
Monadic Second-Order Logic and Bisimulation Invariance for Coalgebras
推广标准的一元二阶逻辑的Kripke模型，我们介绍了一元二阶逻辑解释的余代数的任意集函子。一元二阶逻辑树相似的知名结果，我们提供了一个翻译的这种逻辑到一类自动机，相对于类的coalgebras承认一个树状支持Kripke框架。然后，我们考虑公式的行为等价下的不变性，更特别地，我们调查是否coalgebraic μ演算是一元二阶逻辑的bisimulation不变片段。最近的结果的第三作者的基础上，我们表明，为了提供这样一个共代数推广的Janin-Walukiewicz定理，它足以找到我们所谓的一个适当的一致建设的函子。作为这个结果的应用，我们得到了Janin-Walukiewicz定理的部分新证明，以及袋函子（分次模态逻辑）和所有指数多项式函子的互模拟不变性结果。最后，我们考虑了单调邻域函子的一些细节，它为单调模态逻辑提供了共代数语义。事实证明，这个函子没有足够的统一构造，因此互模拟不变性的自动机理论方法不能直接应用。如果我们考虑邻域模型之间的全局互模拟，这个问题可以克服：我们的主要技术结果之一提供了一个表征的单调模态μ演算扩展与全球模态，作为片段的一元二阶逻辑的单调邻域函子是不变的全局互模拟。
2015-01-28 cs.LO
Satisfiability and Query Answering in Description Logics with Global and Local Cardinality Constraints
TU Dresden（德累斯顿工业大学）；University of Wrocław（弗罗茨瓦夫大学）
我们介绍和调查的表达描述逻辑（DL）ALCSCC++，在其中的全局和局部基数约束在以前的文件中介绍的可以混合。一方面，我们证明了这不会增加可满足性检查和其他标准推理问题的复杂性。另一方面，可满足性问题成为不可判定的，如果逆角色添加到语言。此外，即使没有相反的角色，合取查询蕴涵在这个DL原来是不可判定的。我们证明了查询的可判定性可以恢复，如果全局和局部约束不混合和全局约束适当的限制。后一个结果基于局部非循环模型构造，并且它将查询蕴涵减少到受限设置中的ABox一致性，即，到ABox一致性w.r.t. ALCSCC中的受限基数约束，我们可以显示ExpTime上限。
2020-02-14 cs.AI cs.LO
Intuitionistic Monotone Modal Logic: Proof Theory and Semantics
Free University of Bozen-Bolzano（博尔扎诺自由大学）；University of Bern（伯尔尼大学）
研究直觉主义单调模态逻辑IM，通过构造性邻域模型刻画其自然扩展族，提出基于经典单调模态逻辑M的结构演算，证明IM的可判定性，揭示M与K的构造性和直觉主义变体之间的类比。
2026-07-01 cs.LO math.LO
NP Reasoning in the Monotone $μ$-Calculus
单调模态逻辑的可满足性检验是NP完全的。我们表明，这仍然是真实的逻辑时，扩展与conjunctive和交替自由不动点算子以及通用模态;由此产生的逻辑-conjunctive交替自由单调$μ$ -演算与通用模态-包含并发命题动态逻辑（CPDL）和交替自由片段的游戏逻辑片段。我们得到了我们的结果，通过多项式多Eloise节点的Büchi游戏的可满足性的表征。
2020-05-04 cs.FL cs.GT cs.LO
NM-DEKL$^3_\infty$: A Three-Layer Non-Monotone Evolving Dependent Type Logic
NM-DEKL$^3_\infty$是一种用于形式化动态环境中演化知识的三层非单调依赖类型系统，具备正确性、等价完备性及对μ-演算的嵌入能力。
2026-03-02 cs.CL cs.LO
Uniform Lyndon interpolation for intuitionistic monotone modal logic
本文证明了直觉单调模态逻辑$\mathsf{iM}$具有一致Lyndon插值性质性质（ULIP）.逻辑$\mathsf{iM}$是一种基于直觉的非正规模态逻辑，而ULIP属性是插值的加强，其中插值只依赖于蕴涵的前提或结论，并尊重命题变元的极性。我们的方法来证明ULIP产生明确的一致插值，并利用了一个终止的微积分$\mathsf{iM}$，我们已经为此目的开发。据我们所知，$\mathsf{iM}$具有ULIP和一个终止的逻辑演算的结果是第一个直觉非正规模态逻辑的结果。然而，而不是证明这些特定的结果，我们的目的是显示的建设性证明理论方法，我们用来证明ULIP的灵活性。它在过去几年中得到了发展，并已被应用于子结构，中间，经典（非）正规模态和直觉正规模态逻辑。根据这些结果，直觉非正规模态逻辑似乎是一个自然的下一类尝试应用该方法，我们在这方面迈出了第一步。
2022-08-09 cs.LO math.LO
A Sequent Calculus for Non-Monotone Inductive Definitions
KU Leuven（荷语鲁汶大学）；Vrije Universiteit Brussel（布鲁塞尔自由大学）
本文提出SCFO(ID)演算，用于处理非单调归纳定义，通过稳定语义验证其理论性质，支持对一般归纳定义的定理形式化证明。
2026-09-23 cs.LO
Completeness for Game Logic
游戏逻辑是由Rohit Parikh在20世纪80年代引入的，作为命题动态逻辑（propositional dynamic logic，PDL）的推广，用于推理玩家在确定的2人游戏中可以强制执行的结果。从语义上讲，从程序到游戏的概括是通过从Kripke模型到单调邻域模型来反映的。Parikh提出了一个自然的PDL风格的希尔伯特系统，它很容易被证明是合理的，但它的完备性迄今为止仍然是一个开放的问题。在本文中，我们介绍了一个切免费的游戏逻辑的mu演算，和两个切免费的mu演算，操作注释公式，一个游戏逻辑和一个单调的μ演算，多模态μ演算的变体，其中的语义是由单调邻域模型，而不是Kripke结构。我们表明这些系统是健全的和完整的，帕里克的公理化的完整性如下。我们的方法建立在Afshari & Leigh（LICS 2017）最近的想法和结果的基础上，我们通过系统之间的一系列证明转换来获得完整性。一个关键的要素是从博弈逻辑到单调μ演算的有效性保持翻译。
2019-04-30 cs.LO math.LO
Concrete Domains Meet Expressive Cardinality Restrictions in Description Logics (Extended Version)
本文结合具体域与数字限制，提出DL $\mathcal{ALCOSCC}(\mathfrak{D})$，证明其一致性问题是ExpTime完全的，且某些自然扩展会导致不可判定性。
2025-05-27 cs.LO
Positive and monotone fragments of FO and LTL
本文研究有限字上正逻辑FO+及其片段，证明其与LTL+等逻辑的等价性，并给出一个FO可定义但非FO+可定义的单调语言反例，且该反例不可由FO2定义。
2024-06-25 cs.FL cs.LO
First-Order Query Evaluation with Cardinality Conditions
RWTH Aachen University（亚琛工业大学）；Humboldt-Universität zu Berlin（柏林洪堡大学）
研究带基数条件的一阶逻辑FOC(P)的查询评估问题，证明其在有界度类上可固定参数处理，但在无界度类上不可推广，并识别出在无处稠密类上仍可固定参数处理的片段FOC_1(P)。
2026-06-15 cs.DB cs.DS cs.LO
Moss' logic for ordered coalgebras
本文为有序余代数提出一种有限性 Moss 余代数逻辑，采用单一覆盖模态和关系提升语义，证明了 Hennessy-Milner 性质并给出完备的相继式证明系统。
2022-08-06 cs.LO
Spectra of Cardinality Queries over Description Logic Knowledge Bases
Leipzig University（莱比锡大学）；Center for Scalable Data Analytics and Artificial Intelligence (ScaDS.AI)（可扩展数据分析与人工智能中心（ScaDS.AI））；University of Warsaw（华沙大学）
本文研究描述逻辑知识库上原子计数查询的谱，刻画了$\mathcal{ALCIF}$及其子逻辑中谱的形状，并提出有效表示方法，证明了计算复杂度为$\mathsf{FP}^{\mathsf{NP}[\log]}$-完全。
2024-12-17 cs.AI cs.CC cs.LO
Kripke Completeness of Strictly Positive Modal Logics over Meet-semilattices with Operators
University of Oxford（牛津大学）；Birkbeck, University of London（伦敦大学伯贝克学院）；Institute for Information Transmission Problems（信息传输问题研究所）；Moscow Institute of Physics and Technology（莫斯科物理技术学院）；King’s College London（伦敦国王学院）；Kyushu Sangyo University（九州产业大学）；University of Liverpool（利物浦大学）
本文研究严格正模态逻辑在meet-半格上的Kripke完备性，探讨两种语义是否定义相同后果关系。
2019-03-22 cs.LO
A monotone connection between model class size and description length
本文将模型类的大小与其定义公式的最小长度联系起来，即与其描述的复杂性联系起来。限制到一个固定的域的大小为n的模型，我们研究描述的复杂性与命题逻辑的扩展与计数分配的能力。这种逻辑称为GMLU，也可以被认为是Kripke模型上的分级模态逻辑。虽然GMLU是表达完整的定义多集的分配，我们也研究它的片段GMLU（d），只能计数到整数阈值d。我们特别关注GMLU（d）的等价类的描述复杂性。我们表明，在限制的偏序集的类型实现，基于大小的等价类的顺序是相同的顺序基于描述复杂性。这也证明了模型类的玻尔兹曼熵和描述复杂性之间的单调联系。此外，我们刻画了域大小n和计数阈值d之间的关系如何决定是否存在一个支配类，这实质上意味着一个模型类的极限概率为1。为了得到我们的结果，我们证明了新的估计r-相关的斯特林数。作为另一个重要的工具，我们表明，模型类分为两个不同的情况下，其描述的复杂性。
2023-01-31 cs.LO math.LO
A Rational Entailment for Expressive Description Logics via Description Logic Programs
ISTI - CNR（意大利国家研究委员会信息科学与技术研究所）；CAIR - University of Cape Town（开普敦大学CAIR）
Lehmann和Magidor的有理闭包被认为是非单调逻辑领域的一个里程碑，它也在描述逻辑（DL）的背景下被重新表述。我们在这里展示了如何建模的合理形式的蕴涵表达DL，如SROIQ，提供了一种新的推理过程，编译成一个描述逻辑程序（DL程序）的非单调DL知识库。
2021-06-28 cs.AI cs.LO
Łukasiewicz μ-calculus
本文探讨了ukasiewicz μ-演算的性质，或简称μ，它是ukasiewicz逻辑的一个扩展，具有标量乘法和最小和最大不动点算子（用于单调公式）。我们观察到，具有$n$变量的μ项定义了从$[0, 1]^n$到$[0, 1]$的单调分段线性函数。本文提出了两种计算有理输入下的双μ项输出的有效方法。然后我们考虑通过将盒模态和菱形模态添加到μ-演算而得到的μ-演算。或者，它可以被看作是Kozen的模态μ演算适用于概率非确定性转移系统（PNTS）的推广。我们展示了如何在著名的逻辑PCTL中表达的属性可以被编码为Mukasiewicz模态μ演算公式。我们还表明，算法计算值的ukasiewicz μ-演算条款提供自动（虽然不切实际）的方法验证ukasiewicz模态μ-演算性质的有限理性PNTS的。
2015-10-03 cs.LO
A universal-algebraic proof of the complexity dichotomy for Monotone Monadic SNP
MMSNP逻辑是存在二阶逻辑的一个限制性片段，它允许表达图论和有限模型理论中许多有趣的查询。该逻辑由Feder和Vardi引入，他们表明每个MMSNP语句在计算上等价于有限域约束满足问题（CSP）;所涉及的概率约简由Kun使用扩展结构的显式构造去随机化。我们提出了一个新的证明减少到有限域CSP不依赖于昆的结果。这个新的证明使我们能够得到一个更强的声明，并验证更一般的Bodirsky-Pinsker二分法猜想的CSP在MMSNP。我们的方法利用了这样一个事实，即每个MMSNP语句描述了可数无限$ω$ -范畴结构的CSP的有限并集;此外，根据Hubička和Nešetzil最近的结果，这些结构可以扩展到具有有限关系签名和Ramsey性质的同构结构。这使得我们能够使用泛代数方法来研究MMSNP的计算复杂性。
2020-11-25 cs.CC cs.LO math.LO
A General Framework for Sound and Complete Floyd-Hoare Logics
本文将霍尔逻辑抽象为可追踪的对称monoidal范畴，这是系统理论的一个非常一般的框架。我们的抽象是基于一个跟踪monoidal函子从任意跟踪monoidal范畴到范畴的前序和单调关系。我们给出了几个例子，我们的理论如何概括通常的霍尔逻辑（部分正确的，而程序，部分正确的指针程序），并提供了一些案例研究，它可以用来开发新的霍尔逻辑（运行时分析，而程序和流电路）。
2008-07-07 cs.LO cs.OH
Games for Topological Fixpoint Logic
拓扑不动点逻辑是一个允许拓扑模型的逻辑族，其中不动点算子是关于拓扑解释定义的。在这里，我们考虑一个拓扑不动点逻辑的关系结构的基础上石空间，不动点算子解释通过闭集。我们开发了一个博弈论的语义这个逻辑。首先介绍Stone空间上单调算子闭不动点的博弈刻画。这些不动点游戏允许我们使用两个玩家的图形游戏来描述我们的拓扑不动点逻辑的语义。这是本文的主要结果。最后，我们定义了所考虑的拓扑结构的互模拟，并使用我们的游戏语义来证明我们的拓扑不动点逻辑公式的真理是互模拟不变的。
2016-09-14 cs.GT cs.LO
LPC(ID): A Sequent Calculus Proof System for Propositional Logic Extended with Inductive Definitions
Carnegie Mellon University（卡内基梅隆大学）；Katholieke Universiteit Leuven（鲁汶大学）
逻辑FO（ID）使用来自逻辑编程领域的思想来扩展具有非单调归纳定义的一阶逻辑。这种逻辑形式上扩展了逻辑程序设计、溯因逻辑程序设计和数据逻辑，从而将对这些形式主义的看法形式化为（广义）归纳定义的逻辑。本文的目标是研究FO（ID）的命题片段PC（ID）的演绎推理方法。我们引入了一个正式的证明系统的基础上的演算（根森式演绎系统），这种逻辑。由于PC（ID）是经典命题逻辑和命题归纳定义的集成，我们的推理演算证明系统集成了命题演算和定义的推理规则。我们提出了这个证明系统的可靠性和完整性，相对于PC（ID）的一个略有限制的片段。我们还提供了PC（ID）的一些复杂性结果。通过对PC（ID）证明系统的开发，有助于加深对FO（ID）证明理论基础的理解，从而研究FO（ID）的有效证明系统。
2012-07-11 cs.AI cs.LO
