命題定理證明

Question

我們如何使用廣度優先搜索作爲命題定理證明的一種策略（我看不出一個清晰的問題表達式：在每個狀態和狀態下可用的動作是什麼）。

我一直在尋找解釋在網上無處不在;所有文件都提到BFS，但沒有一個提供算法。

感謝您的幫助

Answer 1

狀態是一個派生列表。從狀態到狀態的轉換應用推理規則，其中每個前提在結論列表中顯示爲結論，並用新推導擴展列表。

有了這些狀態和轉換，你可以做一個平常的BFS，直到你找到你正在尋找的結論。