在我们的软件验证模块中，我们刚刚从真值表转到自然推导。真值表看起来很基本，但现在我们使用 coq 定理证明器来证明更复杂的陈述。让我感到困惑的是，我们最终会得到"经过验证或未证明"类型的答案，而使用真值表，我们可以根据输入得出真或假类型结果，这是否意味着我们使用自然演绎来寻找重言式，还是我完全错过了什么？
它们有不同的含义。真值表对应于命题的语义。你确定命题什么时候为真或假，这取决于自由变量（任何不在"forall"或"exist"中的变量，或你所说的"输入"）何时为真或假。
自然推导是不同的，因为您不会直接为任何输入分配真/假值。通过自然演绎，你从命题开始，然后从那些使用演绎或"自然推理"的命题中构建新的命题。基本上，有一堆规则告诉你如何构建这些命题，称为"推理规则"。
让我们举个例子：我们想证明|= 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。为此，让我们看一下"包含"的（简化）推理规则：
A |- B
--------
|- A -> B
这个推理规则告诉你："如果你能证明B假设你有A，那么你就可以证明A需要B，或者A->B"这是允许你"构建"命题的规则，从某种意义上说，你首先构建较小命题的证明，然后将它们连接在一起以构建较大命题的证明。
我们还有另一个可以使用的推理规则：
A |- A
这是什么意思？这意味着如果你假设某事发生了，你总是可以证明它。有道理吧？
所以我们可以用这些新规则来证明|- A->A .如何？容易：
A |- A
------
|- A -> A
我们使用了"蕴涵"的推理规则，用A代替了B。然后我们必须证明A |- A，但这是我们知道的另一个推理规则！有了这个，我们已经证明了|- A->A是正确的。但是，我们根本不需要使用任何真值表。
您可能会注意到其中一个是如何|= A->A而另一个是如何|- A->A的。这是因为|=的意思是"在语义上需要"，而|-的意思是"证明"。但是，两者都是等效的。如果其中一个是真的，那么另一个也是真的，所以通过证明|- A->A成立，你证明|= A->A是真的，即A->A是重言式。
这是否意味着我们使用自然演绎来寻找重言式，还是我完全错过了什么？
除了重言式之外，您还可以证明更多的事情。重言式是无论如何总是正确的命题。这意味着无论你假设什么，无论你赋予任何"输入"什么价值，它都是真的。这由表示法表示 |= X 表示 X 是重言式。但是，您可以在其左侧包含命题。当你这样做时，这意味着右边的命题是真的，只有当你解释左边的命题是真的。例如A |= A .这意味着在任何解释中，您将值true分配给A（左），则A（右）也将具有值true。你可以在左边包括任何命题或命题列表，例如A,B |= A / B，这意味着只要你解释该A，B具有true的值，A / B也是如此。回到自然演绎，你也可以做同样的事情（记住把|=改成|-），例如：A,B |- A / B您可以使用推理规则来证明这是真的。
但是现在我们使用CoQ定理证明器来证明更复杂的陈述。
你在这里必须小心。Coq不使用自然演绎，而是使用一种叫做直觉逻辑的东西。这可能超出了这个问题的范围，但如果你想了解更多信息，这里是维基百科页面：
http://en.wikipedia.org/wiki/Intuitionistic_logic
您可以使用自然演绎在真值表中尽可能表达的所有内容，这只是一种不同的格式。假设我们有一些命题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
或类似。 从某种意义上说，这是一种重言式，因为它总是正确的，但它能够表达真值表所能表达的一切。