计算机科学家逻辑/谓词逻辑/消解策略/迭代加深

迭代加深

迭代加深是一种完备的搜索策略，它结合了深度优先搜索和广度优先搜索。

$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).