使用 SML 和 HOL 推理规则从第一原理证明定理答案

【问题标题】：Theorem proving from first principles using SML with HOL inference rules使用 SML 和 HOL 推理规则从第一原理证明定理
【发布时间】：2018-10-11 18:52:00
【问题描述】：

我正在尝试使用带有 HOL 推理规则的 SML 来证明定理 [] |- p /\ q <=> q /\ p :thm。这是 SML 代码：

val thm1 = ASSUME ``p:bool /\ q:bool``;
val thm2 = ASSUME ``p:bool``;
val thm3 = ASSUME ``q:bool``;
val thm4 = CONJ thm2 thm3;
val thm5 = CONJ thm3 thm2;
val thm6 = DISCH ``(q:bool/\p:bool)`` thm4;
val thm7 = DISCH ``(p:bool/\q:bool)`` thm5;
val thm8 = IMP_ANTISYM_RULE thm6 thm7;

以上代码产生的结果：

val thm8 =  [(p :bool), (q :bool)] |- (q :bool) /\ (p :bool) <=> p /\ q: thm

我做错了什么？

【问题讨论】：

标签： sml theorem-proving hol

【解决方案1】：

你的最终定理的问题是你仍然有p和q作为假设，通过thm2和thm3引入，而你可以并且应该从thm1获得它们。

您需要的第一个定理类似于p /\ q ==> p。我通过浏览description（第 2.3.24 节）找到了合适的规则。它叫CONJUNCT1。

使用它，我们可以从thm1得到p作为定理：

val thmp = CONJUNCT1 thm1;

同样的想法可以从thm1得到q作为定理：

val thmq = CONJUNCT2 thm1;

然后你可以将你的想法应用到thm5：

val thm5 = CONJ thmq thmp;

这里的重要的事情是我们不使用派生自p的p（thm2）和派生自@的q 987654341@ (thm3) 而是 p 派生自 p /\ q 和 q 派生自 p /\ q（设置 show_assumes := true; 可能有助于更清楚地看到这一点）。

最后，我们将您的想法应用到thm7：

val thm7 = DISCH ``p /\ q`` thm5;

获得预期结果的前半部分，但没有多余的假设。

后半部分也是用类似的方法得到的：

val thm9 = ASSUME (``q /\ p``);
val thmp2 = CONJUNCT2 thm9;
val thmq2 = CONJUNCT1 thm9;
val thm6 =  DISCH ``q /\ p`` (CONJ thmp2 thmq2);

然后你对thm8 的想法就完美了：

val thm8 = IMP_ANTISYM_RULE thm7 thm6;

【讨论】：