/* HEURIS.

A Heurisitic Search Theorem Prover.
EQUAL contains test example.

Alan Bundy 19.6.81 */


/* Top Goal */

go :-
        clause(Goal,_,_,topclause),
        heuristic([Goal]).


/* Heuristic Search Strategy */

heuristic(Fringe) :-
        pick_best(Fringe,Current,Rest),         % Pick the clause with best score
        findall(Clause,successor(Current,Clause),NewClauses),   % findall its successors
        append(Rest,NewClauses,NewFringe),      % Put them on fringe
        heuristic(NewFringe).                   % and recurse


/* Clause is a resolvant of Current with an input clause */

successor(Current,Clause) :-
        clause(Input,_,_,input),        % Pick an input clause
        ( resolve(Current,Input,Clause) ; resolve(Input,Current,Clause) ).
                                        % resolve it with the current clause


/* Resolution Step */

resolve( Parent1, Parent2, Resolvant) :-
        clause(Parent1, Consequent1, Antecedent1, N1),  % Get the two parents
        clause(Parent2, Consequent2, Antecedent2, N2),
        select(Literal, Consequent1, RestConse1),       % Select a common literal
        select(Literal, Antecedent2, RestAnte2),        % and return the rest
        append(RestConse1, Consequent2, Consequent),    % Join the odd bits together
        append(Antecedent1, RestAnte2, Antecedent),
        record_clause(Consequent,Antecedent,Resolvant). % Record the clause


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

record_clause(Consequent,Antecedent,Name) :-    % test for loop
        clause(Name,Consequent,Antecedent,M), !, fail.

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


/* Evaluation Function on Clauses (length of clause) */

evaluate(Consequent,Antecedent,Score) :-
        length(Consequent,C),   % add length of rhs
        length(Antecedent,A),   % to length of lhs
        Score is C+A.           % to get clause length


/* Pick clause with best score (i.e.lowest) */

pick_best([Hd|Tl],Choice,Rest) :-
        clause(Hd,_,_,N),               % Get score of first clause
        pick_best(Tl,Hd,N,Choice,Rest). % and run down list remembering best so far

pick_best([],Hd,N,Hd,[]).       % When you get to the end return running score

pick_best([Hd1|Tl1],Hd,N,Choice,[Hd3|Rest]) :-
        clause(Hd1,_,_,N1),                     % Get score of first clause
        compare(Hd,N,Hd1,N1,Hd2,N2,Hd3,N3),     % Compare with running score and order them
        pick_best(Tl1,Hd2,N2,Choice,Rest).      % recurse with new best score

compare(Hd,N,Hd1,N1,Hd,N,Hd1,N1) :-     % put running score first
        N =< N1, !.                     % unless new score is best

compare(Hd,N,Hd1,N1,Hd1,N1,Hd,N).       % Otherwise put new score first


/* Find a clause with score N */

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

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


/* MINI-PROJECTS

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

2.  Experiment with clauses of your own devising.

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.  Experiment with different versions of the evaluation function by
modifying 'evaluate' (see section 6.5.3 of 'Artificial
Mathematicians').

*/