Logic for Computer Scientists/Predicate Logic/Strategies for Resolution/A Prolog-like Implementation

From Wikibooks, open books for an open world
< Logic for Computer Scientists‎ | Predicate Logic‎ | Strategies for Resolution
Jump to navigation Jump to search

A Prolog-like Implementation[edit | edit source]


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.
Retrieved from "https://en.wikibooks.org/w/index.php?title=Logic_for_Computer_Scientists/Predicate_Logic/Strategies_for_Resolution/A_Prolog-like_Implementation&oldid=1567496"