% metric_rm.pl
% Comparison of the Dodgson metric and the Kemeny metric,
% and rule mining for coevoluting individual preferences 
% and power distribution
% date: 2007.6.30-7.2,4-6
% revised: 2007.8.25 (a branch from metric01b.pl)
% revised: 2008.5.2 (preliminary file import)

% reference
% Gaertner, W. (2006). 
% A Primer in Social Choice Theory, Oxford Univrsity Press.


% Comparative test for the two metrics
%--------------------------------------------------------------

% revised: 2008.5.2.
:- [metric_d].
%:- [metric_d,metric_k].

% predicate models from metric_dand metric_k

% distance(dodgeson(min,K,X),R->Q,H,Z)
% distance(kemeny(min,K),R->Q,H,Z).
% dodgeson_rule(RD,B,R)
% kemeny_distance(K1,U,Q,D)

test_compare(Q->d:(RD;B),k:(U;K)):-
   rr(Q),is_upper_diagonal(Q),
   dodgeson_rule(RD,B,Q),
   kemeny_distance(K,U,Q,_).

test_diff(A,Q->k:(U;K);d(DR)):-
   rr(Q),is_upper_diagonal(Q),
   \+ dodgeson_rule(_,_,Q),
   dodgeson_ranking_1(DR,Q),
   kemeny_distance(K,U,Q,_),
   name_domain(A,Q).

test_diff(A,Q->d:(RD;B)):-
   rr(Q),is_upper_diagonal(Q),
   dodgeson_rule(RD,B,Q),
   \+ kemeny_distance(_,_,Q,_),
   name_domain(A,Q).

test_pivotal_dodgeson(A,Q->d:R,B/W):-
   rr(Q),%is_upper_diagonal(Q),
   dodgeson_ranking_1(R,Q),best(B,R),
   majority(Q->M),best(W,M),
   name_domain(A,Q).

/*
?- test_compare(Q->d:(RD;B),k:(U;K)).

Q = [[+, +, +], [+, +, +], [+, +, +]]
RD = [+, +, +]
B = [a>b, a>c, b>c]
U = [+, +, +]
K = 0 

Yes
?- test_compare(Q->d:(RD;B),k:(U;K)),RD\=U.

No
?- test_diff(A,B),nl,write(A;B),fail.

TTC;[[+, +, -], [+, +, -], [-, +, +]]->k: ([+, +, -];2);d([+, +, 0])
AII;[[+, +, +], [-, -, +], [-, -, +]]->k: ([-, -, +];2);d([-, 0, +])
AZI;[[+, +, +], [+, -, -], [-, -, +]]->k: ([+, +, +];4);d([0, 0, 0])
ZZI;[[+, -, -], [+, -, -], [-, -, +]]->k: ([+, -, -];2);d([0, -, -])
AAZ;[[+, +, +], [+, +, +], [+, -, -]]->k: ([+, +, +];2);d([+, +, 0])
CCN;[[-, +, +], [-, +, +], [-, -, -]]->k: ([-, +, +];2);d([-, 0, +])
TCN;[[+, +, -], [-, +, +], [-, -, -]]->k: ([+, +, -];4);d([0, 0, 0])
TNN;[[+, +, -], [-, -, -], [-, -, -]]->k: ([-, -, -];2);d([0, -, -])

No
?- test_pivotal_dodgeson(A,QR,B/W),B\=W,nl,write(A;QR;B/W),fail.

No
?- 
*/

tell_dodgeson:-
   tell_goal('dodgeson_test1.txt',(
     test_dodgeson(_,_),fail;true
   )).

tell_kemeny:-
   tell_goal('kemeny_test1.txt',(
     test_kemeny(_,_),fail;true
   )).

test_dodgeson(Q->RD,B):-
   rr(Q),is_upper_diagonal(Q),
   test_dodgeson_1(Q->RD,B).

test_dodgeson_1(Q->RD,B):-
   dodgeson_rule(RD,B,Q),
   nl,write(dodgeson(Q->RD,B)),
   !.

test_dodgeson_1(Q->_,_):-
   nl,write(anormal:Q).

test_kemeny(Q->U,K):-
   rr(Q),is_upper_diagonal(Q),
   test_kemeny_1(Q->U,K),
   test_kemeny_2(Q->U,K).

test_kemeny_1(Q->U,K):-
   distance(kemeny(min,K),R->Q,_,_),
   sort(R,[U]),nl,write(1:Q->U;K),
   !.
test_kemeny_1(Q->_,_):-
   nl,write(anormal:Q).

