%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% geoprolog.pl %% http://www.csupomona.edu/~jrfisher/www/geolog %% jrfisher@csupomona.edu %% bezem@ii.uib.no %% Change 3/1/2008: .gl files can now use '|' or ';' %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% :- op(1150,xfx,'=>'), op(1200,xfx,axiom), % Bezem's annotations op(700,xfx,'==='), % mathematical equality op(600,xfx,'#'). % another infix math op :- dynamic theory/1, leaf/1, count/1, log/0, logged/0, goal/0, false/0, geolog:theory_term/1. info:- nl, writeln('%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 07/16/2007 '), write('%% GeoProlog '), (theory(T) -> write('G: '),writeln(T) ; nl), writeln('%% ?- compile(+G). % Compile Geolog rules in file G.gl '), writeln('%% ?- show. % Show ordered rules ... '), writeln('%% ?- go. % Attempt proof ... '), writeln('%% Control C stops runaway ''go''... hit ''a'' key for abort '), writeln('%% ?- golog. % go+log if ''go'' terminated '), writeln('%% ?- golog(+N). % go+log, N steps only '), writeln('%% ?- tree. % Show search tree for last golog ... '), writeln('%% ?- proof. % Generate minimal case proofs ... '), writeln('%% ?- info. % Display this info '), writeln('%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%'),nl. :- info. %%%%% INFERENCE >>>>>>>>>>> %% translate(+TranscribedGeolog,-Prolog) translate(K, (ANT => CONS), Prolog) :- (CONS=(F;R) ; CONS=(F|R)) -> %% split rule Prolog= (try(K,(ANT => CONS),S) :- geolog:ANT, \+sat(CONS), (log->infer(K,ANT,CONS,C1);C1 is 0), memo(F,[],S1), try(_,_,S1), split(C1,S,R) ) ; Prolog= (try(K,(ANT => CONS),S) :- geolog:ANT, \+sat(CONS), (log->infer(K,ANT,CONS,C1);C1 is 0), memo(CONS,S,S1), try(_,_,S1) ) . %% currently memo'ed sat(D) :- (D=(F;R) ; D=(F|R)) -> (sat(F) ; sat(R)) ; D=(_^B) -> geolog:B ; geolog:D. %% alternate cases split(C,S,G) :- (log->writeLink(C);true), %% branch (G=(F;R) ; G=(F|R)) -> memo(F,[],S1), try(_,_,S1), split(C,S,R) ; memo(G,S,S1), try(_,_,S1). % last branch forget(F) :- F=[R|Rs] -> erase(R), forget(Rs) ; true. %% extend current state memo(F,I,O) :- F=V^B -> gensym('sk',V), memo(B,I,O) ; F=(J,K) -> assertz(geolog:J,R), (log->writeFact(J);true), memo(K,[R|I],O) ; assertz(geolog:F,R), (log->writeFact(F);true), O=[R|I]. %%%%% LOADER/COMPILER >>>>>>>>>>> compile(File) :- reset, % first make sure old facts are deleted retractall(theory(_)), abolish(try/3), retractall(geolog:theory_term(_)), init_count, seen, told, retractall(logged), in2gl(File), %% convert .in file to .gl, if it exists %% load and translate a geolog (.gl) file name(File,NameList), append(NameList,[46,103,108],A), name(F,A), %%.gl assertz((try(0,final_rule,S) :- %% top try! (geolog:goal ; geolog:false), forget(S), (log->writeLeaf;true), ! )), see(F), repeat, read(Geolog), process(Geolog), seen, %% user's theory assert(theory(File)), % new theory assertz( (try(-1,countermodel_rule,S) :- %% last try forget(S), (log->writeLeaf;true), writeln('%% COUNTER-MODEL') )), %% S may be partial compile_predicates([try/3]), write('%% '), write(F), writeln(' compiled to Prolog.'), ! . process(end_of_file) :- !. process((A=>C)) :- declare((A=>C)), transcribe((A=>C),G), writeq(G), write('.'), write(' %'), getCount(Count), writeln(Count), translate(Count,G,Clause), assertz(Clause), fail. % Processing anything other than form (A=>C) fails automatically, unnoticed. %% declare Geolog functors dynamic (except 'true'). declare(true) :- !. %% never changes declare((A=>C)) :- !, declare(A), declare(C). declare((A;C)) :- !, declare(A), declare(C). declare((A|C)) :- !, declare(A), declare(C). declare(F) :- F=(A,C) -> declare(A),declare(C) ; dynamic(geolog:F), functor(F,P,A), functor(T,P,A), (geolog:theory_term(T) -> true ; assert(geolog:theory_term(T))). %% delete facts from interrupted run reset :- setof(T,geolog:theory_term(T),S),!, reset(S). reset. reset([F|R]) :- retractall(geolog:F), reset(R). reset([]). %% Separate free variables in consequent and add existential quantifiers (X^...). transcribe((A=>C),(A=>C1)) :- term_variables(A,Universals), alter(C,Universals,C1). alter((C;D),U,(C2;D1)) :- !, copy_term_nat(U^C,U^C1), term_variables(C1,V), exclude(V,U,V1), prefix(V1,C1,C2), alter(D,U,D1). alter((C|D),U,(C2|D1)) :- !, copy_term_nat(U^C,U^C1), term_variables(C1,V), exclude(V,U,V1), prefix(V1,C1,C2), alter(D,U,D1). alter(C,U,C2) :- copy_term_nat(U^C,U^C1), term_variables(C1,V), exclude(V,U,V1), prefix(V1,C1,C2). prefix([],E,E). prefix([V|Vs],E,(V^Es)) :- prefix(Vs,E,Es). %% exclude variables. exclude([X|R],Xclude,R1) :- coincident(X,Xclude), !, exclude(R,Xclude,R1). exclude([X|R],Xclude,[X|R1]) :- exclude(R,Xclude,R1). exclude([],_,[]). coincident(X,[Y|_]) :- X == Y. coincident(X,[_|R]) :- coincident(X,R). %%%%% RUNTIME >>>>>>>>>>> init_count :- retractall(count(_)), assert(count(1)). getCount(C) :- retract(count(C)), C1 is C+1, assert(count(C1)). show :- seen, told, findall((K,(A=>C)),clause(try(K,(A=>C),_),_),Rs), theory(T), write('% source: '), writeln(T), cascade(Rs). cascade([(K,X)|R]) :- writeq(X), write('.'), write(' %'), writeln(K), cascade(R). cascade([]). go:- reset, clear, retractall(log),retractall(logged), init_count, writeln('Thinking ...'), time(try(_,_,[])). %% go+log golog(N) :- seen,told, reset, clear, retractall(limit(_)), retractall(logged), assert(limit(N)), assert(log), retractall(leaf(_)), init_count, theory(T), writeln('Thinking ...'), name(T,NameList), append(NameList,[46,108,111,103],A), name(Log,A), %.log tell(Log), writeq(fact(0,true)), writeln('.'), try(_,_,[]), told, assert(logged), write('%% '), write(Log), writeln(' created'), retractall(log), !. tree :- (logged -> true ; (write('Use golog or golog(+N) first.'), fail)), seen, told, theory(T), name(T,NameList), append(NameList,[46,108,111,103],A), name(Log,A), %.log append(NameList,[46,100,103,108],B), name(Dgl,B), %%.dgl tell(Dgl), count(C), C1 is C-1, write('size ## '), writeln(C1), see(Log), repeat, read(P), express(P), seen, told, %% .dgl CREATED name('java -cp GeologTree.jar GeologTreePane ',PreList), append(PreList,B,D), name(DIAGRAM,D), writeln('Wait for Geolog Tree Viewer to start ...'), shell(DIAGRAM), retractall(log), !. proof :- (logged -> true ; (write('Use golog or golog(+N) first.'), fail)), writeln('Thinking ...'), seen, told, theory(T), name(T,NameList), append(NameList,[46,112,114,102],B), name(Prf,B), %%.prf tell(Prf), proof(T), told, %% .prf CREATED write('%% '), write(Prf), writeln(' created'), clear. express(end_of_file). express(fact(N,F)) :- write('fact ## '), write(N), write(' ## '), writeq(F), nl, fail. express(link(A,B)) :- write('link ## '), write(A), write(' ## '), write(B), nl, fail. express(inference(N,(K,I))) :- write('inference ## '), write(N), write(' ## '), write('rule '), write(K), write(': '), writeq(I), nl, fail. %% logging golog:-golog(1000000). %% Only use if go terminated writeLeaf :- count(C),C1 is C-1, assertz(leaf(C1)). infer(RuleNum,ANT,CONS,Anchor) :- count(C), limit(L), C < L, %% could fail Anchor is C-1, writeq(inference(Anchor, (RuleNum,(ANT=>CONS)))), writeln('.'). writeFact(F) :- getCount(C), writeq(fact(C,F)), writeln('.'), C1 is C-1, (leaf(C1) -> true; (writeq(link(C1,C)), writeln('.'))). writeLink(C) :- count(K), writeq(link(C,K)), writeln('.') . %%%%% SHORTCUTS >>>>>>>>>>> c(File):-compile(File). g:-go. gol:-golog. t:-tree. i:-info. s:-show. %%%%% CONVERT F.in to F.gl >>>>>>>>>>> %% if File.in exists, convert it in2gl(File) :- name(File,NameList), append(NameList,[46,105,110],INL), name(IN,INL), exists_file(IN), !, append(NameList,[46,103,108],GLL), name(GL,GLL), see(IN), tell(GL), repeat, read(Bez), convert(Bez,Comment,Geolog), record(Comment,Geolog), seen, told, write('%% '), write(IN), write(' converted to '),writeln(GL). in2gl(_). %% .in file not present convert(end_of_file,end_of_file,end_of_file). convert(dom(X),'domain declaration', (true => dom(X))). convert(P axiom Q : R,(P axiom Q),R). %% annotation becomes comment record(end_of_file,end_of_file) :- told. record(Anno,Geolog) :- write('%% '), write(Anno),nl, writeq(Geolog), writeln('.'), fail. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Extract minimal case proofs from from .log file. %% Prototype version: needs improvement. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% :- dynamic link/2, fact/2, inference/2. proof(F) :- tree(F), write('Minimal case proofs for: '), writeln(F), nl, tree_leaf(L), write('Leaf '), write(L), writeln(':'), (\+fact(L,goal), \+fact(L,false) -> writeln(' #####') ; gather(L,Rules), sweep(Rules,[],[],UsedRules,_), pare(UsedRules,UsedRules,[],Pared), excise(UsedRules,Pared,MCP), list(MCP) ), writeln('------------'), fail. proof(_). clear :- retractall(link(_,_)), retractall(fact(_,_)), retractall(inference(_,_)). tree(File) :- clear, name(File,NameList), append(NameList,[46, 108, 111, 103],A), % .log name(F,A), see(F), repeat, read(Data), maketree(Data), seen, !. maketree(Data) :- Data=end_of_file -> true ; assert(Data), fail. %% define leaf of tree tree_leaf(L) :- link(_,L), \+link(L,_). %% gather rules up a tree branch gather(0,L) :- !, % root of tree inference(0,(_,I)) -> L=[(0,I)] ; L=[]. gather(N,L) :- link(J,N), gather(J,T), (inference(N,(_,I)) -> L=[(N,I)|T] ; L=T). list([]). list([(N,I)|R]):- inference(N,(K,_)), % retrieve rule # write(N), write(', '), writeq(I), write(', rule #'), write(K), nl, list(R). %% sweep(+,[],[],-,-) sweep([(I,(A=>C))|Rs],Rules,Facts,R,F) :- (used(C,C1,Facts) -> add(A,Facts,NewFacts), NewRules=[(I,(A=>C1))|Rules] ; NewFacts=Facts, NewRules=Rules), sweep(Rs,NewRules,NewFacts,R,F). sweep([],Rules,Facts,Rules,Facts). %% used rules by the facts used(goal,goal,_) :- !. used(false,false,_) :- !. used((C;D),C1,Facts) :- used(C,C1,Facts), ! ; used(D,C1,Facts). used((C|D),C1,Facts) :- used(C,C1,Facts), ! ; used(D,C1,Facts). used(_^C,C,Facts) :- !, used(C,Facts). used(C,C,Facts) :- used(C,Facts). used((A,B),Facts) :- used(A,Facts), ! ; used(B,Facts). used((A),Facts) :- member(A,Facts). add((A,B),Facts,NewFacts) :- !, add(B,[A|Facts],NewFacts). add((A),Facts,[A|Facts]). %% Pare a rule from the proof provided that each of %% its conclusions is concluded by some OTHER non-pared rule. pare([(I,(_=>C))|R],Rules,Pared,Result) :- achieved(I,C,Rules,Pared), !, %% ... via non-Pared rules pare(R,Rules,[I|Pared],Result). pare([_|R],Rules,Pared,Result) :- pare(R,Rules,Pared,Result). pare([],_,Pared,Pared). achieved(I,(A,B),Rules,Pared) :- !, yielded(I,A,Rules,Pared), achieved(I,B,Rules,Pared). achieved(I,(A),Rules,Pared) :- yielded(I,A,Rules,Pared). yielded(I,A,[(N,(_=>C))|R],Pared) :- \+(I is N), \+memberchk(N,Pared), memseq(A,C) ; yielded(I,A,R,Pared). memseq(X,(X,_)) :- !. memseq(X,(_,R)) :- !, memseq(X,R). memseq(X,X). excise([(I,_)|R],Pared,S) :- memberchk(I,Pared), !, excise(R,Pared,S). excise([F|R],Pared,[F|S]) :- excise(R,Pared,S). excise([],_,[]).