0

我的任务是证明：

val problem1Thm =
    [] |- p ==> (p ==> q) ==> (q ==> r) ==> r
        : thm

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

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

我试图在 HOL 中这样做：

val problem1Thm =
let
  val th1 = ASSUME ``p :bool``;
  val th2 = MP ... STUCK [Want p ==> q and p, therefore q is true.
  val th3 = IMP_TRANS ... STUCK [Since th1 and th2, th3 will be true]
in
  body
end;

上面我被第二行难住了，为了在我的单独解释器中进行测试，自从试图将一些东西传递给 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；

4

0 回答 0