问题标签 [hol]

问问题

For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.

34 问题
Newest
Active
Bountied
318
Unanswered
0 投票
3 回答
163 浏览

coq - 证明助手中的认证计算

手动或通过计算机代数系统执行的符号计算可能是错误的，或者仅在某些假设下才成立。一个经典的例子是sqrt(x^2) == x一般不正确，但如果x是真实的且非负的，它确实成立。

是否有使用 Coq、Isabelle、HOL、Metamath 或其他证明助手/检查器来证明符号计算正确性的示例？特别是，我对微积分和线性代数示例感兴趣，例如求解定积分或不定积分、微分方程和矩阵方程。

更新： 更具体地说，有兴趣知道是否存在可以正式解决（可能在证明助手的帮助下）的微积分和线性代数本科作业的示例，以便解决方案可以通过自动验证证明检查器。一个非常简单的精益作业示例在这里。

0 投票
1 回答
25 浏览

emacs - 为 HOL4 设置 Emacs

我是 HOL4 和 Emacs 的新手。为这个可能很愚蠢的问题道歉。

我希望按照https://hol-theorem-prover.org/HOL-interaction.pdf的说明为 HOL4 设置 Emacs 。我试图在 Emacs 上启动 HOL 进程Alt-h h并按下Enter，但 Emacs 返回Symbol’s function definition is void: if-let*。我.emacs.d/init.el的定义如下。我应该怎么做才能修复错误？谢谢。

0 投票
0 回答
20 浏览

sml - HOL 定理证明器：通过蕴涵证明

我的任务是证明：

如果我们假设 p 并将对 r 的含义串在一起，这很容易证明。

  1. 假设 p。
  2. 暗示 p ==> q 为真，因此 q 为真。
  3. 暗示因为 q 为 True，q ==> r 为 True，因此 r 为 True。
  4. 完毕。

我试图在 HOL 中这样做：

上面我被第二行难住了，为了在我的单独解释器中进行测试，自从试图将一些东西传递给 MP 和 IMP_TRANS 可以接受的 HOL 以来，我一直被困住。

这是我所知道的：

  1. MP 需要两个参数，t1 ==> t2 和 t1 来接收 t2。
  2. IMP_TRANS 需要两个参数，t1 ==> t2 和 t2 ==> t3，我需要 t1 和 t2。
  3. 输出必须是需要证明的形式，IMP_TRANS 可能不是所需要的。

我在解释器中尝试了以下内容，以查看适用于 MP/IMP_TRANS 的内容：

  1. IMP_TRANS p ==> q q ==> r;
  2. MP p ==> qth1;

我都收到与错误地将参数传递给任一函数的参数的错误类似的错误。任何帮助将不胜感激，因为我正在使用的资源非常缺乏。

我也一直在看 DISCH，书中给出的示例非常缺乏信息，但这似乎提供了一种暗示，并且是我需要的。观察它在解释器中的作用有助于看到我可以写 DISCH p:boolth1; 输出在哪里p ==> p；

0 投票
0 回答
11 浏览

sml - 用于基于目标的证明的 HOL 中的 PAT_ASSUM 通用量词

我正在尝试将“s”应用于我的通用量词，以将假设列表操作为 P(s) ==> M(s), P(s) 的形式，然后证明 M(s)。

到目前为止，这是我所拥有的：

目标堆栈：

扩展 PAT_ASSUM 时，我收到此错误提示 Alpha 'a.

我知道要解决剩下的问题，另一个 PAT_ASSUM 将用于A ==> B该模式，我运行 IMP_ELIM，这部分是简单的部分。我只是在努力通过显示 s 是 'a.


12345678910