test_kemeny_2(Q->U,K):-
   kemeny_distance(K,U,Q,_),
   nl,write(2:Q->U;K),
   !.
test_kemeny_2(Q->_,_):-
   nl,write(anormal:Q).

% making experimental data (1)

/*
?- gen_win(G,[monotonic:yes]),\+ \+ (
test_pivotal_dodgeson(A,QR,B/W),B\=W,
nl,write(coevo(G;A;B/W)),write('.')
),fail.
*/

coevo(([[1, 2, 3], [1, 2], [1, 3], [1], [2, 3], [2]];'IAA';b/a)).
coevo(([[1, 2, 3], [1, 2], [1, 3], [1], [2, 3], [3]];'IAA';b/a)).
coevo(([[1, 2, 3], [1, 2], [1, 3], [1], [2, 3]];'IAA';b/a)).
coevo(([[1, 2, 3], [1, 2], [1, 3], [1]];'CAA';b/a)).
coevo(([[1, 2, 3], [1, 2], [1, 3], [2, 3], [2], [3]];'AIA';b/a)).
coevo(([[1, 2, 3], [1, 2], [1, 3], [2, 3], [2]];'AIA';b/a)).
coevo(([[1, 2, 3], [1, 2], [1, 3], [2, 3], [3]];'ZZA';a/c)).
coevo(([[1, 2, 3], [1, 2], [2, 3], [2]];'ACA';b/a)).
coevo(([[1, 2, 3], [1, 3], [2, 3], [3]];'CCA';a/b)).

/*
No
?- coevo(G;A;B),gen_win(G),verify_win,nl,fail.

game:[[1, 2, 3], [1, 2], [1, 3], [1], [2, 3], [2]]
 + :[monotonic, strong, not weak, essential]
 - :[improper:[1, 3]]

game:[[1, 2, 3], [1, 2], [1, 3], [1], [2, 3], [3]]
 + :[monotonic, strong, not weak, essential]
 - :[improper:[1, 2]]

game:[[1, 2, 3], [1, 2], [1, 3], [1], [2, 3]]
 + :[monotonic, strong, not weak, essential]
 - :[improper:[1]]

game:[[1, 2, 3], [1, 2], [1, 3], [1]]
 + :[monotonic, proper, strong]
 - :[weak(vetoers):[1], inessential(dictator):1]

game:[[1, 2, 3], [1, 2], [1, 3], [2, 3], [2], [3]]
 + :[monotonic, strong, not weak, essential]
 - :[improper:[1, 2]]

game:[[1, 2, 3], [1, 2], [1, 3], [2, 3], [2]]
 + :[monotonic, strong, not weak, essential]
 - :[improper:[1, 3]]

game:[[1, 2, 3], [1, 2], [1, 3], [2, 3], [3]]
 + :[monotonic, strong, not weak, essential]
 - :[improper:[1, 2]]

game:[[1, 2, 3], [1, 2], [2, 3], [2]]
 + :[monotonic, proper, strong]
 - :[weak(vetoers):[2], inessential(dictator):2]

game:[[1, 2, 3], [1, 3], [2, 3], [3]]
 + :[monotonic, proper, strong]
 - :[weak(vetoers):[3], inessential(dictator):3]

No
?- gen_win(G,[monotonic:yes]),\+ coevo(G;_),nl,write(G),fail.

[[1, 2, 3], [1, 2], [1, 3], [1], [2, 3], [2], [3]]
[[1, 2, 3], [1, 2], [1, 3], [2, 3]]
[[1, 2, 3], [1, 2], [1, 3]]
[[1, 2, 3], [1, 2], [2, 3]]
[[1, 2, 3], [1, 2]]
[[1, 2, 3], [1, 3], [2, 3]]
[[1, 2, 3], [1, 3]]
[[1, 2, 3], [2, 3]]
[[1, 2, 3]]

No
?- gen_win(G,[monotonic:yes]),\+ coevo(G;_),verify_win,nl,fail.

game:[[1, 2, 3], [1, 2], [1, 3], [1], [2, 3], [2], [3]]
 + :[monotonic, strong, not weak, essential]
 - :[improper:[1, 2]]

game:[[1, 2, 3], [1, 2], [1, 3], [2, 3]]
 + :[monotonic, proper, strong, not weak, essential]
 - :[]

game:[[1, 2, 3], [1, 2], [1, 3]]
 + :[monotonic, proper, essential]
 - :[not strong:[1], weak(vetoers):[1]]

game:[[1, 2, 3], [1, 2], [2, 3]]
 + :[monotonic, proper, essential]
 - :[not strong:[1, 3], weak(vetoers):[2]]

game:[[1, 2, 3], [1, 2]]
 + :[monotonic, proper, essential]
 - :[not strong:[1, 3], weak(vetoers):[1, 2]]

game:[[1, 2, 3], [1, 3], [2, 3]]
 + :[monotonic, proper, essential]
 - :[not strong:[1, 2], weak(vetoers):[3]]

game:[[1, 2, 3], [1, 3]]
 + :[monotonic, proper, essential]
 - :[not strong:[1, 2], weak(vetoers):[1, 3]]

game:[[1, 2, 3], [2, 3]]
 + :[monotonic, proper, essential]
 - :[not strong:[1, 2], weak(vetoers):[2, 3]]

game:[[1, 2, 3]]
 + :[monotonic, proper, essential]
 - :[not strong:[1, 2], weak(vetoers):[1, 2, 3]]

No
?-
*/

