/* SEMANT.

A Depth First Theorem Prover
with vetting by use of interpretations and
incorporating input restriction.
Use with MODEL
DIVIDE contains test example

Alan Bundy 22.6.81 */


/* Top Goal */

go :-
        clause(Goal,_,_,topclause),     % Find the top clause
        semantic(Goal).                 % and away you go


/* Depth first theorem prover */
semantic(Old) :-
        successor(Old,New),     % Find a successor to the current clause
        vet(New),               % check that it is unsatisfiable
        semantic(New).          % 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 it with the
          resolve(Input,Current,Clause) ;       % current clause
          paramodulate(Current,Input,Clause) ;  % or paramodulate it
          paramodulate(Input,Current,Clause) ).



/* Resolution Step */

resolve( Parent1, Parent2, Resolvant) :-
        clause(Parent1, Consequent1, Antecedent1, _),   % Get the two parents
        clause(Parent2, Consequent2, Antecedent2, _),
        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



/* Paramodulation Step */

paramodulate( Parent1, Parent2, Paramodulant ) :-
        clause(Parent1, Consequent1, Antecedent1, _),   % Get the two parents
        clause(Parent2, Consequent2, Antecedent2, _),
        select(equal(T,S), Consequent1, RestConse1),    % select an equation
        replace(T,S,Consequent2,Antecedent2,NewConse2,NewAnte2),% put it in the other clause
        append(RestConse1,NewConse2,Consequent),        % join the odd bits together
        append(Antecedent1,NewAnte2,Antecedent),
        record_clause(Consequent,Antecedent,Paramodulant).      %record the clause


/* Replace T by S (or S by T) in clause */

replace(T,S,OldConse,OldAnte,NewConse,OldAnte) :-       % replace T by S in
        replace1(T,S,OldConse,NewConse).                % the consequent

replace(T,S,OldConse,OldAnte,OldConse,NewAnte) :-       % or T by S in
        replace1(T,S,OldAnte,NewAnte).                  % the antecedent

replace(S,T,OldConse,OldAnte,NewConse,OldAnte) :-       % or S by T in
        replace1(S,T,OldConse,NewConse).                % the consequent

replace(S,T,OldConse,OldAnte,OldConse,NewAnte) :-       % or S by T in
        replace1(S,T,OldAnte,NewAnte).                  % the antecedent


/* Replace T by S in Old to get New */

replace1(T,S,Old,New) :-
        some(replace2(T,S),Old,New).    % replace one of the literals

replace2(T,S,T,S).              % replace this occurence

replace2(T,S,Old,New) :-                % replace one of the arguments
        Old =.. [Sym | OldArgs],        % get the arguments
        replace1(T,S,OldArgs,NewArgs),  % replace one
        New =.. [Sym | NewArgs].        % put it all together again



/* Record Existence of New Clause */

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

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

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


/* Apply Pred to just one element of list */

some(Pred, [Hd1 | Tl], [Hd2 | Tl]) :-
        apply(Pred, [Hd1,Hd2]).         % apply it to this one

some(Pred, [Hd | Tl1], [Hd | Tl2]) :-
        some( Pred, Tl1, Tl2).          % or one of the others


/* MINI-PROJECTS

1.  Try out theorem prover with the arithmetic clauses and models of
file DIVIDE.

2.  Experiment with some clauses and models of your own devising (See
chapter 10 for some ideas).

3.  Modify the theorem prover so that it works by breadth first search
(Compare with file BREADT).

4.  Modify the theorem prover so that it works by heuristic search
(Compare with file HEURIS).

*/