Feb, 2023

基于度量的解析结构抽象逻辑系统的 Lindstrom 可刻画性

PDF
TL;DR该论文主要探讨了一些逻辑系统及其特性，包括一种基于度量（解析结构）的谓词逻辑系统，其定义了一种新型满足性，是描述具有勒贝格积分和满足紧致性，基本链条件和弱否定的解析结构的逻辑系统中的极大系统。
first-order logicdefinabilityinfinitary logic systemschain logichajek's logic
发现论文，激发创造
  • 线性时态逻辑的 Sahlqvist 风格对应定理

    本文探讨了线性时态逻辑（LTL）中，一类包括模态算子 F，G，X 和 U 的 Sahlqvist 公式具有一阶语言可定义的框架条件的对应关系。

    Jun, 2022

  • 强度因素：一个量化模态逻辑的不确定性系统

    提出了一种新的基于概率论和证明论的处理量化模态逻辑 (一阶模态逻辑) 不确定性的系统，通过解决归纳处置的问题，使 Chisholm 的理论得到具体实现，可用于交互式系统，用于解释其不确定性提供合理解释。

    May, 2017

  • 有限及可枚举模型中概率逻辑的有效性和可满足性的可计算性

    本文研究的是 epsilonE-logic 中关于有限模型的可满足性和有效性问题，特别是对于有理的 epsilon，结果为 Sigma^0_1 和 Pi^0_1 完备性，而对于 epsilon=0，结果为可判定，但对于可数模型的 εE 逻辑的可计算性仍然存在研究点；此外，还讨论了在计算学习理论，加权图和神经网络中的应用。

    Oct, 2014

  • 一个有限置信一阶逻辑推理系统

    本文提出了一种高度可表达的有限置信逻辑，可以进行可计算的推理，在一阶逻辑上保持可判定性，在命题逻辑上保持可操作性，并引入一种采用此逻辑作为表示语言的推理系统，该系统展示了有限置信的好处。

    May, 2017

  • 比较和评估扩展 Lambek 演算

    该论文通过建立 Lambek calculus 的扩展和变体的两个统一框架，利用证明网和图重写规则建立逻辑框架，用于在不同的语言分析框架之间架起桥梁，强调区别，帮助识别问题。

    Jun, 2015

  • 计算描述逻辑本体的 Horn 重写

    将一个使用 DL L1 表达的本体 O1 重写为 Horn DL L2 中的本体 O2，以保证在任意数据集扩展时 O1 和 O2 是等价的。对存在 Horn 重写的本体进行研究，并识别出一类本体可以用多项式大小的 Horn 重写表示。

    Apr, 2015

  • 描述逻辑进入二阶：使用全量量化概念扩展 EL

    该论文涉及描述逻辑的特性，首次引入普遍量化的概念，提出两种扩展的语义模型，包括模态逻辑中的公理原型和二阶逻辑中的量词的替代。研究表明，在某些扩展的语义中，所得出的结论与经典的描述逻辑相符，并证明了某种程度上用于这种扩展的算法的多项式可判定性。

    Aug, 2023

  • 关于策略的推理：关于模型检查问题

    介绍了一种更广泛的策略逻辑，用于在多代理并发游戏中推理策略，证明了其包括 CHP-SL，同时维护可决策模型检查问题。

    Dec, 2011

  • 证明结构研究

    提出并阐述了一种新的证明操纵和分析形式主义，为证明检索方式提高了效率，实现了较短证明的自动化，特别是在首阶问题上的历史证明中进行了一项全面的形式重建分析。

    Feb, 2023

  • 无 Lambda 高阶逻辑叠加

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

    May, 2020