220 lines
6.7 KiB
Prolog
220 lines
6.7 KiB
Prolog
/*****************************/
|
|
/* Christian Ohlsson */
|
|
/* Logik för dataloger */
|
|
/* Karlstad 990228 */
|
|
/* Laboration 3 i Logik */
|
|
/*****************************/
|
|
/* Functions included */
|
|
/* prenex */
|
|
/* implout */
|
|
/* negin */
|
|
/* kvant */
|
|
/* free_in */
|
|
/* rename_var */
|
|
/*****************************/
|
|
|
|
:- op(200,fx,~).
|
|
:- op(400,xfy,#).
|
|
:- op(400,xfy,&).
|
|
:- op(700,xfy,->).
|
|
:- op(700,xfy,<->).
|
|
|
|
prenex(Formel,PNF):-
|
|
implout(Formel,Svar1),
|
|
negin(Svar1,Svar2),
|
|
kvant(Svar2,PNF,[x1,x2,x3,x4,x5,x6,x7,x8,x9,x10],L).
|
|
|
|
/* ***************************** IMPLOUT **************************** */
|
|
|
|
implout((P<->Q),((P1&Q1)#(~P1&~Q1))) :- !,implout(P,P1),implout(Q,Q1).
|
|
implout((P->Q),(~P1#Q1)) :- !,implout(P,P1),implout(Q,Q1).
|
|
implout(all(X,P),all(X,P1)) :- !,implout(P,P1).
|
|
implout(exist(X,P),exist(X,P1)) :- !,implout(P,P1).
|
|
implout((P&Q),(P1&Q1)) :- !,implout(P,P1),implout(Q,Q1).
|
|
implout((P#Q),(P1#Q1)) :- !,implout(P,P1),implout(Q,Q1).
|
|
implout((~P),(~P1)) :- !,implout(P,P1).
|
|
implout(P,P).
|
|
|
|
/* ***************************** NEGIN **************************** */
|
|
|
|
negin((~P),P1) :- !,neg(P,P1).
|
|
negin(all(X,P),all(X,P1)) :- !,negin(P,P1).
|
|
negin(exist(X,P),exist(X,P1)) :- !,negin(P,P1).
|
|
negin((P&Q),(P1&Q1)) :- !,negin(P,P1),negin(Q,Q1).
|
|
negin((P#Q),(P1#Q1)) :- !,negin(P,P1),negin(Q,Q1).
|
|
negin(P,P).
|
|
neg((~P),P1) :- !,negin(P,P1).
|
|
neg(all(X,P),exist(X,P1)) :- !,neg(P,P1).
|
|
neg(exist(X,P),all(X,P1)) :- !,neg(P,P1).
|
|
neg((P&Q),(P1#Q1)) :- !,neg(P,P1),neg(Q,Q1).
|
|
neg((P#Q),(P1&Q1)) :- !,neg(P,P1),neg(Q,Q1).
|
|
neg(P,(~P)).
|
|
|
|
/* ***************************** RENAME-VAR **************************** */
|
|
|
|
r_v(X,exist(X,P),exist(F,P1),[F|R]):- r_v(X,P,P1,[F|R]).
|
|
r_v(X,exist(Y,P),exist(Y,P1),[F|R]):- X\==Y, r_v(X,P,P1,[F|R]).
|
|
|
|
r_v(X,all(X,P),all(F,P1),[F|R]):- r_v(X,P,P1,[F|R]).
|
|
r_v(X,all(Y,P),all(Y,P1),[F|R]):- X\==Y, r_v(X,P,P1,[F|R]).
|
|
|
|
r_v(X,Y#Z,Y1#Z1,[F|R]):- r_v(X,Y,Y1,[F|R]),r_v(X,Z,Z1,[F|R]).
|
|
r_v(X,Y&Z,Y1&Z1,[F|R]):- r_v(X,Y,Y1,[F|R]),r_v(X,Z,Z1,[F|R]).
|
|
r_v(X,Y->Z,Y1->Z1,[F|R]):- r_v(X,Y,Y1,[F|R]),r_v(X,Z,Z1,[F|R]).
|
|
r_v(X,Y<->Z,Y1<->Z1,[F|R]):- r_v(X,Y,Y1,[F|R]),r_v(X,Z,Z1,[F|R]).
|
|
|
|
r_v(X,Y,Y2,[F|R]):- Y=..[T,S],r_v(X,S,Y1,[F|R]), Y2=..[T,Y1].
|
|
r_v(X,[T|S],[F|S1],[F|R]):- X==T, r_v(X,S,S1,[F|R]).
|
|
r_v(X,[T|S],[S2|S1],[F|R]):- X\==T, r_v(X,S,S1,[F|R]),r_v(X,T,S2,[F|R]).
|
|
r_v(X,~P,~P1,[F|R]):- r_v(X,P,P1,[F|R]).
|
|
r_v(X,X,F,[F|R]).
|
|
r_v(X,U,U,[F|R]):- X\==U.
|
|
|
|
/* ***************************** FREE ****************************** */
|
|
|
|
free_in(X,exist(Y,P)):- X\==Y, free_in(X,P).
|
|
free_in(X,all(Y,P)):- X\==Y, free_in(X,P).
|
|
free_in(X,Y#Z):-free_in(X,Y);free_in(X,Z).
|
|
free_in(X,Y&Z):-free_in(X,Y);free_in(X,Z).
|
|
free_in(X,Y->Z):-free_in(X,Y);free_in(X,Z).
|
|
free_in(X,Y<->Z):-free_in(X,Y);free_in(X,Z).
|
|
|
|
free_in(X,Y):- Y=..[F,R],free_in(X,R).
|
|
free_in(X,[F|R]):-free_in(X,F);free_in(X,R).
|
|
|
|
free_in(X,~Z):-free_in(X,Z).
|
|
free_in(X,X).
|
|
|
|
|
|
/* ********************************************************************* */
|
|
/* ***************************** ALL & ***************************** */
|
|
|
|
kvant(all(X,Y)&Z,SY,[F|R],L3):-
|
|
(free_in(X,Z),
|
|
r_v(X,Z,Z1,[F]),
|
|
kvant(Y,Y1,R,R1),
|
|
kvant(Z1,Z2,R1,L2),
|
|
kvant(all(X,(Y1&Z2)),SY,L2,L3));
|
|
(kvant(Y,Y1,R,R1),
|
|
kvant(Z,Z2,R1,L2),
|
|
kvant(all(X,(Y1&Z2)),SY,L2,L3)).
|
|
|
|
/* ***************************** & ALL **************************** */
|
|
|
|
kvant(Z&all(X,Y),SY,[F|R],L3):-
|
|
(free_in(X,Z),
|
|
r_v(X,Z,Z1,[F]),
|
|
kvant(Y,Y1,R,R1),
|
|
kvant(Z1,Z2,R1,L2),
|
|
kvant(all(X,(Z2&Y1)),SY,L2,L3));
|
|
(kvant(Y,Y1,R,R1),
|
|
kvant(Z,Z2,R1,L2),
|
|
kvant(all(X,(Z2&Y1)),SY,L2,L3)).
|
|
|
|
|
|
/* ***************************** ALL # **************************** */
|
|
|
|
kvant(all(X,Y)#Z,SY,[F|R],L3):-
|
|
(free_in(X,Z),
|
|
r_v(X,Z,Z1,[F]),
|
|
kvant(Y,Y1,R,R1),
|
|
kvant(Z1,Z2,R1,L2),
|
|
kvant(all(X,(Y1#Z2)),SY,L2,L3));
|
|
(kvant(Y,Y1,R,R1),
|
|
kvant(Z,Z2,R1,L2),
|
|
kvant(all(X,(Y1#Z2)),SY,L2,L3)).
|
|
|
|
|
|
/* ***************************** # ALL **************************** */
|
|
|
|
kvant(Z#all(X,Y),SY,[F|R],L3):-
|
|
(free_in(X,Z),
|
|
r_v(X,Z,Z1,[F]),
|
|
kvant(Y,Y1,R,R1),
|
|
kvant(Z1,Z2,R1,L2),
|
|
kvant(all(X,(Z2#Y1)),SY,L2,L3));
|
|
(kvant(Y,Y1,R,R1),
|
|
kvant(Z,Z2,R1,L2),
|
|
kvant(all(X,(Z2#Y1)),SY,L2,L3)).
|
|
|
|
|
|
/* *************************** EXIST & ************************** */
|
|
|
|
kvant(exist(X,Y)&Z,SY,[F|R],L3):-
|
|
(free_in(X,Z),
|
|
r_v(X,Z,Z1,[F]),
|
|
kvant(Y,Y1,R,R1),
|
|
kvant(Z1,Z2,R1,L2),
|
|
kvant(exist(X,(Y1&Z2)),SY,L2,L3));
|
|
(kvant(Y,Y1,R,R1),
|
|
kvant(Z,Z2,R1,L2),
|
|
kvant(exist(X,(Y1&Z2)),SY,L2,L3)).
|
|
|
|
/* *************************** & EXIST ************************** */
|
|
|
|
kvant(Z&exist(X,Y),SY,[F|R],L3):-
|
|
(free_in(X,Z),
|
|
r_v(X,Z,Z1,[F]),
|
|
kvant(Y,Y1,R,R1),
|
|
kvant(Z1,Z2,R1,L2),
|
|
kvant(exist(X,(Z2&Y1)),SY,L2,L3));
|
|
(kvant(Y,Y1,R,R1),
|
|
kvant(Z,Z2,R1,L2),
|
|
kvant(exist(X,(Z2&Y1)),SY,L2,L3)).
|
|
|
|
/* *************************** EXIST # ************************** */
|
|
|
|
kvant(exist(X,Y)#Z,SY,[F|R],L3):-
|
|
(free_in(X,Z),
|
|
r_v(X,Z,Z1,[F]),
|
|
kvant(Y,Y1,R,R1),
|
|
kvant(Z1,Z2,R1,L2),
|
|
kvant(exist(X,(Y1#Z2)),SY,L2,L3));
|
|
(kvant(Y,Y1,R,R1),
|
|
kvant(Z,Z2,R1,L2),
|
|
kvant(exist(X,(Y1#Z2)),SY,L2,L3)).
|
|
|
|
/* *************************** # EXIST ************************** */
|
|
|
|
kvant(Z#exist(X,Y),SY,[F|R],L3):-
|
|
(free_in(X,Z),
|
|
r_v(X,Z,Z1,[F]),
|
|
kvant(Y,Y1,R,R1),
|
|
kvant(Z1,Z2,R1,L2),
|
|
kvant(exist(X,(Z2#Y1)),SY,L2,L3));
|
|
(kvant(Y,Y1,R,R1),
|
|
kvant(Z,Z2,R1,L2),
|
|
kvant(exist(X,(Z2#Y1)),SY,L2,L3)).
|
|
|
|
|
|
|
|
/* *************************** & ************************** */
|
|
|
|
kvant(P&Q,PQ,L,L3):-
|
|
kvant(P,P1,L,L1),
|
|
kvant(Q,Q1,L1,L2),
|
|
((P1\==P);(Q1\==Q)),
|
|
kvant(P1&Q1,PQ,L2,L3).
|
|
|
|
/* *************************** # ************************** */
|
|
|
|
kvant(P#Q,PQ,L,L3):-
|
|
kvant(P,P1,L,L1),
|
|
kvant(Q,Q1,L1,L2),
|
|
((P1\==P);(Q1\==Q)),
|
|
kvant(P1#Q1,PQ,L2,L3).
|
|
|
|
/* *************************** EXIST ************************** */
|
|
|
|
kvant(all(X,F),all(X,F1),L1,L2):-
|
|
kvant(F,F1,L1,L2).
|
|
|
|
/* *************************** ALL ************************** */
|
|
|
|
kvant(exist(X,F),exist(X,F1),L1,L2):-
|
|
kvant(F,F1,L1,L2).
|
|
|
|
/* *************************** BASFALL ************************** */
|
|
|
|
kvant(X,X,L,L).
|