411 REFERENCE · Wikibooks
Logic for Computer Scientists/Predicate Logic/Strategies for Resolution/A Prolog-like Implementation
Reference material by Wikibooks contributors. This retains its source identity and is not 411 news reporting.
A Prolog-like Implementation
gprove(true,_).
gprove((G & H),A):-
gprove(G,A),
gprove(H,A).
gprove(G,A):-
member(G,A).
gprove(G,A):-
(G <- B),
neg(G,NG),
gprove(B,[NG|A]).
p(a,X) <- ~p(b,Y) & q(X,Y).
p(b,Y) <- ~p(a,X) & q(X,Y).
~q(X,Y) <- ~p(a,X) & ~p(b,Y).
p(Z,Z) <- true.
q(b,a) <- true.
yes <- p(U,V).
~p(U,V) <- ~yes.