什麼是學術界以外的自然演繹？

Question

我正在學習自然扣除作爲我的形式規範的一部分&在大學/學院驗證計算機科學課程。

我覺得很有趣，但是當我能找到實用的東西時，我學得好多了。

任何人都可以向我解釋是否以及如何使用自然演繹除了正式驗證代碼位？

謝謝！

Answer 1

自然演繹在實際的形式化方法中並沒有太多用處：後繼演算通常是更好的基礎，因爲它更接近構建邏輯決策過程時使用的表格方法。 Tableau方法對於計算機科學中邏輯的實際應用非常重要。

自然演繹最常用於建構型理論，這使得它在編程語言設計中有一定的影響力。但它被認爲是一個很好的知識，而不是必須知道的。

自然演繹的主要價值在於它是學習形式推理最好的方法，但這是一個主要在學術界看到的教學應用。

Answer 2

自然扣除是非常有趣和酷的一種，但它是學術界以外很少使用。對程序進行修正的正式證據使用自然演繹是乏味的，因此經常使用更高層次的工具。

Answer 3

我應該過馬路嗎？

• 有一輛大巴士即將通過。
• 有熔岩在路上流淌。
• 還有一個十米遠的十字路口。

扣除：不應該過馬路。