% 

/*
?- coevo(G;A;B/W),gen_win(G),verify_win,name_domain(A,R),
majority(R->M),best(W,M),nl,write(m:W;R->M),
forall(distance(dodgson(min,K,X),R->Q,H,Z),(nl,write(K:X;Q;Z))),nl,fail.

game:[[1, 2, 3], [1, 2], [1, 3], [1], [2, 3], [2]]
 + :[monotonic, strong, not weak, essential]
 - :[improper:[1, 3]]
m:a;[[-, -, +], [+, +, +], [+, +, +]]->[+, +, +]
2:a;[[+, +, +], [+, +, +], [+, +, +]];[[a], [], []]
1:b;[[-, -, +], [-, +, +], [+, +, +]];[[b], []]
3:c;[[-, -, -], [+, -, -], [+, +, +]];[[c], [], [], []]

game:[[1, 2, 3], [1, 2], [1, 3], [1], [2, 3], [3]]
 + :[monotonic, strong, not weak, essential]
 - :[improper:[1, 2]]
m:a;[[-, -, +], [+, +, +], [+, +, +]]->[+, +, +]
2:a;[[+, +, +], [+, +, +], [+, +, +]];[[a], [], []]
1:b;[[-, -, +], [+, +, +], [-, +, +]];[[b], []]
3:c;[[-, -, -], [+, +, +], [+, -, -]];[[c], [], [], []]

game:[[1, 2, 3], [1, 2], [1, 3], [1], [2, 3]]
 + :[monotonic, strong, not weak, essential]
 - :[improper:[1]]
m:a;[[-, -, +], [+, +, +], [+, +, +]]->[+, +, +]
2:a;[[+, +, +], [+, +, +], [+, +, +]];[[a], [], []]
1:b;[[-, -, +], [-, +, +], [+, +, +]];[[b], []]
3:c;[[-, -, -], [+, -, -], [+, +, +]];[[c], [], [], []]

game:[[1, 2, 3], [1, 2], [1, 3], [1]]
 + :[monotonic, proper, strong]
 - :[weak(vetoers):[1], inessential(dictator):1]
m:a;[[-, +, +], [+, +, +], [+, +, +]]->[+, +, +]
1:a;[[+, +, +], [+, +, +], [+, +, +]];[[a], [b]]
0:b;[[-, +, +], [+, +, +], [+, +, +]];[[b]]
2:c;[[-, -, -], [+, +, +], [+, +, +]];[[c], [b], [b]]

game:[[1, 2, 3], [1, 2], [1, 3], [2, 3], [2], [3]]
 + :[monotonic, strong, not weak, essential]
 - :[improper:[1, 2]]
m:a;[[+, +, +], [-, -, +], [+, +, +]]->[+, +, +]
2:a;[[+, +, +], [+, +, +], [+, +, +]];[[a], [], []]
1:b;[[+, +, +], [-, -, +], [-, +, +]];[[b], []]
3:c;[[+, +, +], [-, -, -], [+, -, -]];[[c], [], [], []]

game:[[1, 2, 3], [1, 2], [1, 3], [2, 3], [2]]
 + :[monotonic, strong, not weak, essential]
 - :[improper:[1, 3]]
m:a;[[+, +, +], [-, -, +], [+, +, +]]->[+, +, +]
2:a;[[+, +, +], [+, +, +], [+, +, +]];[[a], [], []]
1:b;[[-, +, +], [-, -, +], [+, +, +]];[[b], []]
3:c;[[+, -, -], [-, -, -], [+, +, +]];[[c], [], [], []]

game:[[1, 2, 3], [1, 2], [1, 3], [2, 3], [3]]
 + :[monotonic, strong, not weak, essential]
 - :[improper:[1, 2]]
m:c;[[+, -, -], [+, -, -], [+, +, +]]->[+, -, -]
1:a;[[+, +, -], [+, -, -], [+, +, +]];[[a], []]
3:b;[[-, -, +], [+, -, -], [-, +, +]];[[b], [], [], []]
2:c;[[+, -, -], [+, -, -], [+, -, -]];[[c], [], []]

game:[[1, 2, 3], [1, 2], [2, 3], [2]]
 + :[monotonic, proper, strong]
 - :[weak(vetoers):[2], inessential(dictator):2]
m:a;[[+, +, +], [-, +, +], [+, +, +]]->[+, +, +]
1:a;[[+, +, +], [+, +, +], [+, +, +]];[[a], [b]]
0:b;[[+, +, +], [-, +, +], [+, +, +]];[[b]]
2:c;[[+, +, +], [-, -, -], [+, +, +]];[[c], [b], [b]]

game:[[1, 2, 3], [1, 3], [2, 3], [3]]
 + :[monotonic, proper, strong]
 - :[weak(vetoers):[3], inessential(dictator):3]
m:b;[[-, +, +], [-, +, +], [+, +, +]]->[-, +, +]
0:a;[[-, +, +], [-, +, +], [+, +, +]];[[a]]
1:b;[[-, +, +], [-, +, +], [-, +, +]];[[b], [a]]
2:c;[[-, +, +], [-, +, +], [+, -, -]];[[c], [a], [a]]

No
?-

*/

