Logic for Computer Scientists/Predicate Logic/Strategies for Resolution/Iterative Deepending

Iterative Deepening

Iterative deepening is a complete search strategy, which combines depth-first with breadth-first search.

$depthbound=1$
do while (not found)
Search by limited depth-first search until $depthbound$ .
Set $depthbound=depthbound+1$

Number of expansions in a tree with branching factor $b$ until depth $d$ is

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

The total number of expansions in iterative deepening search is

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

Hence time complexity of iterative deepening is still $O(b^{d})$ .

As exemplified by PTTP ("Prolog Technology Theorem Prover") Prolog can be viewed as an "almost complete" theorem prover, which has to be extended by only a few ingredients in order to handle the non-Horn case. By this technique the benefits of optimizing Prolog compilers are accessible to theorem proving. First we will briefly review the standard approach, and then we will describe the necessary modifications to obtain restart model elimination. The PTTP-approach transforms a given clause set into a Prolog program. The transformed Prolog program must execute the clauses according to some complete proof procedure. Model elimination turns out to be particularly useful for this, since it is, like Prolog, an input proof procedure. In particular, the transformation from the input clauses to Prolog works as follows:

An input clause such as
$C\gets A\land B$ is transformed into a Prolog clause
```
 (1) c :- a, b.
```
Additionally, since in the model elimination calculus every literal in a clause can equally well serve as an entry point into the clause, all contrapositives are needed. In this case these are

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

This example also shows how negation is treated, namely by making it part of the predicate name.

Prolog's unsound unification has to be replaced by a sound unification algorithm. This can either be done by directly building-in sound unification into the Prolog implementation, or by reprogramming sound unification in Prolog and calling this code instead of Prolog's unsound unification.
A complete search strategy is needed. Usually depth bounded iterative deepening is used. The strategy can be compiled into the Prolog program by additional parameters, being used as "current depth" and "limit depth". The cost of an extension step can be uniformly 1 (depth bounded search), or can be proportional to the length of the input clause (inference bounded search).
The model elimination reduction operation has to be implemented. This can be realized by memorizing the subgoals solved so far (the A-literals) as a list in an additional argument, and by Prolog code that checks a goal for a complementary member of that list. Of course, this check has to be carried out with sound unification. The Prolog clause (1) from above then looks like
```
 (1') c(Anc) :- a([-a|Anc]), b([-b|Anc]).
```
where Anc is a Prolog list which contains the ancestor literals (called A-literals in ()); code for reduction steps then looks like

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