:-op(100,fy,not). :-op(110,yfx,&). :-op(120,yfx,v). :-op(900,yfx,/=). :- dynamic numatoms/1, theatom/2, option/2. numatoms(0). numrows(0). option(avoid_neg_head,on). option(verbose,off). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Countermodels I /= (F,G) :- !, I /= F & G. I /= (F;G) :- !, I /= F v G. I /= (G :- F) :- !, I /= (F -> G). I /= (not F) :- !, I /= (F -> false). _I /= true :- !. _I /= false :- !,fail. [H|_] /= A :- number(A),!,holds(A,H). I /= F & G :- I /= F, I /= G. I /= F v G :- I /= F,!; I /= G. [T] /= (F -> G) :- [T] /= G,!; \+ ([T] /= F). [H,T] /= (F -> G) :- [T] /= (F -> G), ([H,T] /= G,!; \+ ([H,T] /= F)). countermodel(I,T) :- member(F,T), \+ (I /= F),!. countermodels(G,Is):- all_true_interp(Z), findall(T,get_subset(Z,T),Ts), all_t_countermodels(Ts,G,[],Is). all_t_countermodels([],_,Is,Is):-!. all_t_countermodels([T|Ts],G,Is0,Is):- t_countermodels(T,G,Is1), append(Is0,Is1,Is2), all_t_countermodels(Ts,G,Is2,Is). % Gets all countermodels [H,T] fixing T t_countermodels(T,G,Is):- countermodel([T],G),!, findall([H,T],get_subset(T,H),Is) ; findall([H,T],(get_subset(T,H),H \= T,countermodel([H,T],G)),Is). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Extracting the propositional signature set_atoms(true,true):-!. set_atoms(false,false):-!. set_atoms([],[]):-!. set_atoms(T,T2):- T =.. [F|Args], ( member(F,[&,v,->,-,not,(,),(;),(:-),(.)]),!, set_atoms_args(Args,Args2),T2 =.. [F|Args2] ; theatom(I,T),!,T2=I ; numatoms(N),retract(numatoms(_)),N1 is N+1,assertz(numatoms(N1)), assertz(theatom(N,T)),T2=N ). set_atoms_args([],[]):-!. set_atoms_args([F|Fs],[G|Gs]):- set_atoms(F,G),set_atoms_args(Fs,Gs). set_signature(L):- (retractall(numatoms(_)),!;true), (retractall(theatom(_,_)),!;true), asserta(numatoms(0)), set_atoms(L,_). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% rebuild(T,P):- (retractall(numatoms(_)),!;true), (retractall(theatom(_,_)),!;true), asserta(numatoms(0)), set_atoms(T,T2), (option(verbose,on),!,write('Computing countermodels...'),nl; true), countermodels(T2,CMs), maplist(to_3valued,CMs,CMs2), minprogram(CMs2,P). minimise_program(T,P):- (retractall(numatoms(_)),!;true), (retractall(theatom(_,_)),!;true), asserta(numatoms(0)), set_atoms(T,T2), (option(verbose,on),!,write('Computing countermodels...'),nl; true), get_program_cms(T2,CMs0), t_closure(CMs0,CMs), minprogram(CMs,P). :- dynamic cm/3, numcms/1, implicate/5, implic/3, numimplicates/1, i/1. :- dynamic chart/2. % implicate(IdCode,NumOfOnes,Labelling,Weight,PrimeMark) minprogram(CMs,Rs):- initialize(CMs), findall(r(N,X),implicate(X,N,_,_,_),As), sort(As,Bs), classify(Bs,S0), (option(verbose,on),!,write('Obtaining prime implicates...'),nl;true), prime_implicates(S0), (option(avoid_neg_head,on),!,remove_neg_heads; true), (option(verbose,on),!,write('Getting minimal coverings...'),nl;true), get_implicate_countermodels, build_chart, filter_essential(Es), findall(M,chart(M,_),Ms0),sort(Ms0,Ms), % get the uncovered countermodels ( Ms=[],!,Ts=Es % all countermodels were covered: Petrick's method unneeded ; findall(Y,chart(_,Y),Ys0),sort(Ys0,Ys), % get the non-essential implicates findall(Ns,(member(W,Ys),findall(N,chart(N,W),Ns)),NsList), petrick(Ms,NsList,Vs), member(V,Vs), % pick one list among the obtained with Petrick's method findall(Q,(member(J,V),nth0(J,Ys,Q)),Qs), append(Es,Qs,Ts) ), build_rules(Ts,Rs). initialize(CMs):- (retractall(cm(_,_,_)),!; true), (retractall(numcms(_)),!; true), (retractall(implicate(_,_,_,_,_)),!; true), (retractall(numimplicates(_)),!; true), (retractall(implic(_,_,_)),!; true), (retractall(i(_)),!; true), (retractall(chart(_,_)),!; true), asserta(numcms(0)), asserta(i(0)), repeat, ( member(X,CMs), numcms(N), assertz(cm(N,X,[])), count(1,X,Ones), assertz(implicate(N,Ones,X,0,prime)), retractall(numcms(_)), N1 is N+1, asserta(numcms(N1)), fail ; true ),!,numcms(M),asserta(numimplicates(M)), compute_submodels. compute_submodels:- repeat, ( cm(X,Rx,[]),compute_submodels(X,Rx),fail ; true ),!. compute_submodels(X,Rx):- ( is_total(Rx),!,findall(Y,(submodel(Rx,M),cm(Y,M,_)),Ys), sort(Ys,Ws),Zs=Ws ; Zs=[X] ), retract(cm(X,Rx,_)),asserta(cm(X,Rx,Zs)). classify([],[]):-!. classify([r(N,X)],[r(N,[X])]):-!. classify([r(N,X)|Rs],Es):- classify(Rs,Cs),Cs=[r(M,Ys)|Ds], (N=M,!,Es=[r(M,[X|Ys])|Ds] ;Es=[r(N,[X]),r(M,Ys)|Ds] ). prime_implicates([]):-!. prime_implicates(S):- i(I),I1 is I+1, (option(verbose,on),!,write(I),write(' ************'),nl,write_classes(S);true), match_consec_classes(S), match_intra_classes(S), findall(r(N,X),implicate(X,N,_,I1,_),As), sort(As,Bs), classify(Bs,S1), retractall(i(_)),asserta(i(I1)), % remove previous nonprime implicates I0 is I-1, (retractall(implicate(_,_,_,I0,nonprime)),!;true), prime_implicates(S1). match_consec_classes([]):-!. match_consec_classes([_]):-!. match_consec_classes([r(N,Xs),r(M,Ys)|Cs]):- N1 is N+1, M=N1,!, match_pairs(a,N,Xs,Ys), match_consec_classes([r(M,Ys)|Cs]). match_consec_classes([_,r(M,Ys)|Cs]):-match_consec_classes([r(M,Ys)|Cs]). match_pairs(Type,N,Xs,Ys):- i(I),I1 is I+1, repeat, ( member(X,Xs), member(Y,Ys), implicate(X,_,Rx,I,_),implicate(Y,_,Ry,I,_), adj(Type,Rx,Ry,Rz,Pre,Suf), insert_newimp(N,Rz,I1), mark_nonprime(Type,X,Y,Pre,Suf), fail ; true),!. insert_newimp(N,R,I):-implicate(_,N,R,I,_),!. insert_newimp(N,R,I):-numimplicates(M),retractall(numimplicates(_)), assertz(implicate(M,N,R,I,prime)), M1 is M+1, asserta(numimplicates(M1)). % if matching of type a, Y has more ones mark_nonprime(a,_X,Y,_Pre,_Suf):- mark_implicate_num(Y). mark_nonprime(b,X,Y,Pre,Suf):- mark_implicate_num(X),mark_implicate_num(Y), append(Pre,[0|Suf],A),append(Pre,[2|Suf],B), mark_implicate(A),mark_implicate(B). mark_implicate_num(X):-implicate(X,Nx,Rx,I,prime),!, retract(implicate(X,Nx,Rx,I,prime)),assert(implicate(X,Nx,Rx,I,nonprime)). mark_implicate_num(_). mark_implicate(Rx):-implicate(X,Nx,Rx,I,prime),!, retract(implicate(X,Nx,Rx,I,prime)),assert(implicate(X,Nx,Rx,I,nonprime)). mark_implicate(_). match_intra_classes([]):-!. match_intra_classes([r(N,Xs)|Cs]):- match_all(N,Xs), match_intra_classes(Cs). match_all(_,[]):-!. match_all(N,[X|Xs]):-match_pairs(b,N,[X],Xs),match_all(N,Xs). test([(p->q)->r]). test2([(not p->q)->p]). test3([(r -> not p v s), (p -> q v not r)]). test4([(not p -> q) -> not r;p]). % adj(Type,implicate1,implicate2,resulting_implicate,preffix,suffix) adj(_,[],[],[],[],[]):-!. adj(Type,[X|Xs],[X|Ys],[X|Zs],[X|Pre],Suf):-!,adj(Type,Xs,Ys,Zs,Pre,Suf). adj(Type,[X|Xs],[Y|Xs],[Z|Xs],[],Xs):-adj_val(Type,X,Y,Z),!. adj_val(a,0,1,n). adj_val(a,1,0,n). adj_val(a,1,2,p). adj_val(a,2,1,p). adj_val(b,n,p,-). adj_val(b,p,n,-). write_classes([]):-!. write_classes([r(_N,Xs)|Cs]):-write_implicates(Xs),write_classes(Cs). write_implicates([]):-!. write_implicates([X|Xs]):- implicate(X,_,Rx,_,_),concat_atom(Rx,A),write(A),nl,write_implicates(Xs). get_cms(L,S):- findall(Xs,(get_cm(L,M),cm(_,M,Xs)),S0), appendall(S0,S1),sort(S1,S). appendall([],[]). appendall([X|Xs],Z):-appendall(Xs,Y),append(X,Y,Z). is_total([]):-!. is_total([X|Xs]):-X=0,!,is_total(Xs); X=2,is_total(Xs). submodel([],[]):-!. submodel([0|Xs],[0|Ys]):-!,submodel(Xs,Ys). submodel([2|Xs],[Y|Ys]):-(Y=2;Y=1),submodel(Xs,Ys). get_cm([],[]). get_cm([X|Xs],[V|Ys]):-label_values(X,Vs),member(V,Vs),get_cm(Xs,Ys). label_values(0,[0]). label_values(1,[1]). label_values(2,[2]). label_values(n,[0,1]). label_values(p,[1,2]). label_values(-,[0,1,2]). t_closure([],[]):-!. t_closure([M|Ms],S):- is_total(M),!,findall(P,submodel(M,P),Ps),sort(Ps,Ps1), t_closure(Ms,Qs),merge_set(Ps1,Qs,S). t_closure([M|Ms],S):- t_closure(Ms,Qs),merge_set([M],Qs,S). remove_neg_heads:- repeat, ( implicate(X,Nx,Rx,I,prime), has_neg_head(Rx), retract(implicate(X,Nx,Rx,I,prime)), fail ; true),!. has_neg_head(Rx):- member(p,Rx), % it has some 'not p' in the head \+ member(1,Rx), \+ member(n,Rx). % but doesn't have positive lit's in the head get_implicate_countermodels:- repeat, ( implicate(X,Nx,Rx,I,prime), get_cms(Rx,CMs), retract(implicate(X,Nx,Rx,I,prime)), assertz(implic(X,Rx,CMs)), fail ; true),!. build_chart:- repeat, ( implic(X,_Rx,CMs), member(M,CMs), asserta(chart(M,X)), fail ; true),!. filter_essential(Es):- findall(X,(chart(M,X),is_essential(M,X)),Es0),sort(Es0,Es), remove_covered(Es). remove_covered([]):-!. remove_covered([X|Xs]):- % remove all countermodels covered by X findall(M,chart(M,X),Ms), repeat, ( member(A,Ms), retractall(chart(A,_)), fail ; true),!, remove_covered(Xs). is_essential(M,X):-chart(M,Y),Y \= X,!,fail. is_essential(_,_). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Building the rules from a set of implicates build_rules([],[]):-!. build_rules([X|Xs],[R|Rs]):- numatoms(N), implic(X,Rx,_), build_rule(N,Rx,([] :- []),(H :- B)), commas(B,B1),semis(H,H1), (H1=false,!, (B1=true,!,R=false ;B1=false,!,R=true ;R=(:-B1) ) ;B1=true,!,R=(H1) ;R=(H1 :- B1) ), build_rules(Xs,Rs). commas(L,E):-rbinop((,),true,L,E). semis(L,E):-rbinop((;),false,L,E). build_rule(_,[],R,R):-!. build_rule(N,[V|Vs],R0,R):- N1 is N-1, theatom(N1,P),add_atom(P,V,R0,R1),build_rule(N1,Vs,R1,R). add_atom(_P,-,R,R):-!. add_atom(P,n,(H :- B),([P|H] :- B)):-!. add_atom(P,p,(H :- B),([not P|H] :- B)):-!. add_atom(P,1,(H :- B),([P,not P|H] :- B)):-!. add_atom(P,2,(H :- B),(H :- [P|B])):-!. add_atom(P,0,(H :- B),(H :- [not P|B])):-!. % rbinop(F,Neut,Xs,E). rbinop(_F,Neut,[],Neut):-!. rbinop(_F,_Neut,[X],X):-!. rbinop(F,Neut,[X|Xs],E):-rbinop(F,Neut,Xs,E0),E =.. [F,X,E0]. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% :-dynamic prog_num/1. main:- option(verbose,off), set_signature([p,q]),tell('162.txt'), asserta(prog_num(1)), repeat, (generate_countermodels(CMs), prog_num(N),retract(prog_num(_)),N1 is N+1,asserta(prog_num(N1)), maplist(to_3valued,CMs,CMs2), write('--- P'),write(N),write(' ---'),nl, write_min_programs(CMs2),nl, fail ; true),!,told. % write_min_programs(CMs):- % minprogram(CMs,P),!,write_program(P). write_min_programs(CMs):- findall(P,minprogram(CMs,P),Ps),write_min_progs(Ps). write_min_progs([X]):-!,write_program(X). write_min_progs([X|Xs]):- write_program(X),nl,write('other choice:'),nl,nl, write_min_progs(Xs). generate_countermodels(CMs):- all_true_interp(Z), findall(Y,get_subset(Z,Y),Ys), generate_countermodels(Ys,[],CMs). generate_countermodels([],CMs,CMs). generate_countermodels([Y|Ys],CMs0,CMs):- findall([X,Y],get_subset(Y,X),CMs1), ( append(CMs0,CMs1,CMs2) % option 1, include [Y,Y] and all [X,Y]'s ; extract([Y,Y],CMs1,CMs1b), % otherwise, take any possibility but [Y,Y] sublist(CMs1b,CMs1c), append(CMs0,CMs1c,CMs2) ), generate_countermodels(Ys,CMs2,CMs). sublist([],[]). sublist([_|Xs],Ys):-sublist(Xs,Ys). sublist([X|Xs],[X|Ys]):-sublist(Xs,Ys). write_program(Rs):-member(R,Rs),write(R),write('.'),nl,fail;true. extract(X,L,L2):-append(Pre,[X|Suf],L),append(Pre,Suf,L2). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% get_program_cms([],[]):-!. get_program_cms([R|Rs],CMs):- rule_cms(R,CMs1), get_program_cms(Rs,CMs2), append(CMs1,CMs2,CMs3),sort(CMs3,CMs). rule_cms(R,CMs):- transform_rule(R,Hp,Hn,Bp,Bn), % gets rid of tautologies ( intersection(Bp,Bn,A1),A1 \= [],!, CMs=[] ; intersection(Hp,Bp,A2),A2 \= [],!, CMs=[] ; intersection(Hn,Bn,A3),A3 \= [],!, CMs=[] ; % If it's not a tautology, remove redundant info subtract(Hp,Bn,Hp1), subtract(Hn,Bp,Hn1), get_labelling(Hp1,Hn1,Bp,Bn,L), findall(M,get_cm(L,M),CMs) ). transform_rule((H :- B),Hp,Hn,Bp,Bn):-!, transform_head(H,Hp,Hn),transform_body(B,Bp,Bn). transform_rule((:- B),[],[],Bp,Bn):-!,transform_body(B,Bp,Bn). transform_rule(H,Hp,Hn,[],[]):-!,transform_head(H,Hp,Hn). transform_head(H,Hp,Hn):-transform_binop((;),H,Hp0,Hn0),sort(Hp0,Hp),sort(Hn0,Hn). transform_body(B,Bp,Bn):-transform_binop((,),B,Bp0,Bn0),sort(Bp0,Bp),sort(Bn0,Bn). transform_binop(F,E,Ep,En):- E =.. [F,Lit,E1],!, transform_binop(F,E1,Ep0,En0), ( Lit = (not P),!,Ep=Ep0,En=[P|En0] ; Ep=[Lit|Ep0],En=En0 ). transform_binop(_F,not P,[],[P]):-!. transform_binop(_F,P,[P],[]). get_labelling(Hp,Hn,Bp,Bn,Rx):-numatoms(N),get_labelling(N,Hp,Hn,Bp,Bn,Rx). get_labelling(0,_Hp,_Hn,_Bp,_Bn,[]):- !. get_labelling(N,Hp,Hn,Bp,Bn,[V|L]):- P is N-1, ( member(P,Hp),!, (member(P,Hn),!,V=1 ; V=n ) ; member(P,Hn),!, V=p ; member(P,Bp),!, V=2 ; member(P,Bn),!, V=0 ; V=(-) ), get_labelling(P,Hp,Hn,Bp,Bn,L). %%%%%%%%%%%%% set_option(OP,VAL):- (retractall(option(OP,_)),!;true), asserta(option(OP,VAL)). :-write('Type help(minlp) for instructions on use.'),nl. help(minlp):- write('rebuild(T,P) gets a minimal program P strongly equivalent to an arbitary'),nl, write(' theory T. This theory is a list of formulas using operators:'),nl, write(' , & for conjunction'),nl, write(' ; v for disjunction'),nl, write(' not for (default) negation'),nl, write(' -> for implication left to right'),nl, write(' :- for implication right to left'),nl, write(' Example:'),nl, write(' ?- rebuild([(p->q)->r],P),write_program(P).'),nl, nl, write('write_program(P) writes a program.'),nl, nl, write('minimise_program(T,P)'),nl, write(' works like rebuild but T is restricted to a set of logic'),nl, write(' program rules only allowing the the operators below:'),nl, write(' , ; :- not'),nl, write(' Example:'),nl, write(' ?- minimise_program([(p;q :- not p),(q; not q)],P).'),nl, nl, write('set_option(OP,VAL) sets an option OP to value VAL where:'),nl, write(' OP=verbose sets verbose mode. VAL can be on or off.'),nl, write(' OP=avoid_neg_head when VAL=on, implicates without positive'),nl, write(' head literals are ruled out in favour of'),nl, write(' constraints.'),nl, true. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Petrick's method ex2(Sol):- petrick([0,1,2,5,6,7], [[0,1], [0,2], [1,5], [2,6], [5,7], [6,7]], Sol). ex3(Sol):- petrick([9,12,13,15], [[9,13], [12,13], [9,12,13], [13,15], [9,13,15], [12,13,15]], Sol). ex4(P):- petrick([0,1,2,3], [[0,2,3], [1,2], [0,1], [2,3] ],P). petrick(Is,Rs,P4):- get_p_funct(Is,Rs,P0), findall(T,expand(P0,T),P1), sort_by_length(P1,[],P2), remove_supersets(P2,P3), P3=[L|_],length(L,N),sublist(has_length(N),P3,P4). has_length(N,L):-length(L,N). get_p_funct([],_,[]):-!. get_p_funct([I|Is],Rs,Es):- length(Rs,N), row_nums(N,I,Rs,E0), sort(E0,E), get_p_funct(Is,Rs,Es0), add_term(Es0,E,Es). row_nums(0,_I,_Rs,[]):-!. row_nums(N,I,Rs,Es):- M is N-1, row_nums(M,I,Rs,Es0), nth0(M,Rs,NRowIs), (member(I,NRowIs),!,Es=[M|Es0] ;Es=Es0). expand([],[]). expand([L|Ls],Xs):-member(X,L),expand(Ls,Xs0),merge_set([X],Xs0,Xs). sort_by_length([],Ms,Ms):-!. sort_by_length([L|Ls],Ms,Ns):- insert_by_length(L,Ms,Ms1),sort_by_length(Ls,Ms1,Ns). insert_by_length(L,[],[L]):-!. insert_by_length(L1,[L2|Ls],Ms):- length(L1,N1),length(L2,N2), (N1> 1), get_subset_elem(Mask2,X1,Y). all_true_interp(I):-nbits(B),numatoms(N),all_true_interp(N,B,I). all_true_interp(N,B,[X]):-N