home *** CD-ROM | disk | FTP | other *** search
- Newsgroups: comp.lang.prolog
- 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
- From: jur@robin.cs.hut.fi (Jussi Rintanen)
- Subject: Occurs check
- Message-ID: <1992Dec13.173016.8849@nntp.hut.fi>
- Sender: usenet@nntp.hut.fi (Usenet pseudouser id)
- Nntp-Posting-Host: robin.cs.hut.fi
- Reply-To: Jussi.Rintanen@hut.fi
- Organization: Helsinki University of Technology, Finland
- Date: Sun, 13 Dec 1992 17:30:16 GMT
- Lines: 114
-
-
- I have a simple program that finds proofs of theorems of propositional
- logics. The logics are formulated as sets of axiom schemes and the
- modus ponens inference rule. The axiom schemes (like A->(B->A)) are
- represented as terms with uninstantiated variables.
- The program works by trying out alternative ways of deriving
- a theorem from the axioms (using MP). In this process the theorem
- (and other formulae - possibly with uninstantiated variables - to be proved)
- are unified with parts of the axiom schemes: the occurs check is needed to
- avoid circular bindings.
-
- Question 1: What implementations of Prolog implement the occurs check?
- (Our university has both Sicstus and NU-Prolog.)
-
- ================================================================
- The program:
-
- /* Copyright 1992 Jussi Rintanen, Helsinki University of Technology */
-
- ?- dynamic(axiom/2).
- ?- dynamic(premise/1).
- ?- dynamic(bymp/2).
- ?- dynamic(derivable/2).
-
- %premise(p).
- axiom(impl(A,impl(B,A)),k).
- axiom(impl(impl(A,impl(B,G)),impl(impl(A,B),impl(A,G))),s).
- axiom(impl(impl(not(A),not(B)),impl(impl(not(A),B),A)),c).
-
- % these clauses, as well as the clauses for predicate hr, can be
- % easily computed from the axioms
- bymp(impl(_,A),[k,Pr]) :- derivable(A,Pr).
- bymp(impl(impl(A,B),impl(A,G)),[s,Pr]) :- derivable(impl(A,impl(B,G)),Pr).
- bymp(impl(A,G),[s,Pr1,Pr2]) :-
- derivable(impl(A,impl(B,G)),Pr1),
- derivable(impl(A,B),Pr2).
- bymp(G,[s,Pr1,Pr2,Pr3]) :-
- derivable(impl(A,impl(B,G)),Pr1),
- derivable(impl(A,B),Pr2),
- derivable(A,Pr3).
-
- bymp(A,[c,Pr1,Pr2]) :-
- derivable(impl(not(A),not(B)),Pr1),
- derivable(impl(not(A),B),Pr2).
-
- bymp(impl(impl(not(A),B),A),[c,Pr]) :-
- derivable(impl(not(A),not(B)),Pr).
-
- derivable(P,premise) :- premise(P).
- derivable(P,ax(Ax)) :- axiom(P,Ax).
- derivable(P,Proof) :- bymp(P,Proof).
-
- %
- % Iterative deepening
-
- iterdeep(Goal,Answer,Depth) :-
- iterdeep(Goal,Depth),
- write('Answer in depth '), write(Depth), nl.
-
- iterdeep(Goal,Answer,Depth) :-
- Depth1 is Depth + 1,
- iterdeep(Goal,Answer,Depth1).
-
- iterdeep(Goal,N) :- N > 0,
- clause(Goal,Body),
- N0 is N - 1,
- eachclause(Body,N0).
- eachclause(true,_) :- !.
- eachclause((A,B),N) :- !, eachclause(A,N), eachclause(B,N).
- eachclause(C,N) :- iterdeep(C,N).
-
- %
- proof(A,P) :- iterdeep(derivable(A,P),P,1).
-
- %
- hr(P,premise,[(L,P,'P')|X]-X,L) :- premise(P).
- hr(P,ax(Ax),[(L,P,Ax)|X]-X,L) :- axiom(P,Ax).
-
- hr(F,[AN,P1,P2,P3],Proof,L5) :-
- axiom(AF,AN), AF = impl(S1,impl(S2,impl(S3,F))),
- hr(S1,P1,Sp1,L1),
- hr(S2,P2,Sp2,L2),
- hr(S3,P3,Sp3,L3),
- conc(Sp1,Sp2,Sp12),
- conc(Sp12,Sp3,Sp123),
- conc(Sp123,[(L4,AF,AN),(L5,F,mp(L1,L2,L3,L4))|X]-X,Proof).
-
- hr(F,[AN,P1,P2],Proof,L5) :-
- axiom(AF,AN), AF = impl(S1,impl(S2,F)),
- hr(S1,P1,Sp1,L1),
- hr(S2,P2,Sp2,L2),
- conc(Sp1,Sp2,Sp12),
- conc(Sp12,[(L4,AF,AN),(L5,F,mp(L1,L2,L4))|X]-X,Proof).
-
- hr(F,[AN,P1],Proof,L5) :-
- axiom(AF,AN), AF = impl(S1,F),
- hr(S1,P1,Sp1,L1),
- conc(Sp1,[(L4,AF,AN),(L5,F,mp(L1,L4))|X]-X,Proof).
-
- lnumber([],_).
- lnumber([(N,_,_)|Ls],N) :- N1 is N + 1, lnumber(Ls,N1).
-
- sh(Formula,Proof) :-
- hr(Formula,Proof,Tabular-[],_),
- lnumber(Tabular,1),
- pt(Tabular).
-
- giveproof(F) :- proof(F,P), sh(F,P).
-
- pt([]) :- nl.
- pt([(A,B,C)|Ls]) :- write(A), write(' '), write(B), write(' '), write(C), nl,
- pt(Ls).
-
- conc(A-B,B-C,A-C).
-