May, 2023

SCL (FOL) 能模拟非冗余叠加子句学习

PDF
TL;DR通过固定减少顺序，基于超前法逻辑来推导非冗余子句，本研究展示了 SCL (FOL) 可以模拟无相等符号的一阶逻辑。我们建立一个地面部分模型，根据固定的顺序来执行基于超前法的推理，其中假面积分的最小 false 地面实例触发非冗余超级位置推论。我们定义了 SCL 计算的相应策略，使得由 SCL 学习的子句和超前法推论的子句重合。从这个角度来看，SCL 计算可以被看作是超前法计算的一般化。
发现论文，激发创造
  • 认识与利用子句学习的潜力

    本文通过分析阐述了布尔可满足性问题中，采用了子句学习增强 DPLL 的实现方式是最高效的，并与已有的分辨规则证明体系相对照，证明了该方法在一些条件下可以提供更短的证明过程，且该算法可以通过利用问题结构，通过导向学习算法的方法取得指数性的加速。

    Jun, 2011

  • 信息过载：CDCL 求解器为何需要遗忘已学子句

    文章发现适当的子句学习可以促进 CDCL 求解器的性能，但在某些情况下，此方法可能会大大降低求解过程，这主要来自 CDCL 求解器具有多峰运行时间分布。通过使用威布尔混合分布来描述这种多峰分布，得出遗忘子句在 CDCL 求解器中对于优化单元传播速度外还有其它应用的结论。

    Feb, 2022

  • 无 Lambda 高阶逻辑叠加

    本研究介绍了反证完成的超位置演算法，用于意图性和外延句子 $\lambda$- 自由高阶逻辑，这两种形式允许部分应用和应用变量。 这些演算法由一个术语排序参数化，无需完全单调，从而可以采用 $\lambda$- 自由高阶词典路径和 Knuth-Bendix 排序。作者们在 Zipperposition prover 中实现了这些演算法，并在 Isabelle/HOL 和 TPTP 基准测试中评估它们。 它们似乎是通向完全高效自动定理证明程序的一个重要的步骤。

    May, 2020

  • 延迟统一的叠加

    将统一规则移动到演算水平可提高欠定规则推理系统的完备性和效率

    Feb, 2024

  • 超冗余：一种用于布尔函数化简复杂度分析的工具

    本文探讨了超冗余子句和超不可约子句的概念，以及如何通过引入新变量将子句变为超不可约，从而证明最小公式大小的复杂性难题或在忘记变量或修订公式时确定大小。

    May, 2022

  • 选择逻辑及其计算性质

    提供了一个选择逻辑框架，探讨了强等价、计算复杂度的特性，为 Qualitative Choice Logic (QCL) 和 Conjunctive Choice Logic (CCL) 提供了新结果。

    Jun, 2021

  • 懒惰模型扩展：将基础与搜索交错

    论文提出一种延迟递归地进行理论理解，克服现有策略中的瓶颈问题，用于处理 ASP、FO (.)、Zinc 等类似的知识表示语言的模型生成问题。

    Feb, 2014

  • 描述逻辑中限缩的复杂性

    本文中，我们将关注于异常演绎的一种替代方法：减缩并研究经过限制的 DLs，在 ALC 到 ALCIO 和 ALCQO 之间寻找出推理的确切计算复杂度，范围从 NExpTime^NP 到不可判定。

    Jan, 2014

  • 挑战 SAT 求解中分辨率限制

    本文提出了一种新的问题转化方法，将 CNF 公式的决策问题转化为 Horn 公式的最大可满足性问题，并证明了在鸽笼公式的情况下 MaxSAT resolution steps 的数量存在多项式绑定。

    May, 2017

  • 具有类似语义的逻辑中的量表和修饰语

    通过 Context Logic 和 Activation Bit Vector Machine，可以解决 Fuzzy Logic 对复杂公式的处理不足，VSA 模型则提供了基于向量符号体系结构的内在图像处理机制，本文研究了如何处理形容词和动词语义的等级。

    Jan, 2022