
(Message 6)
From:     HELEN    HPS (on ERCC DEC-10) <Pain@EDXA>
Date:     Wednesday, 16-Jan-85 14:06:21-GMT
To:       ecmi08@2972,Pain@EDXA
Via:      uk.ac.edinburgh.edxa  ; (to uk.ac.edinburgh.emas) 16 Jan 85  14:11:55 gmt
Msg ID:   <132001-454-734@EDXA>

--------
/* HEURISTIC SEARCH THEOREM PROVER */

go :- heuristic([pair(1,goal)]).

/* Top Level Stuff */
heuristic(Agenda) :-
	member(pair(0,Empty),Agenda).


heuristic( [pair(Score,Current) | Rest] ) :-
	setof1(Clause,successor(Current,Clause),NewClauses),
	add_to_agenda(NewClauses,Rest,NewAgenda),
	heuristic(NewAgenda).			


successor(Current,Clause) :-
	successor1(Current,Clause1),
	vet(Clause1,Clause,model1),
	message(Clause).		%new

successor1(Current,Clause) :-
	factor(Current,Clause).

successor1(Current,Clause) :-
	is_clause(Parent,_,_),
	( resolve(Current,Parent,Clause) ;
		resolve(Parent,Current,Clause) ).

/* Rules of Inference */
resolve( Parent1, Parent2, Resolvant) :-
	is_clause(Parent1, Consequent1, Antecedent1),
	is_clause(Parent2, Consequent2, Antecedent2),
	select(Proposition, Consequent1, RestConse1),
	select(Proposition, Antecedent2, RestAnte2),
	append(RestConse1, Consequent2, Consequent),
	append(Antecedent1, RestAnte2, Antecedent),
	gensym(resolvant,Resolvant),
	assert(is_clause(Resolvant,Consequent,Antecedent)).


factor( Clause, Factor ) :-
	is_clause(Clause,Consequent,Antecedent),
	select(Proposition,Consequent,OneGone),
	select(Proposition,OneGone,TwoGone),
	gensym(factor,Factor),
	assert(is_clause(Factor,OneGone,Antecedent)).

factor( Clause, Factor ) :-
	is_clause(Clause,Consequent,Antecedent),
	select(Proposition,Antecedent,OneGone),
	select(Proposition,OneGone,TwoGone),
	gensym(factor,Factor),
	assert(is_clause(Factor,Consequent,OneGone)).


/* Print Message */		%new
message(Clause) :-
	is_clause(Clause,Conse,Ante),
	write('New Clause, '),
	write(Clause),
	write(', is '),
	write(Ante),
	write(' -> '),
	write(Conse),
	write('

').


/* Evaluation Function */
add_to_agenda([],Agenda,Agenda).

add_to_agenda([Name|Rest],Agenda,NewAgenda) :-
	\+ on(Name,Agenda),		%new
	evaluate(Name,Score),
	insert_into_agenda(Agenda,Score,Name,MidAgenda),	%new
	add_to_agenda(Rest,MidAgenda,NewAgenda).


evaluate(Name,Score) :-
	is_clause(Name,Consequence,Antecedent),
	length(Consequence,C),
	length(Antecedent,A),
	Score is C+A.


insert_into_agenda([],Score,Name,[pair(Score,Name)]).

insert_into_agenda([pair(Score1,Name1)|Rest],Score,Name,
			[pair(Score,Name),pair(Score1,Name1)|Rest]) :-
	Score =< Score1,
	!.

insert_into_agenda([X|Rest],Score,Name,[X|NewRest]) :-
	insert_into_agenda(Rest,Score,Name,NewRest).

/* Loop Check */		%new
on(Clause,Agenda) :-
	is_clause(Clause,Conse,Ante),
	member(pair(Score,Another),Agenda),
	is_clause(Another,Conse,Ante).


/* SEMANTIC CHECKING */

vet(Clause1,Clause,Interp) :-
	is_clause(Clause1,Conse,Ante),
	constants(Consts),
	checklist(instantiate(Consts),Conse),
	checklist(instantiate(Consts),Ante),
	false_clause(Conse,Ante,Interp),
	gensym(instance,Clause),
	assert(is_clause(Clause,Conse,Ante)).


instantiate(Consts,Constant) :-
	atomic(Constant).

instantiate(Consts,Variable) :-
	var(Variable), member(Variable,Consts).

instantiate(Consts,Complex) :-
	\+ atomic(Complex),
	\+ var(Complex),
	Complex =.. [Sym|Paras],
	checklist(instantiate(Consts),Paras).


false_clause(Consequent,Antecedent,Interp) :-
	checklist(meaning(Interp,false), Consequent),	
	checklist(meaning(Interp,true), Antecedent).


meaning( Interp, Value, Constant ) :-
	atomic(Constant), !, interpret(Interp, Value, Constant).

meaning( Interp, Value, Complex ) :-
	Complex =.. [Sym | Paras], !,
	maplist(meaning(Interp), Vals, Paras),
	Complex1 =.. [Sym | Vals],
	interpret(Interp, Value, Complex1).


/* GENERAL UTILITIES */

/* List Processing */
append([],List,List).

append([Car|Cdr],List,[Car|Ans]) :- append(Cdr,List,Ans).

member(E,L) :- append(L1,[E|L2],L).

select(E,L,R) :- append(L1,[E|L2],L), append(L1,L2,R).


/* Logical */
setof1(X,P,Set) :- setof(X,P,Set), !.

setof1(X,P,[]).


checklist(P,[]) :- !.

checklist(P,[Y|YList]) :- !,
	P =.. [Sym | XList],
	append(XList,[Y],Paras),
	Q =.. [Sym | Paras],
	Q,
	checklist(P,YList).

maplist(P,[],[]) :- !.

maplist(P,[Y|YList],[Z|ZList]) :- !,
	P =.. [Sym | XList],
	append(XList,[Y,Z],Paras),
	Q =.. [Sym | Paras],
	Q,
	maplist(P,YList,ZList).

/* Generate New Name */
gensym(Prefix,Var) :-
	var(Var), atomic(Prefix),
	get(Prefix,N),
	N1 is N+1,
	assert(latest(Prefix,N1)),
	concat(Prefix,N1,Var).

get(Prefix,N) :- retract(latest(Prefix,N)), !.
get(Prefix,0).

concat(N1,N2,N) :-
	name(N1,Ls1),
	name(N2,Ls2),
	append(Ls1,Ls2,Ls),
	name(N,Ls).


/* EXAMPLE SPECIFIC STUFF */

/* Axioms and Negated Conjecture */
is_clause(reflexive,  [equal(X,X)], [] ).

is_clause(funny,[equal(X,Y)],[equal(X,z),equal(z,Y)]).

is_clause(twisted,    [equal(U,W)], [equal(U,V), equal(W,V)] ).

is_clause(hypothesis, [equal(x,y)], [] ).

is_clause(goal,	   [], [equal(y,x)] ).

/* Constants */
constants([x,y,z]).

/* Interpretation Model1 */
interpret(model1, 2, x).

interpret(model1, 2, y).

interpret(model1, 3, z).

interpret(model1, true, equal(X,Y)) :-
	X == Y.

interpret(model1, false, equal(X,Y)) :-
	X \== Y.


--------
 