% making experimental data (2)


/*
?- gen_win(G,[monotonic:no(_)]),\+ \+ (
test_pivotal_dodgson(A,QR,B/W),B\=W,
nl,write(coevo2(G;A;B/W)),write('.')
),fail.
*/


coevo2(([[1, 2, 3], [1, 2], [1, 3], [1], [2]];'IAA';b/a)).
coevo2(([[1, 2, 3], [1, 2], [1, 3], [1], [3]];'IAA';b/a)).
coevo2(([[1, 2, 3], [1, 2], [1, 3], [2], [3]];'AIA';b/a)).
coevo2(([[1, 2, 3], [1, 2], [1, 3], [2]];'AIA';b/a)).
coevo2(([[1, 2, 3], [1, 2], [1, 3], [3]];'ZZA';a/c)).
coevo2(([[1, 2, 3], [1, 2], [1], [2, 3], [2]];'IAA';b/a)).
coevo2(([[1, 2, 3], [1, 2], [1], [2, 3], [3]];'IAA';b/a)).
coevo2(([[1, 2, 3], [1, 2], [1], [2, 3]];'IAA';b/a)).
coevo2(([[1, 2, 3], [1, 2], [1], [2]];'IAA';b/a)).
coevo2(([[1, 2, 3], [1, 2], [1], [3]];'IAA';b/a)).
coevo2(([[1, 2, 3], [1, 2], [1]];'CAA';b/a)).
coevo2(([[1, 2, 3], [1, 2], [2, 3], [2], [3]];'AIA';b/a)).
coevo2(([[1, 2, 3], [1, 2], [2, 3], [3]];'ZZA';a/c)).
coevo2(([[1, 2, 3], [1, 2], [2], [3]];'AIA';b/a)).
coevo2(([[1, 2, 3], [1, 2], [2]];'ACA';b/a)).
coevo2(([[1, 2, 3], [1, 2], [3]];'ZZA';a/c)).
coevo2(([[1, 2, 3], [1, 3], [1], [2, 3], [2]];'IAA';b/a)).
coevo2(([[1, 2, 3], [1, 3], [1], [2, 3], [3]];'IAA';b/a)).
coevo2(([[1, 2, 3], [1, 3], [1], [2, 3]];'IAA';b/a)).
coevo2(([[1, 2, 3], [1, 3], [1], [2]];'IAA';b/a)).
coevo2(([[1, 2, 3], [1, 3], [1], [3]];'IAA';b/a)).
coevo2(([[1, 2, 3], [1, 3], [1]];'CAA';b/a)).
coevo2(([[1, 2, 3], [1, 3], [2, 3], [2], [3]];'AIA';b/a)).
coevo2(([[1, 2, 3], [1, 3], [2, 3], [2]];'AIA';b/a)).
coevo2(([[1, 2, 3], [1, 3], [2], [3]];'AIA';b/a)).
coevo2(([[1, 2, 3], [1, 3], [2]];'AIA';b/a)).
coevo2(([[1, 2, 3], [1, 3], [3]];'CCA';a/b)).
coevo2(([[1, 2, 3], [1], [2, 3], [2]];'IAA';b/a)).
coevo2(([[1, 2, 3], [1], [2, 3], [3]];'IAA';b/a)).
coevo2(([[1, 2, 3], [1], [2, 3]];'IAA';b/a)).
coevo2(([[1, 2, 3], [1], [2]];'IAA';b/a)).
coevo2(([[1, 2, 3], [1], [3]];'IAA';b/a)).
coevo2(([[1, 2, 3], [1]];'CAA';b/a)).
coevo2(([[1, 2, 3], [2, 3], [2], [3]];'AIA';b/a)).
coevo2(([[1, 2, 3], [2, 3], [2]];'ACA';b/a)).
coevo2(([[1, 2, 3], [2, 3], [3]];'CCA';a/b)).
coevo2(([[1, 2, 3], [2], [3]];'AIA';b/a)).
coevo2(([[1, 2, 3], [2]];'ACA';b/a)).
coevo2(([[1, 2, 3], [3]];'CCA';a/b)).
coevo2(([[1, 2], [1, 3], [1], [2, 3], [2]];'IAA';b/a)).
coevo2(([[1, 2], [1, 3], [1], [2, 3], [3]];'IAA';b/a)).
coevo2(([[1, 2], [1, 3], [1], [2]];'IAA';b/a)).
coevo2(([[1, 2], [1, 3], [1], [3]];'IAA';b/a)).
coevo2(([[1, 2], [1, 3], [1]];'CAA';b/a)).
coevo2(([[1, 2], [1, 3], [2, 3], [2], [3]];'AIA';b/a)).
coevo2(([[1, 2], [1, 3], [2, 3], [2]];'AIA';b/a)).
coevo2(([[1, 2], [1, 3], [2, 3], [3]];'ZZA';a/c)).
coevo2(([[1, 2], [1, 3], [2], [3]];'AIA';b/a)).
coevo2(([[1, 2], [1, 3], [2]];'AIA';b/a)).
coevo2(([[1, 2], [1, 3], [3]];'ZZA';a/c)).
coevo2(([[1, 2], [1], [2, 3], [2]];'IAA';b/a)).
coevo2(([[1, 2], [1], [2, 3], [3]];'IAA';b/a)).
coevo2(([[1, 2], [1], [2, 3]];'IAA';b/a)).
coevo2(([[1, 2], [1], [2]];'IAA';b/a)).
coevo2(([[1, 2], [1], [3]];'IAA';b/a)).
coevo2(([[1, 2], [1]];'CAA';b/a)).
coevo2(([[1, 2], [2, 3], [2], [3]];'AIA';b/a)).
coevo2(([[1, 2], [2, 3], [2]];'ACA';b/a)).
coevo2(([[1, 2], [2, 3], [3]];'ZZA';a/c)).
coevo2(([[1, 2], [2], [3]];'AIA';b/a)).
coevo2(([[1, 2], [2]];'ACA';b/a)).
coevo2(([[1, 2], [3]];'ZZA';a/c)).
coevo2(([[1, 3], [1], [2, 3], [2]];'IAA';b/a)).
coevo2(([[1, 3], [1], [2, 3], [3]];'IAA';b/a)).
coevo2(([[1, 3], [1], [2, 3]];'IAA';b/a)).
coevo2(([[1, 3], [1], [2]];'IAA';b/a)).
coevo2(([[1, 3], [1], [3]];'IAA';b/a)).
coevo2(([[1, 3], [1]];'CAA';b/a)).
coevo2(([[1, 3], [2, 3], [2], [3]];'AIA';b/a)).
coevo2(([[1, 3], [2, 3], [2]];'AIA';b/a)).
coevo2(([[1, 3], [2, 3], [3]];'CCA';a/b)).
coevo2(([[1, 3], [2], [3]];'AIA';b/a)).
coevo2(([[1, 3], [2]];'AIA';b/a)).
coevo2(([[1, 3], [3]];'CCA';a/b)).
coevo2(([[1], [2, 3], [2]];'IAA';b/a)).
coevo2(([[1], [2, 3], [3]];'IAA';b/a)).
coevo2(([[1], [2, 3]];'IAA';b/a)).
coevo2(([[1], [2]];'IAA';b/a)).
coevo2(([[1], [3]];'IAA';b/a)).
coevo2(([[1]];'CAA';b/a)).
coevo2(([[2, 3], [2], [3]];'AIA';b/a)).
coevo2(([[2, 3], [2]];'ACA';b/a)).
coevo2(([[2, 3], [3]];'CCA';a/b)).
coevo2(([[2], [3]];'AIA';b/a)).
coevo2(([[2]];'ACA';b/a)).
coevo2(([[3]];'CCA';a/b)).
%...

