計算機科學家邏輯/謂詞邏輯/消解策略/迭代加深

迭代加深

迭代加深是一種完備的搜尋策略，它結合了深度優先搜尋和廣度優先搜尋。

$depthbound=1$
do while (not found)
透過有限深度優先搜尋，直到 $depthbound$ .
設定 $depthbound=depthbound+1$

分支因子為 $b$ 的樹中，直到深度為 $d$ 的擴充套件次數為

1+b+b^{2}+\cdots +b^{d-1}+b^{d}

迭代加深搜尋中的總擴充套件次數為

(d+1)*1+d*b+(d-1)*b^{2}+\cdots +3*b^{d-2}+2*b^{d-1}+1*b^{d}

因此，迭代加深的時空複雜度仍然為 $O(b^{d})$ .

正如 PTTP ("Prolog Technology Theorem Prover") 所示，Prolog 可以被視為一種“幾乎完備”的定理證明器，只需要新增幾個成分就可以處理非 Horn 情況。透過這種技術，最佳化 Prolog 編譯器的優勢就可以用於定理證明。首先，我們將簡要回顧標準方法，然後我們將描述必要的修改以獲得重啟模型消除。PTTP 方法將給定的子句集轉換為 Prolog 程式。轉換後的 Prolog 程式必須根據某種完備的證明過程來執行子句。模型消除被證明對此特別有用，因為它像 Prolog 一樣，是一種輸入證明過程。特別是，從輸入子句到 Prolog 的轉換如下所示

例如，輸入子句
$C\gets A\land B$ 被轉換為 Prolog 子句
```
 (1) c :- a, b.
```
此外，由於在模型消除演算中，子句中的每個文字都可以同樣好地用作子句的入口點，因此需要所有逆否命題。在本例中，這些命題是

 (2) not_a :-  not_c, b.
 (3)  not_b :-  a, not_c.

這個例子也說明了如何處理否定，即將其作為謂詞名稱的一部分。

Prolog 不安全的統一演算法必須用安全的統一演算法替換。這可以透過直接將安全統一演算法內建到 Prolog 實現中來實現，也可以透過在 Prolog 中重新程式設計安全統一演算法，並在呼叫 Prolog 不安全的統一演算法時呼叫此程式碼來實現。
需要一種完備的搜尋策略。通常使用深度受限的迭代加深。該策略可以透過額外的引數編譯到 Prolog 程式中，這些引數用作“當前深度”和“限制深度”。擴充套件步驟的成本可以統一為 1（深度受限搜尋），或者可以與輸入子句的長度成比例（推理受限搜尋）。
必須實現模型消除還原操作。這可以透過在額外的引數中將迄今為止解決的子目標（A 文字）作為列表記憶，以及透過檢查子目標是否有該列表中互補成員的 Prolog 程式碼來實現。當然，此檢查必須使用安全統一演算法進行。上面的 Prolog 子句 (1) 如下所示
```
 (1') c(Anc) :- a([-a|Anc]), b([-b|Anc]).
```
其中 Anc 是一個 Prolog 列表，它包含祖先文字（在 () 中稱為 A 文字）；還原步驟的程式碼如下所示

(Red-C)  c(Anc) :- member(c,Anc).
(Red-notC)  not_c(Anc) :- member(-c,Anc).