在我们的软件验证模块中，我们刚刚从真值表转向自然演绎。真值表看起来很基础，但现在我们使用 coq 定理证明器来证明更复杂的陈述。让我感到困惑的是，我们如何最终得到一种“已证明或未证明”类型的答案，当使用真值表时，我们可以根据输入得到真或假类型的结果，这是否意味着我们使用自然演绎来查看对于重言式，还是我完全错过了什么？
问问题
984 次
2 回答
4
它们有不同的含义。真值表对应于命题的语义。您确定命题何时为真或为假，这取决于自由变量（不在“forall”或“存在”内的任何变量，或您所说的“输入”）何时为真或不为真。
自然演绎是不同的，因为您不直接为任何输入分配真/假值。通过自然演绎，您从命题开始，并从使用演绎或“自然推理”的命题中构建新的命题。基本上，有一堆规则告诉你如何构建这些命题，称为“推理规则”。
让我们举个例子：我们要证明|= A->A.
真值表
首先让我们看一下真值表|= X->Y
X | Y | X-> Y
-------------
T | T | T
T | F | F
F | T | T
F | F | T
所以现在让我们将它应用到|= A->A
A | A | A-> A
-------------
T | T | T
T | F | F
F | T | T
F | F | T
由于 A 始终具有相同的值，我们可以在其中裁剪 2 行并最终得到：
A | A | A-> A
-------------
T | T | T
F | F | T
这是什么意思？这意味着这|= A->A总是正确的，所以我们已经在语义上证明了它。
自然扣除
在这里，我们要|- A->A使用演绎来证明。为此，让我们看一下“entails”的（简化的）推理规则：
A |- B
--------
|- A -> B
这个推理规则告诉你：“如果你可以证明 B 假设你有 A，那么你就可以证明 A 蕴涵 B，或者 A->B” 这就是允许你“构建”命题的规则，在这个意义上，你首先构建较小命题的证明，然后将它们连接在一起以构建更大命题的证明。
我们还有另一个可以使用的推理规则：
A |- A
这是什么意思？这意味着如果你假设它发生了，你总是可以证明它。有道理吗？
所以我们可以用这些新规则来证明|- A->A。如何？简单的：
A |- A
------
|- A -> A
我们使用了“entails”的推理规则，并将 B 替换为 A。然后我们必须证明A |- A，但这是我们知道的另一个推理规则！有了这个，我们已经证明|- A->A是真的。但是，我们根本不需要使用任何真值表。
您可能会注意到其中一个如何，|= A->A而另一个如何|- A->A。这是因为|=意思是“在语义上包含”，而|-意思是“证明”。但是，两者是等价的。如果其中一个是真的，那么另一个也是，所以通过证明|- A->A成立，你证明|= A->A是真的，即这A->A是一个重言式。
这是否意味着我们使用自然演绎来寻找重言式，或者我完全错过了什么？
除了重言式，你可以证明更多的东西。重言式是无论如何都是正确的命题。这意味着无论您假设什么，无论您为任何“输入”分配什么值，它都是正确的。这由|= X表示 X 是重言式的符号表示。但是，您可以在其左侧包含命题。当你这样做时，它意味着右边的命题是真的，只有当你解释左边的命题是真的时。例如A |= A. 这意味着在您将值分配true给A(left) 的任何解释中，A(right) 也将具有 value true。例如，您可以在左侧包含任何命题或命题列表A,B |= A /\ B，这意味着无论何时您解释A并且B有价值true，所以也有A /\ B。回到自然演绎，你也可以这样做（记得改成|=）|-，例如：A,B |- A /\ B
你可以使用推理规则来证明这是真的。
但现在我们使用 coq 定理证明器来证明更复杂的陈述
你必须在这里小心。Coq 不使用自然演绎，而是使用直觉逻辑。这可能超出了这个问题的范围，但如果您想了解更多信息，请访问维基百科页面：
于 2013-11-30T01:12:25.227 回答
0
您可以使用自然演绎在真值表中制定所有可能的内容，这只是一种不同的格式。假设我们有一些P : Prop -> Prop -> Prop关于真值表的命题，例如
A | B | P
---------
T | F | T
T | T | T
F | T | T
F | F | F
我们可以这样说
Theorem or_equiv : forall A B, A \/ B -> P A B
或类似的。这是一个重言式，因为它总是正确的，但它能够表达真值表所能表达的一切。
于 2013-11-15T00:38:37.887 回答