个人中心
文章发布
退出
作者热门文章
- html - 出于某种原因，IE8 对我的 Sass 文件中继承的 html5 CSS 不友好？
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景？
26
4
我正在阅读 "Concrete semantics with Isabelle/HOL"我对高阶逻辑非常感兴趣。我知道普通的一阶逻辑和一些模态逻辑，但我以前几乎没有接触过高阶逻辑及其元理论，所以我想填补空白。我读到 HOL 本质上是 Church 的简单类型理论，而 Pure 是前者的直觉变体。问题在于“本质上”这个词:Isabelle/HOL 和 Isabelle/Pure 理论与例如 Andrews' textbook 有何不同？ ?是否有教科书介绍 Isabelle/HOL 和 Isabelle/Pure 中使用的那种高阶逻辑，并讨论了它们的元理论特性？
最佳答案
关于 HOL 及其许多变体和方言，可以说很多。它是 Isabelle 邮件列表中的一个经常出现的主题。和另一个 HOL系统。例如，这是 2013 年 1 月/2 月在 isabelle-users 上的相关主题。 :Where to learn about HOL vs FOL?还有一些对相关文献的引用。
在 Isabelle/Isar Implementation 中还有一点关于 Isabelle/Pure(这是最小的 HOL)的逻辑。手册，第 节2 原始逻辑 .
关于logic - 是否有高阶逻辑的引用定义，如 HOL、Isabelle 等？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/27908036/
26
4
0
我在 Isabelle/HOL 中有一些定义和定理，需要在 HOL 中使用这些相同的定义和定理。手动翻译代码当然是可能的，但很麻烦。有没有(半)自动执行这种翻译的程序？ 如果由于某种原因这是不可能的，
我将从 Isabelle/HOL 开始，并完成发行版中包含的 prog-prove.pdf 教程。我被第 4.4.5 节“规则反转”难住了。本教程(本质上)给出了以下示例: theory Struct
我看过很多关于 Isabelle 的语法和证明策略的文档。然而，我对它的基础知之甚少。我有几个问题，如果有人能花时间回答，我将不胜感激: 为什么 Isabelle/HOL 不承认不终止的函数？许多其他
我注意到，在使用 Isabelle/HOL Isar 时，有几种方法可以处理通用量化。我正在尝试以适合本科生理解和重现的风格编写一些证明(这就是我使用 Isar 的原因!)，我对如何以一种好的方式表达
我看到了构造 THE x. A在 Isabelle/HOL 标准库的源代码中。这个构造表示什么？好像和SOME x. A差不多. 最佳答案 THE是一个描述运算符，如 SOME ，但具有较弱的公理化。
我试图在 Isabelle/HOL 中证明这个引理。 引理“(0::nat) ≠ undefined” 但是挑剔的人找到了这个和它的否定的反例 引理“(0::nat) = undefined” 这怎么
根据我对 Isabelle 文件的扫描，Sledgehammer 工具仅适用于 Isabelle/HOL。我很好奇伊莎贝尔其他理论的自动化。例如: 伊莎贝尔/采埃孚 伊莎贝尔/FOL 他们是否支持:
关闭。这个问题不符合Stack Overflow guidelines .它目前不接受答案。 我们不允许提问寻求书籍、工具、软件库等的推荐。您可以编辑问题，以便用事实和引用来回答。 关闭 6 年前。
关闭。这个问题不符合Stack Overflow guidelines .它目前不接受答案。 我们不允许提问寻求书籍、工具、软件库等的推荐。您可以编辑问题，以便用事实和引用来回答。 关闭 6 年前。
我试图证明一个引理在某个部分有一个错误的假设。在 Coq 中，我曾经写过“一致”，它会摆脱目标。但是，我不确定如何在 Isabelle Isar 中进行。我试图证明关于我的 le 的引理功能: pri
考虑以下简单过程语言的 Isabelle/HOL 定义: typedecl channel datatype process = Put channel char process | Get "cha
HTTP2 如何解决线头阻塞 (HOL) 问题？ 这个问题在http1.1中很常见，不过听说HTTP2已经修复了这个问题。有人可以解释 HTTP2 究竟是如何解决这个问题的吗？ 最佳答案 HTTP 线
我有这个 C 代码: while(p->next) p = p->next; 我想证明不管list有多长，当这个循环结束时，p->next等于NULL，EIP指的是下一条指令在这个循环之后。 但是
问题 Isabelle/HOL验证器的核心算法是什么？ 我正在寻找计划元循环评估器级别的东西。 澄清 我只对 Verifier 感兴趣，而不是自动定理证明的策略。 语境 我想从头开始实现一个简单的证明
关闭。这个问题不满足Stack Overflow guidelines .它目前不接受答案。 想改善这个问题吗？更新问题，使其成为 on-topic对于堆栈溢出。 7年前关闭。 Improve thi
我正在阅读 "Concrete semantics with Isabelle/HOL"我对高阶逻辑非常感兴趣。我知道普通的一阶逻辑和一些模态逻辑，但我以前几乎没有接触过高阶逻辑及其元理论，所以我想填
我很难理解为什么下面的每个示例都有效或无效，更抽象地说，归纳法与战术 vs Isar 是如何相互作用的。我正在使用最新的 Isabelle/HOL (2016-1) 在 Windows 10 上使用
我需要在一篇论文中做一个演示，该论文在某些时候使用了 Isabelle/Isar 和 Isabelle/HOL。 我尝试在线研究 Isabelle/HOL 和 Isabelle/Isar，以便能够在一
在 Isabelle/HOL 中，我可以用 (SOME _. True) 表示任何类型的任意(但固定)值。有没有更简洁的表示法？ 最佳答案 未定义 (我希望我可以只写上面的内容，但答案必须超过 9 个
我正在阅读 Isabelle 教程，并试图阐明我使用 primrec 和 fun 的概念。到目前为止我搜索过的内容，包括答案 here ;我知道 primrec 中的构造函数只能有一个方程，而 pri
我是一名优秀的程序员,十分优秀！