% rminer.pl (a derivative from metric01b.pl)
% the rule mining for social choice
% date: 2007.7.11
% revised: 2007.7.16

:- [sged06]. % cumulative load
:- chdom(_->l:L), nl,write('default domain':L),nl,nl.
:- make_n_agents(3).

% naive rule mining for social choice logic programming (SCLP)

rule_miner(A,B):-
   formulate_hypothesis(A->B,C),
   \+ gen_win(_,C).

:- dynamic rm/1.

minimal_rule_miner(A,B):-
   \+ clause(rm(_),true),
   rule_miner(A,B),
   \+ (
     rule_miner(C,D),(C,D)\=(A,B),
     subset(C,A),subset(D,B)
   ).

minimal_rule_miner(A,B):-
   \+ \+ clause(rm(_),true),
   rm(A->B),
   \+ (
     rm(C->D),(C,D)\=(A,B),
     subset(C,A),subset(D,B)
   ).

formulate_hypothesis(Y->Z,O):-
   axioms_for_win(X),
   formulate_hypothesis(X,Y->Z,O).

formulate_hypothesis([],[]->[],[]).
formulate_hypothesis([A:_|X],[A|B]->C,[A:yes|D]):-
   formulate_hypothesis(X,B->C,D).
formulate_hypothesis([A:_|X],B->[A|C],[A:no(_)|D]):-
   formulate_hypothesis(X,B->C,D).
formulate_hypothesis([_|X],B->C,D):-
   formulate_hypothesis(X,B->C,D).

gen_rm:- C=rm(A->B),
   forall(rule_miner(A,B),
    (clause(C,_)->true;assert(C))
   ),
   nl,write('save the rm/1 results to file? (y/n)'),
   read(Y),
   (member(Y,[y,'Y'])->tell_rm;true).

tell_rm:- C=rm(_), tell_goal('rm.pl',forall,C).

mr(A->B):-
   \+ \+ clause(rm(_),true),
   minimal_rule_miner(A,B).

/*

?- minimal_rule_miner(A,B).

A = [monotonic]
B = [proper, strong] 

Yes
?- gen_rm.

save the rm/1 results to file? (y/n)y.
complete

Yes
?- mr(C->D),nl,write(C->D),fail.

[monotonic]->[proper, strong]
[monotonic, not weak]->[strong]
[strong]->[monotonic, not weak]
[]->[monotonic, essential]
[]->[proper, not weak]
[]->[proper, essential]
[strong, essential]->[not weak]
[]->[strong, essential]
[not weak]->[essential]

No
?- rule_miner([monotonic,proper,strong|A],B).

A = ['not weak']
B = [essential] ;

A = [essential]
B = ['not weak'] ;

No
?- rule_miner([proper,strong|A],B),nl,write(A->B),fail.

[not weak]->[monotonic, essential]
[essential]->[monotonic, not weak]
[]->[monotonic, not weak, essential]
[]->[monotonic, not weak]
[]->[monotonic, essential]
[not weak]->[essential]
[essential]->[not weak]

No
?-
*/

% end