MMMay, 2024

一种基于存在图的系统命题公式简化框架

PDF
TL;DR本文介绍了一种基于 Peirce 的存在图推理和蕴含图的命题逻辑简化演算法，该算法可以应用于嵌套形式的命题逻辑公式，保持等价性、保证变量、子句和文字数量的单调递减，并最大限度地保留结构问题信息；同时，提出了一个系统化应用两个规则（EPR 和 TWSR）的简化过程，可用于简化大型布尔可满足性问题和任意形式的命题公式，并对其在空间和时间方面进行了算法复杂性的形式分析；最后，展示了如何通过引入一种新的 n 元蕴含图扩展我们的规则，以涵盖所有已知的等价性保持预处理过程。
simplification calculuspropositional logicexistential graphsequivalence-preservingsat preprocessing
发现论文，激发创造
  • 概率定理证明

    该论文提出了一种将概率论和第一阶逻辑相结合的方法，在有限域内具有 Herbrand 解释的情况下，定义了概率证明定理及其推广问题，然后提出了能够同时拥有图模型推理和一阶定理证明的完整能力的方法，并开发了一种高效算法。实验表明，当逻辑结构存在时，该算法远优于目前已有的方法。

    Feb, 2012

  • 命题蕴涵的复杂性

    本研究考察了基于一组有限的布尔连结词所建立的命题公式的子句集合 G 是否蕴含某个公式 f 的复杂性，并证明了只有当连结词可由 {false，true} 和 {and，or，xor} 定义时，蕴含问题才能有效求解，此时问题的复杂度为多项式级别，否则问题的复杂度仍然是 coNP 完备的，并且还考虑了 G 被限制为单元素的情况。

    Nov, 2008

  • 可判定存在规则集的派生图表征

    本文通过建立新的概念来对存在性规则集进行表征探究，特别是在有限制下的集合，在其多项式时间内具有查询蕴含。

    Jul, 2023

  • 结合存在规则和传递性：下一步

    本文探讨存在规则作为本体规范的形式化方法，重点研究了如何将传递性与可判定类的存在规则组合，并给出了能够安全添加传递性的情况和相应的查询重写算法。

    Apr, 2015

  • 知识图谱上存在性一阶查询的推理

    这篇论文通过系统检视问题之前的范围并提出一个新的数据集，讨论了同时出现的新挑战，并提出了一种模糊逻辑理论的新搜索算法，以解决新的公式并在现有公式中胜过以前的方法。

    Apr, 2023

  • 关系嵌入的提升规则注入

    本文提出了一种高效的基于关联规则的方法，将实体元组嵌入映射到近似布尔空间中，通过从 WordNet 中进行的关联规则挖掘来鼓励关系嵌入上的部分排序，以实现自动化知识库的构建。通过引入少量的常识规则，相较于矩阵分解基准方法，实现平均精度的 2 个百分点的提高，并观察到运行时间几乎没有增加。

    Jun, 2016

  • 发现强等价逻辑程序类

    本文应用计算机辅助定理发现技术，发现强等价逻辑程序在答案集语义下的定理，进而得到了新的程序化简规则。具体发现了关于规则和空集、两个规则、两个规则和其中一个规则、两个规则和另一个规则、以及三个规则和其中两个规则之间的强等价的确切条件。

    Oct, 2011

  • 存在规则的规范化：不是那么无害！

    该研究系统研究了存在性规则对于不同的追踪变体以及基于一阶逻辑的重写的 (chase (non-) termination and FO-rewritability) 影响，从而探讨了相关的开放性问题。

    Jun, 2022

  • 作为存在规则语言的 Notation3

    Notation3 逻辑（N3）是 RDF 的扩展，允许用户编写引入新的空白节点到 RDF 图中的规则；本文探讨了 N3 规则中带有空白节点的头部与存在规则的关系，并给出了一个等价的映射；研究结果表明存在规则的推理引擎在处理包含大量事实的用例时表现良好，而 EYE 推理引擎在处理大量依赖规则时非常快速。

    Aug, 2023

  • 平衡图

    本文提出一种 Peirce 存在图的扩展，以提供 Quantified Equilibrium Logic（QEL）表达式的图表表示。使用这种形式化方法，逻辑连接词被圆圈和正方形等区域所代替，量化变量则用 “身份” 线表示。虽然表达能力和 QEL 一样，但新的表示方法可用于说明或教育目的。

    Sep, 2016