Isabelle/Pure Isabelle/HOL Isabelle/Isar 概念性问题

Question

我需要在一篇论文中做一个演示，该论文在某些时候使用了 Isabelle/Isar 和 Isabelle/HOL。

我尝试在线研究 Isabelle/HOL 和 Isabelle/Isar，以便能够在一张或两张幻灯片中阐明它们之间的关系。以下是我目前理解的关系:

• Isabelle - 为演绎系统提供通用基础设施
  • 基于标准机器学习编程语言
  • 提供了一个 IDE，允许您编写稍后可以证明的理论。
• Isabelle/Pure - 根据 this 的高阶逻辑的最小版本关联:
  • 它是可以输入到 isabelle IDE 中的实际语言吗？
  • 还是技术规范？

• Isabelle/HOL(高阶逻辑):

  • 它是图书馆还是语言？
  • 它与 Isabelle/Pure 有什么关系？
  • 本质上是程序性的吗？
    • 战术只存在于 Isabelle/HOL 中吗？
    • 是 LCF - 逻辑可交换函数吗？

• 伊莎贝尔/伊萨尔:

  • 基于 Isabelle/Pure 的结构化证明语言
  • 陈述式
  • 它是否是 Isabelle/HOL 的扩展，如 here 所述？
  • 语言环境是否仅存在于 Isabelle/Isar 中？

Isabelle/IDE 默认支持什么？

只是觉得我从不同来源获得了相互矛盾的信息，并且想解决这个问题。

提前致谢

Answer 1

编辑 - 在此处查看这个高度相关的问题和 Manuel Eberls 的回答:What are all the isabelle/slashes?

---

由于这是对家庭作业问题的回答，而我本人对 Isabelle 项目的所有部分了解有限，因此此回答只是试图为您指明您在的正确方向您问题的某些部分。

来自Isabelle/ISAR reference manual :

The Isabelle system essentially provides a generic infrastructure for building deductive systems (programmed in Standard ML), with a special focus on interactive theorem proving in higher-order logics.

它还继续引入 ISAR:

In contrast Isar provides an interpreted language environment of its own,which has been specifically tailored for the needs of theory and proof development.[...]The main concern of Isar is the design of a human-readable structured prooflanguage

让我们通过查看来自 Makarius Wenzel 的出版物，尝试将 Pure 与所有这些联系起来关于主题:

Thus Isar proof texts may be understood as structured compositions of formal entities of the Pure framework, namely propositions, facts, and goals

通俗地说，Pure 是语义基础。 Isar 是一种“遵循”这种语义并为其提供语法的语言。 Isabelle 只是它运行的(其中一个)平台。

您对 Pure 和 Isar 之间的区别的一些困惑似乎源于以下事实:Isabelle Pure source code一次定义，或者至少似乎定义了语义 (Pure) 和语法 (Isar):

(* The Pure theory, with definitions of Isar commands and some lemmas. *)

依我拙见，这可能与你对两者的语法、语义和“实现”的理解有关。计算机或纸张之外的“纯”只是语义，因此，就像数学一样，只是我们大脑中的东西。给它语法，你可以把它写在纸上或输入机器。为了让机器能够处理您的文本(因为这最终是我们所追求的)，它需要一个实现。一些框架告诉它如何阅读语法以及如何处理它。这个框架是伊莎贝尔。在 Isabelle 之上，还有 Isabelle/Pure，它定义语义(处理)和 Isabelle/Isar，它定义语法。出于实际原因，Isabelle 的 Pure 实现已经一次性提供了 Isar 语法。

从所有这些，您也许可以自己弄清楚 HOL!

更多引用资料:

• The Isabelle/Isar Implementation