我正在学习自然演绎作为我在大学/学院的正式规范和验证计算机科学课程的一部分.
我发现它很有趣,但是当我找到适合实际用途的东西时,我学得更好.
任何人都可以向我解释是否以及如何使用自然演绎除了正式验证代码位之外？
谢谢!
自然演绎在实际的形式方法中并没有那么多使用：顺序微积分通常是更好的基础，因为它更接近于构建逻辑决策过程中使用的表格方法。Tableau 方法对于计算机科学中逻辑的实际应用非常重要。
自然演绎最常用于构造类型理论，这使其在编程语言设计中具有一定的优势。不过，它被认为是“值得了解的事情”，而不是“必须知道的事情”。
自然演绎的主要价值在于它是学习形式推理的最好方法，但这是一种主要出现在学术界的教学应用。