Jul, 2012

PIDE 框架下的 Isabelle/jEdit 证明器集成开发环境

PDF
TL;DRPIDE 框架基于 ML 和 Scala 结合的双语言架构，实现与 LCF 风格的证明器（如 Isabelle，Coq 或 HOL）的连接，并与 JVM 平台上的先进前端技术相结合以弥补命令行交互不足。其中 Isabelle/jEdit 作为 Isabelle2011-1 的一部分，采用了连续证明检查的交互模型，实现了正式内容的增强文本编辑。该框架可以作为当前 Isabelle 的可用接口，并可以启示基于 PIDE 的进一步项目的参考应用。
发现论文，激发创造
  • Isabelle 密码机

    该研究结合学习与定理证明的多种方式显著提高了 E 自动定理证明器在 Isabelle Sledgehammer 问题上的性能，特别是在 ENIGMA 指导，神经前提选择和 E 的有针对性策略的开发方法上。最终的 ENIGMA 和前提选择系统在 15 秒内比 E 的最佳先前版本提高了 25.3％，也优于所有其他先前的 ATP 和 SMT 系统。该方法可在从 Isabelle 提取的数十万个一阶未分类和已分类问题的几次迭代训练中进行训练。

    May, 2022

  • 面向 IDP 的 Web-based IDE

    使用基于 Web 技术的 IDE，方便用户在线使用 IDP 知识库系统，该系统基于一阶逻辑，可用于开发大型应用。

    Nov, 2015

  • 使用 Isabelle 证明助手进行考试

    本文介绍一种使用 Isabelle 证明助手对自动推理课程学习成果进行测试的方法，该方法允许测试不同逻辑证明系统中形式证明的一般理解和特别是在 Isabelle/HOL 高阶逻辑中证明的理解，最终讨论了使用该方法考试并进行评分的经验和未来潜在的工作。

    Mar, 2023

  • 自然演绎作为高阶归结

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

    Oct, 2000

  • OWL 本体真正可解释性的前夕：采用 Evee 和 Evonne 的描述逻辑证明（扩展版）

    本文介绍了一个计算 DLs 证明的 Java 库及其在 Protégé 中的插件，并提供了一款显示计算结果的高级应用。

    Jun, 2022

  • Budge：一种编程语言和定理证明器

    基于哥德尔编号和质因数分解的简单编程语言，配合具有显式作用域的循环和定理证明器，可以表示和工作于形式系统。编程语言和定理证明器之间可以相互表示，并提供实例程序和它们的求值。

    May, 2022

  • 使用 IDPD3 可视化交互推断

    介绍了 IDPD3 库，作为一种 visualisations 工具， 用于知识库系统中逻辑理论和交互式模拟的可视化和解释。

    Nov, 2015

  • 利用 Isabelle 教授高阶逻辑

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

    Apr, 2024

  • 原有表征定理的 Isabelle 形式化

    本篇论文基于 Isabelle-verified 事件结构枚举算法，通过对巨大数据库进行跨站数据挖掘，发现了连接看似不相关的数学对象（并发理论中的事件结构和计算生物学中的完整图）的新定理，并通过 Isabelle/HOL 定义和定理进行了形式验证，完成了 Isabelle-verified 事件结构枚举算法验证的全面验证框架以链接事件结构和完整图。

    Jun, 2023

  • 神经符号专家系统中可解释推理规则的动态生成

    提出一种系统性推理方法，它可以生成基于事实库的人类可解释证明树。新方法使用神经语言建模、引导生成和半参数密集检索来替换手工制定的规则，从而动态实例化可解释推理规则，并在多个事实上得分。经验证的知识证明完全落实在科学 QA 数据集上。

    Sep, 2022