/*
?- gen_win(G,[monotonic:no(_)]),\+ coevo2(G;L),nl,write(G),fail.

[[1, 2, 3], [1, 2], [1, 3], [1], [2], [3]]
[[1, 2, 3], [1, 2], [1], [2, 3], [2], [3]]
[[1, 2, 3], [1, 2], [1], [2], [3]]
[[1, 2, 3], [1, 3], [1], [2, 3], [2], [3]]
[[1, 2, 3], [1, 3], [1], [2], [3]]
[[1, 2, 3], [1], [2, 3], [2], [3]]
[[1, 2, 3], [1], [2], [3]]
[[1, 2], [1, 3], [1], [2, 3], [2], [3]]
[[1, 2], [1, 3], [1], [2, 3]]
[[1, 2], [1, 3], [1], [2], [3]]
[[1, 2], [1, 3], [2, 3]]
[[1, 2], [1, 3]]
[[1, 2], [1], [2, 3], [2], [3]]
[[1, 2], [1], [2], [3]]
[[1, 2], [2, 3]]
[[1, 2]]
[[1, 3], [1], [2, 3], [2], [3]]
[[1, 3], [1], [2], [3]]
[[1, 3], [2, 3]]
[[1, 3]]
[[1], [2, 3], [2], [3]]
[[1], [2], [3]]
[[2, 3]]

No
?- gen_win(G,[monotonic:no(_),proper:yes]),\+ coevo2(G;L),nl,write(G),fail.

[[1, 2, 3], [1], [2], [3]]
[[1, 2], [1, 3], [2, 3]]
[[1, 2], [1, 3]]
[[1, 2], [2, 3]]
[[1, 2]]
[[1, 3], [2, 3]]
[[1, 3]]
[[1], [2], [3]]
[[2, 3]]

No
?- gen_win(G,[monotonic:no(_),'not weak':no(_)]),\+ coevo2(G;L),nl,write(G),fail.

[[1, 2], [1, 3]]
[[1, 2], [2, 3]]
[[1, 2]]
[[1, 3], [2, 3]]
[[1, 3]]
[[2, 3]]

No
?- gen_win(G,[monotonic:no(_),'not weak':no(_),proper:no(_)]).

No
?-

% Observation. Any nonmonotonic game is proper if it is weak.

?- gen_win(G,[monotonic:no(_),strong:yes]),\+ coevo2(G;L),nl,write(G),fail.

[[1, 2, 3], [1, 2], [1, 3], [1], [2], [3]]
[[1, 2, 3], [1, 2], [1], [2, 3], [2], [3]]
[[1, 2, 3], [1, 2], [1], [2], [3]]
[[1, 2, 3], [1, 3], [1], [2, 3], [2], [3]]
[[1, 2, 3], [1, 3], [1], [2], [3]]
[[1, 2, 3], [1], [2, 3], [2], [3]]
[[1, 2, 3], [1], [2], [3]]

No
?- coevo2(G;A;B/W),gen_win(G),verify_win,name_domain(A,R),
majority(R->M),best(W,M),nl,write(m:W;R->M),
forall(distance(dodgson(min,K,X),R->Q,H,Z),(nl,write(K:X;Q;Z))),nl,fail.

game:[[1, 2, 3], [1, 2], [1, 3], [1], [2]]
 + :[strong, not weak, essential]
 - :[nonmonotonic: ([2], [2, 3]), improper:[1, 3]]
m:a;[[-, -, +], [+, +, +], [+, +, +]]->[+, +, +]
2:a;[[+, +, +], [+, +, +], [+, +, +]];[[a], [], []]
1:b;[[-, -, +], [-, +, +], [+, +, +]];[[b], []]
3:c;[[-, -, -], [+, -, -], [+, +, +]];[[c], [], [], []]

game:[[1, 2, 3], [1, 2], [1, 3], [1], [3]]
 + :[strong, not weak, essential]
 - :[nonmonotonic: ([3], [2, 3]), improper:[1, 2]]
m:a;[[-, -, +], [+, +, +], [+, +, +]]->[+, +, +]
2:a;[[+, +, +], [+, +, +], [+, +, +]];[[a], [], []]
1:b;[[-, -, +], [+, +, +], [-, +, +]];[[b], []]
3:c;[[-, -, -], [+, +, +], [+, -, -]];[[c], [], [], []]

game:[[1, 2, 3], [1, 2], [1, 3], [2], [3]]
 + :[not weak, essential]
 - :[nonmonotonic: ([2], [2, 3]), improper:[1, 2], not strong:[1]]
m:a;[[+, +, +], [-, -, +], [+, +, +]]->[+, +, +]
2:a;[[+, +, +], [+, +, +], [+, +, +]];[[a], [], []]
1:b;[[+, +, +], [-, -, +], [-, +, +]];[[b], []]
3:c;[[+, +, +], [-, -, -], [+, -, -]];[[c], [], [], []]

game:[[1, 2, 3], [1, 2], [1, 3], [2]]
 + :[not weak, essential]
 - :[nonmonotonic: ([2], [2, 3]), improper:[1, 3], not strong:[1]]
m:a;[[+, +, +], [-, -, +], [+, +, +]]->[+, +, +]
2:a;[[+, +, +], [+, +, +], [+, +, +]];[[a], [], []]
1:b;[[-, +, +], [-, -, +], [+, +, +]];[[b], []]
3:c;[[+, -, -], [-, -, -], [+, +, +]];[[c], [], [], []]

game:[[1, 2, 3], [1, 2], [1, 3], [3]]
 + :[not weak, essential]
 - :[nonmonotonic: ([3], [2, 3]), improper:[1, 2], not strong:[1]]
m:c;[[+, -, -], [+, -, -], [+, +, +]]->[+, -, -]
1:a;[[+, +, -], [+, -, -], [+, +, +]];[[a], []]
3:b;[[-, -, +], [+, -, -], [-, +, +]];[[b], [], [], []]
2:c;[[+, -, -], [+, -, -], [+, -, -]];[[c], [], []]

game:[[1, 2, 3], [1, 2], [1], [2, 3], [2]]
 + :[strong, not weak, essential]
 - :[nonmonotonic: ([1], [1, 3]), improper:[1]]
m:a;[[-, -, +], [+, +, +], [+, +, +]]->[+, +, +]
2:a;[[+, +, +], [+, +, +], [+, +, +]];[[a], [], []]
1:b;[[-, -, +], [-, +, +], [+, +, +]];[[b], []]
3:c;[[-, -, -], [+, -, -], [+, +, +]];[[c], [], [], []]

game:[[1, 2, 3], [1, 2], [1], [2, 3], [3]]
 + :[not weak, essential]
 - :[nonmonotonic: ([1], [1, 3]), improper:[1, 2], not strong:[1, 3]]
m:a;[[-, -, +], [+, +, +], [+, +, +]]->[+, +, +]
2:a;[[+, +, +], [+, +, +], [+, +, +]];[[a], [], []]
1:b;[[-, -, +], [+, +, +], [-, +, +]];[[b], []]
3:c;[[-, -, -], [+, +, +], [+, -, -]];[[c], [], [], []]

No
?- 

*/


