/* BREADTH.

A Breadth First Search Theorem Prover.
EQUAL contains test example.

Alan Bundy 16.6.81 */


/* Top Goal */

go :- breadth(0).


/* Breadth First Search Strategy */

breadth(N) :-
        N1 is N+1,                      % Calculate new depth
        repeat(resolve(input,N,N1)),    % Form all resolvants at that depth
        repeat(resolve(N,input,N1)),
        breadth(N1).                    % and recurse


/* Repeat as many times as possible */

repeat(Goal) :- Goal, fail.     % Keep trying and failing
repeat(Goal).                   % and succeed only when you run out of things to do


/* Resolution Step */

resolve( N1, N2, N ) :-
        find_clause(Parent1, Consequent1, Antecedent1, N1),     % Find clauses at
        find_clause(Parent2, Consequent2, Antecedent2, N2),     % appropriate depths
        select(Literal, Consequent1, RestConse1),       % find a common literal
        select(Literal, Antecedent2, RestAnte2),        % return leftovers
        append(RestConse1, Consequent2, Consequent),    % cobble leftovers together
        append(Antecedent1, RestAnte2, Antecedent),
        record_clause(Consequent,Antecedent,N).         % record new clause


/* Record Existence of New Clause */
record_clause([],[],N) :-                       % test for empty clause
        writef('Success! Empty Clause Found\n\n'), !,   % tell user
        abort.                                  % and stop

record_clause(Consequent,Antecedent,N) :-       % test for loop
        find_clause(Name,Consequent,Antecedent,M), !.   % i.e. clause with same innards

record_clause(Consequent,Antecedent,N) :- !,    % record new clause
        gensym(clause,Name),                    % make up new name
        assert(clause(Name,Consequent,Antecedent,N)),   % assert clause
        writef('%t is name of new resolvant %l <- %l at depth %t\n\n',
                [Name,Consequent,Antecedent,N]).        % tell user


/* Find a clause at depth N */

find_clause(Name,Consequent,Antecedent,0) :-
        clause(Name,Consequent,Antecedent,topclause), !.

find_clause(Name,Consequent,Antecedent,N) :-
        clause(Name,Consequent,Antecedent,N).


/* MINI-PROJECTS

1. Try this theorem prover with the clauses of file EQUAL.

2.  Experiment by making up some clauses of your own and trying them
out.

3.  Modify the theorem prover to print out the solution when it has
found it.

4.  Modify the theorem prover to remove the input restriction.

5.  Modify the theorem prover to incorporate the literal selection
restriction.

6. Build a depth first theorem prover along the same lines.

*/