home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #30 / NN_1992_30.iso / spool / comp / lang / prolog / 2225 < prev    next >
Encoding:
Text File  |  1992-12-13  |  3.7 KB  |  127 lines

  1. Newsgroups: comp.lang.prolog
  2. Path: sparky!uunet!ornl!sunova!linac!uwm.edu!zaphod.mps.ohio-state.edu!sdd.hp.com!spool.mu.edu!yale.edu!ira.uka.de!math.fu-berlin.de!news.netmbx.de!Germany.EU.net!mcsun!news.funet.fi!funic!nntp.hut.fi!robin.cs.hut.fi!jur
  3. From: jur@robin.cs.hut.fi (Jussi Rintanen)
  4. Subject: Occurs check
  5. Message-ID: <1992Dec13.173016.8849@nntp.hut.fi>
  6. Sender: usenet@nntp.hut.fi (Usenet pseudouser id)
  7. Nntp-Posting-Host: robin.cs.hut.fi
  8. Reply-To: Jussi.Rintanen@hut.fi
  9. Organization: Helsinki University of Technology, Finland
  10. Date: Sun, 13 Dec 1992 17:30:16 GMT
  11. Lines: 114
  12.  
  13.  
  14. I have a simple program that finds proofs of theorems of propositional
  15. logics. The logics are formulated as sets of axiom schemes and the
  16. modus ponens inference rule. The axiom schemes (like A->(B->A)) are
  17. represented as terms with uninstantiated variables.
  18. The program works by trying out alternative ways of deriving
  19. a theorem from the axioms (using MP). In this process the theorem
  20. (and other formulae - possibly with uninstantiated variables - to be proved)
  21. are unified with parts of the axiom schemes: the occurs check is needed to
  22. avoid circular bindings.
  23.  
  24. Question 1: What implementations of Prolog implement the occurs check?
  25. (Our university has both Sicstus and NU-Prolog.)
  26.  
  27. ================================================================
  28. The program:
  29.  
  30. /* Copyright 1992 Jussi Rintanen, Helsinki University of Technology */
  31.  
  32. ?- dynamic(axiom/2).
  33. ?- dynamic(premise/1).
  34. ?- dynamic(bymp/2).
  35. ?- dynamic(derivable/2).
  36.  
  37. %premise(p).
  38. axiom(impl(A,impl(B,A)),k).
  39. axiom(impl(impl(A,impl(B,G)),impl(impl(A,B),impl(A,G))),s).
  40. axiom(impl(impl(not(A),not(B)),impl(impl(not(A),B),A)),c).
  41.  
  42. % these clauses, as well as the clauses for predicate hr, can be
  43. % easily computed from the axioms
  44. bymp(impl(_,A),[k,Pr]) :- derivable(A,Pr).
  45. bymp(impl(impl(A,B),impl(A,G)),[s,Pr]) :- derivable(impl(A,impl(B,G)),Pr).
  46. bymp(impl(A,G),[s,Pr1,Pr2]) :-
  47.     derivable(impl(A,impl(B,G)),Pr1),
  48.     derivable(impl(A,B),Pr2).
  49. bymp(G,[s,Pr1,Pr2,Pr3]) :-
  50.     derivable(impl(A,impl(B,G)),Pr1),
  51.     derivable(impl(A,B),Pr2),
  52.     derivable(A,Pr3).
  53.  
  54. bymp(A,[c,Pr1,Pr2]) :-
  55.     derivable(impl(not(A),not(B)),Pr1),
  56.     derivable(impl(not(A),B),Pr2).
  57.  
  58. bymp(impl(impl(not(A),B),A),[c,Pr]) :-
  59.     derivable(impl(not(A),not(B)),Pr).
  60.  
  61. derivable(P,premise) :- premise(P).
  62. derivable(P,ax(Ax)) :- axiom(P,Ax).
  63. derivable(P,Proof) :- bymp(P,Proof).
  64.  
  65. %
  66. % Iterative deepening
  67.  
  68. iterdeep(Goal,Answer,Depth) :-
  69.     iterdeep(Goal,Depth),
  70.     write('Answer in depth '), write(Depth), nl.
  71.  
  72. iterdeep(Goal,Answer,Depth) :-
  73.     Depth1 is Depth + 1,
  74.     iterdeep(Goal,Answer,Depth1).
  75.  
  76. iterdeep(Goal,N) :- N > 0,
  77.     clause(Goal,Body),
  78.     N0 is N - 1,
  79.     eachclause(Body,N0).
  80. eachclause(true,_) :- !.
  81. eachclause((A,B),N) :- !, eachclause(A,N), eachclause(B,N).
  82. eachclause(C,N) :- iterdeep(C,N).
  83.  
  84. %
  85. proof(A,P) :- iterdeep(derivable(A,P),P,1).
  86.  
  87. %
  88. hr(P,premise,[(L,P,'P')|X]-X,L) :- premise(P).
  89. hr(P,ax(Ax),[(L,P,Ax)|X]-X,L) :- axiom(P,Ax).
  90.  
  91. hr(F,[AN,P1,P2,P3],Proof,L5) :-
  92.     axiom(AF,AN), AF = impl(S1,impl(S2,impl(S3,F))),
  93.     hr(S1,P1,Sp1,L1),
  94.     hr(S2,P2,Sp2,L2),
  95.     hr(S3,P3,Sp3,L3),
  96.     conc(Sp1,Sp2,Sp12),
  97.     conc(Sp12,Sp3,Sp123),
  98.     conc(Sp123,[(L4,AF,AN),(L5,F,mp(L1,L2,L3,L4))|X]-X,Proof).
  99.  
  100. hr(F,[AN,P1,P2],Proof,L5) :-
  101.     axiom(AF,AN), AF = impl(S1,impl(S2,F)),
  102.     hr(S1,P1,Sp1,L1),
  103.     hr(S2,P2,Sp2,L2),
  104.     conc(Sp1,Sp2,Sp12),
  105.     conc(Sp12,[(L4,AF,AN),(L5,F,mp(L1,L2,L4))|X]-X,Proof).
  106.  
  107. hr(F,[AN,P1],Proof,L5) :-
  108.     axiom(AF,AN), AF = impl(S1,F),
  109.     hr(S1,P1,Sp1,L1),
  110.     conc(Sp1,[(L4,AF,AN),(L5,F,mp(L1,L4))|X]-X,Proof).
  111.  
  112. lnumber([],_).
  113. lnumber([(N,_,_)|Ls],N) :- N1 is N + 1, lnumber(Ls,N1).
  114.  
  115. sh(Formula,Proof) :-
  116.     hr(Formula,Proof,Tabular-[],_),
  117.     lnumber(Tabular,1),
  118.     pt(Tabular).
  119.  
  120. giveproof(F) :- proof(F,P), sh(F,P).
  121.  
  122. pt([]) :- nl.
  123. pt([(A,B,C)|Ls]) :- write(A), write(' '), write(B), write(' '), write(C), nl,
  124.     pt(Ls).
  125.  
  126. conc(A-B,B-C,A-C).
  127.