时间戳

首页 > 解决方案 > 使用 SML 和 HOL 推理规则从第一原理证明定理

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

问题描述

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

我究竟做错了什么？

标签： smltheorem-provinghol

解决方案

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

您需要的第一个定理类似于p /\ q ==> p. 我通过浏览描述找到了适当的规则（第 2.3.24 节）。它被称为CONJUNCT1。

使用它，我们可以得到p一个定理thm1：

val thmp = CONJUNCT1 thm1;

相同的想法可以q作为定理从thm1：

val thmq = CONJUNCT2 thm1;

然后您可以将您的想法应用于thm5：

val thm5 = CONJ thmq thmp;

这里重要的是我们不使用p派生自p（thm2）和q派生自q（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;

推荐阅读