May, 2020

无 Lambda 高阶逻辑叠加

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

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

    Feb, 2024

  • 自然演绎作为高阶归结

    开发了交互式定理证明器 Isabelle，以 Horn clause 表示每个推理规则，使用基于类型的 λ 演算表示逻辑语法，支持多个逻辑系统并具有逻辑编程潜能。

    Oct, 2000

  • 比较和评估扩展 Lambek 演算

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

    Jun, 2015

  • 通用概率编程的 Lambda 演算基础

    本文通过在 terms 上创建一个 measure space，定义级别逐步逼近的连续 lambda-Calculus 的典型操作语义，并定义采样基异质的语义来实现 MCMC 的 Tracing，并证明了分布语义与集成所有 Traces 的分布具有等价性，这是第一个针对高阶函数语言 Trace MCMC 的验证正确性的证明。

    Dec, 2015

  • 利用 Isabelle 教授高阶逻辑

    我们在 Isabelle 证明助手中对高阶逻辑进行了形式化处理，直接构建在 Isabelle/Pure 的基础框架上，旨在尽可能简洁易读，为对高阶逻辑和证明助手感兴趣但不想学习更复杂的 Isabelle/HOL 与较重自动化的人提供了良好的入门。通过展示我们的开发和方法，我们解释了一个样例证明，描述了高阶逻辑的公理和规则，并讨论了在课堂环境中教授这一主题的经验。

    Apr, 2024

  • 高阶贝叶斯推断的指称验证

    我们提出一个模块化的语义计算方法，用于概率编程语言中的贝叶斯推断算法，并使用高阶函数和归纳类型等方式操纵概率程序的中间表示，定义了语义结构类及其转换的词义准则，并使用 Kock's 综合测度理论证明了一个准 Borel 同源定理。

    Nov, 2017

  • 抽象辩证框架的编码转换为高阶逻辑

    提出了一种将抽象辩证框架及其语义编码为经典高阶逻辑的方法，通过证明助手 Isabelle/HOL 来正式编码并证明重要性质和语义关系。这种方法允许在统一逻辑环境中使用自动化和交互式推理工具对抽象辩证框架进行计算机辅助分析。示例应用包括形式分析和验证元理论性质以及在特定语义约束下生成解释和扩展。

    Dec, 2023

  • 高阶逻辑和定理证明的图表示

    本文首次使用图神经网络 (GNNs) 实现高阶证明搜索，并证明 GNNs 能够提高此领域的最新成果。我们考虑了高阶逻辑的几种图形表示，并将它们与 HOList 基准进行了评估。

    May, 2019

  • 依赖类型高阶逻辑中的定理证明 —— 扩展预印本

    介绍了 DHOL 的依赖类型扩展是如何保留了 HOL 的风格和概念框架，并且使用 DHOL 定理证明器实现了从 DHOL 到 HOL 的翻译，进而获得 DHOL 的定理证明器。

    May, 2023

  • 扩展 Lambek 演算与一阶线性逻辑

    该研究介绍一阶乘性直觉线性逻辑（MILL1），展示 Lambek calculus、multiple context-free languages 以及 Displacement calculus (Morrill 等人) 三种不同的 MILL1 片段。

    May, 2013