% rule mining for D-metric manipulability

/*
% cited from sged06:
axioms_for_win([
  monotonic:_,
  proper:_,
  strong:_,
  'not weak':_,
  essential:_
]).
inspectall_win([M,P,S,W,E,D]):-
   inspect_win(monotonic:M),
   inspect_win(proper:P),
   inspect_win(strong:S),
   inspect_win('not weak':W),
   inspect_win(essential:E),
   (W=[J]->D=no(J);D=yes).
*/

construct_rule(Y->Z,O):-
   axioms_for_win(X),
   construct_rule_1(X,Y->Z),
   construct_rule_2(X,Y->Z,O).

construct_rule_1([],[]->[]).
construct_rule_1([A:_|X],[A|B]->C):-
   construct_rule_1(X,B->C).
construct_rule_1([A:_|X],B->[A|C]):-
   construct_rule_1(X,B->C).
construct_rule_1([_|X],B->C):-
   construct_rule_1(X,B->C).

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

/*

?- construct_rule(Y->Z,O).

Y = [monotonic, proper, strong, 'not weak', essential]
Z = []
O = [monotonic:yes, proper:yes, strong:yes, 'not weak':yes, essential:yes] ;

Y = [monotonic, proper, strong, 'not weak']
Z = [essential]
O = [monotonic:yes, proper:yes, strong:yes, 'not weak':yes, essential:no(_G357)] 

Yes
?- 
*/





