用A *算法定理證明

Question

我正在爲我的碩士學位準備期末考試，這是一個過去考試的問題，它真的讓我困惑，不知道從哪裏開始。

我的想法是可接受的啓發式算法是解析規則，然後證明解析規則是可接受的，對嗎？如果是這樣，爲了證明解決規則是可以接受的，我應該從哪裏開始？感謝幫助球員。

考慮一個定理證明器應用程序。 A *算法可用於搜索最簡單的 （最短）證明。假設已知公理和定理在命題邏輯中被表示爲Horn子句的知識庫，並且證明者使用後向鏈。 （a）提出可接受的啓發式。

（二）證明建議的啓發是受理

Answer 1

肯定，表示定理證明意味着它是一種分辨率。
Horn子句是明確的子句或完整性約束。也就是說，Horn子句具有假或正常原子作爲頭。
完整性約束是表格的一個子句
false←a1∧...∧ak。
完整性約束允許系統證明在知識庫的所有模型中原子的某些連接是錯誤的 - 也就是說證明原子的否定分離
Horn子句知識庫可能意味着原子的否定
例如：考慮知識庫KB1：

false←a∧b. 
a←c. 
b←c. 

原子c在KB1的所有模型中都是錯誤的。如果c在KB1的模型I中是正確的，那麼a和b在I中都是正確的（否則我不會是KB1的模型）。因爲我的虛假是虛假的，我和甲和乙是真實的，我的第一個條款是錯誤的，這與我作爲KB1的模型是矛盾的。因此，c在KB1的所有模型中都是錯誤的。這表示爲 KB1¬c 這意味着在KB1的所有模型中¬c都是真的，因此在KB1的所有模型中c都是錯誤的。