Breadth-first Resolution Algorithm

Question

I want to implement a resolution algorithm which tries to get empty set as it resolves the candidate clauses.

I want algorithm to resolve the candidate parent clauses in a breadth-first order. However, I got confused at a point:

Let S be conjunction of all the clauses in knowledge base and negation of goal clause

when we try to resolve candidate clauses in S with the ones again in S, we get S'

As second step in the algorithm, should we try to resolve for S and S' or S' with S' itself? and how should it proceed?

For example;

Suppose knowledge base + neg. of goal set consists of set of clauses such as

p(a,b) ^ q(z),~p(z,b) ^ ~q(y) ((let's call this set S)

when we run resolution algorithm on set S, we get clauses like:

q(a) ^ ~p(z,b) (let's call this set S')

now, If we have to employ BFS strategy, should we first find the resolvents whose first parent is in S and second is in S' first? or try to check for the resolvents whose parents are both from S'?

In some examples, when you first check with S' and S' for resolvents, you get the solution. However, when you proceed with checking pair of sets (S, S') (S, (S, S')) you get another way leading to empty clause. So, which order does correspond to BFS?

Thanks in advance

Answer 1

Here it is stated that:

All of the first-level resolvents are computed first, then the second-level resolvents, and so on. A first-level resolvent is one between two clauses in the base set; an i-th level resolvent is one whose deepest parent is an (i-1)-th level resolvent.

and here:

• Level 0 clauses are the original axioms and the negation of the goal
• Level k clauses are the resolvents computed from two clauses, one of which must be from level k-1 and the other from any earlier level.

What I mean from these statements and my comments are as the following:

• Level 0 consists original clauses and negation of the goal. Let this set be X.
• Level 1 consists resolution of (X,X) which are the only possible candidates. Let this set be Y.
• Level 2 consists resolutions of (Y,X) and (Y,Y).

and so on.

My explanation applies the second statement. Actually it will give the same results as the first one except that you will resolve same sets at every level which is unnecessary. Breadth-first strategy is already very inefficient and a wrong approach makes it even worse.

I hope this clarifies your question.