% revised: 11 Jul 2007

rule_miner(d-sensitive(-),A,B):-
   construct_rule(A->B,C),
   \+ (gen_win(G,C),(coevo(G;_);coevo2(G;_))).
rule_miner(d-sensitive(+),A,B):-
   construct_rule(A->B,C),
   \+ (gen_win(G,C),\+ (coevo(G;_);coevo2(G;_))).

/*
rule_miner(mono(+),d-invariance(-),A,B):-
   construct_rule(A->B,C),member(monotonic,A),
   \+ (gen_win(G,C),coevo(G;_)).
rule_miner(mono(+),d-invariance(+),A,B):-
   construct_rule(A->B,C),member(monotonic,A),
   \+ (gen_win(G,C),\+ coevo(G;_)).
rule_miner(mono(-),d-invariance(-),A,B):-
   construct_rule(A->B,C),\+ member(monotonic,A),
   \+ (gen_win(G,C),coevo2(G;_)).
rule_miner(mono(-),d-invariance(+),A,B):-
   construct_rule(A->B,C),\+ member(monotonic,A),
   \+ (gen_win(G,C),\+ coevo2(G;_)).

minimal_rule_miner(S,T,A,B):-
   rule_miner(S,T,A,B),
   \+ (
     rule_miner(S,T,C,D),
     (C,D)\=(A,B),
     subset(C,A),subset(D,B)
   ).
*/

