Jun, 2023

哥德尔 - 邓梅特线性时间逻辑

PDF
TL;DR该研究探讨了一个版本的线性时态逻辑，其命题片段是 Godel-Dummett 逻辑，并使用了两种自然语义学，一种是真值语义学，另一种是双关系语义学，证明了这些语义定义了相同的逻辑，并提出了决定语句有效性的算法以及一个用于 Godel 临时逻辑的演绎演算法，从而证明了所有的有效语句都能够用这个演算法证明。
发现论文，激发创造
  • 在良基语义下，可反驳逻辑和逻辑编程的相互定义

    本文提出将 Nute's Defeasible Logic 理论转化为逻辑程序的方法，并提供相应的相反方向翻译。通过某些自然限制，使得 Defeasible Logic ADL 的推理结论与 Logic Program 的 Well-Founded Semantics 相一致，这样就可以证明这两种形式语言是密切相关的。

    Jun, 2011

  • 命题性可废弃逻辑具有线性时间复杂度

    使用具有严格和举止性规则以及规则优先关系的可撤销逻辑的命题形式可以在线性时间内进行推理，这与大多数其他命题非单调逻辑形成了鲜明对比。

    May, 2004

  • 关于带不确定性有限轨迹的时间逻辑（技术报告）

    提出了一种新的基于超定理解的概率时态逻辑，用于处理现实动态系统中的不确定性，探讨了逻辑的特性并提供了基于自动机的推断机制。同时，研究了具有更好计算性质的逻辑片段，可以通过现有的声明性流程发现技术从事件日志数据中发现公式。

    Mar, 2019

  • 实时和概率时态逻辑：一概述

    该论文分析了用于真实时间系统的逻辑规范和验证的逻辑符号，分别比较了它们的决策性，公理化程度，表达能力和模型检查等特征。

    May, 2010

  • 有限轨迹上的理论线性时序逻辑 (扩展版)

    本文提出了一种基于 Satisfiability Modulo Theories 的 Linear Temporal Logic 语言 ——LTLf Modulo Theories，该语言具有高表现力，可用于数据感知过程和规划的模型检验。我们提供了一种基于 SMT 编码的单遍树状表格系统的 LTLfMT 的半决策过程，并在黑色可满足检查工具中实现。实验结果表明了该算法在新型基准测试上的可行性。

    Apr, 2022

  • 无限模态逻辑：贝叶斯推理的半定量解释

    本文介绍了一个半定量的方法 —— 用阶数算术来将模态逻辑系统和贝叶斯推理结合起来。最终的系统可以将传统模态逻辑语义自然地，优雅地映射到新的系统中。我们声称该逻辑系统可以被完全有限地表述，并提供了对 “除去不可能的，剩下的，无论多么不可能都是真的” 这一句话的完美解释。此外，还证明了该逻辑系统的一个有限模型特性定理。

    Apr, 2022

  • 一种针对可反驳逻辑的模型论语义

    本文研究了可撤销逻辑的模型论语义。该逻辑具有证明论，并且在所提供的语义条件下是准确和完整的。同时，本文还简要概述了这种方法如何扩展到各种可撤销逻辑。

    Jul, 2002

  • 三个神话、一个谜题及其解决方案

    通过对阿拉伯语的基本原理进行研究，我们证明现代逻辑学中关于自然语言词汇用途、语法结构以及符号的理论与阿拉伯语存在矛盾，并提出了一种实用的方法来解决 3CNF 公式的产生问题，相关证据支持我们的论点。

    Oct, 2023

  • 可计数理论模型的可处理性及其在信念修正和真值维护中的应用

    本文介绍了可分解否定范式（DNNF）作为可行的命题理论形式，并提供了一些在多项式时间内可以执行的强大逻辑操作。在此基础上，本文提出了将任何合取范式（CNF）转化为 DNNF 的算法，并提供其空间和时间复杂度上的结构保证。同时它也介绍了将有序二叉决策图（OBDD）表示的命题理论转换为等价的 DNNF 的线性时间算法。接着，介绍了采用新的操作在 d-DNNF 上遍历之后实现线性时间、完整的信念修正系统。

    Mar, 2000

  • 稳定模型语义的认知基础

    本文介绍了关于稳定模型语义的一种另类的认识论方法，探讨了稳定模型语义可以完全定义为 Kripke-Kleene 语义的扩展，证明了封闭世界假设可以看作是要累加到 Kripke-Kleene 语义上的一个 “虚假” 的附加来源。

    Mar, 2004