logic - 什么是学术界以外的自然扣除？

Question

我正在大学/学院学习自然演绎，作为我正式规范和验证计算机科学类(class)的一部分。

我觉得这很有趣，但是当我找到实际用途时，我会学得更好。

谁能向我解释除了用于正式验证代码位之外是否以及如何使用自然演绎？

谢谢!

Answer 1

自然演绎在实际形式方法中的使用并不多:顺序演算通常是更好的基础，因为它更接近用于构建逻辑决策程序的表格方法。 Tableau 方法对于计算机科学中逻辑的实际应用非常重要。

自然演绎最常用于构造类型理论，这使其在编程语言设计中具有一定的影响力。不过，它被认为是一个好消息，而不是必须知道。

自然演绎的主要值(value)在于它是学习形式推理的最佳方式，但这是学术界最常见的教学应用。