minimal_rule_miner(T,A,B):-
   rule_miner(T,A,B),
   \+ (
     rule_miner(T,C,D),
     (C,D)\=(A,B),
     subset(C,A),subset(D,B)
   ).

:- dynamic dmr/1.

tell_minimal_rules:-
   C=dmr(T:A->B),
   forall(minimal_rule_miner(T,A,B),
    (
     clause(C,_)->true;assert(C)
    )
   ),
   nl,write('save the dmr/1 results to file? (y/n)'),
   read(Y),
   (member(Y,[y,'Y'])->tell_goal('metric_miner.pl',forall,C);true).

% eliminate insensitive rules to d-invariance.

dmr_1((B):C->D):- dmr((B):C->D), \+ (dmr((B1):C->D), B1\=B).

% theorem for simple games (d-invariance insensitive).

dmr_2((B):C->D):- dmr((B):C->D), \+ dmr_1((B):C->D).


/*

?- minimal_rule_miner(S,T,A,B).

S = mono(+)
T = d-invariance(-)
A = [monotonic, proper, strong, 'not weak', essential]
B = [] ;

S = mono(+)
T = d-invariance(-)
A = [monotonic, proper, strong, 'not weak']
B = [essential] 

Yes
?- dmr((A,B):C->D),\+ (dmr((A,B1):C->D),B1\=B).

A = mono(+)
B = d-invariance(-)
C = ['not weak']
D = [essential]
B1 = _G169 

Yes

% revised: 11 Jul 2007

?- tell_minimal_rules.

Yes
?- dmr_1((B):C->D),nl,write((B):C->D),fail.

d-sensitive(-):[monotonic, proper, not weak]->[]
d-sensitive(-):[monotonic, proper, essential]->[]
d-sensitive(-):[monotonic]->[strong]
d-sensitive(-):[monotonic, essential]->[not weak]
d-sensitive(-):[strong]->[monotonic, not weak]
d-sensitive(-):[]->[monotonic, essential]
d-sensitive(-):[]->[proper, essential]
d-sensitive(-):[strong, essential]->[not weak]
d-sensitive(-):[]->[strong, essential]
d-sensitive(-):[not weak]->[essential]
d-sensitive(+):[monotonic]->[proper, strong]
d-sensitive(+):[monotonic, not weak]->[strong]
d-sensitive(+):[strong]->[not weak]
d-sensitive(+):[]->[essential]

No
?- dmr_1((B):C->D), \+ (oof(X,[C,D]),oof(essential,X)),nl,write((B):C->D),fail.

d-sensitive(-):[monotonic, proper, not weak]->[]
d-sensitive(-):[monotonic]->[strong]
d-sensitive(-):[strong]->[monotonic, not weak]
d-sensitive(+):[monotonic]->[proper, strong]
d-sensitive(+):[monotonic, not weak]->[strong]
d-sensitive(+):[strong]->[not weak]

No
?- dmr_2((B):C->D),nl,write((B):C->D),fail.

d-sensitive(-):[]->[proper, not weak]
d-sensitive(+):[]->[proper, not weak]

No
?-

*/


% end