/************************************************************ coalitions, simple games, essential decomposability and transitivity of dominance relations: revised version program: sged06.pl language: prolog date: 2006.12.26-31 & 2007.1.1,5-9,12. last revision: 21:04 pm, 12 Jan 2007 creator: Kenryo INDO ************************************************************/ % load the ia-domain manager if oof/2 does not exist. :- (\+ clause(mia_domain(_,_),_)->[drsc06];true). % cumulative system list sys_list([gprf06,cswf06,spcf06,dcdi06,drsc06,sged06]). % override init_me/0 init_me:- sys_list(L),oof(P,L),nl,write(reload:P),[P],fail;true. % override display_swf_header/0,1 in cswf06 display_swf_header:- bagof(N,K^R^(id_r(K:N,R),r_j_admitted(2,R)),L), nl,write('swf:row col |'),write_sequence(L). display_swf_header(XY):- b(XY), findall(T,(id_r(_,R),rb(T,XY,R),r_j_admitted(2,R)),L), tab(1),XY=(X,Y),write(X),write(Y),write(|),write_sequence(L). %------------- % generating individual admissible domain % mia_domain(L,Y) :- .. from drsc06.pl %------------- % logical implications if(A,B):- \+ (A, \+ B). % if(A,B):- forall(A,B). iff(A,B):- if(A,B),if(B,A). if(A,B,fail):- A, \+ B. if(A,B,true):- \+ if(A,B,fail). only_if(A,B,fail):- \+ A, B. only_if(A,B,true):- \+ only_if(A,B,fail). iff(A,B,fail):- if(A,B,fail). iff(A,B,fail):- only_if(A,B,fail). iff(A,B,true):- \+ iff(A,B,fail). %------------- % list concatenate l_concat([A],A). l_concat([L|R],Z):- l_concat(R,Q),concat(L,Q,Z). %------------- % display each element in a list display_each(W):- \+ var(W),forall(oof(X,W),(nl,write(X))). %------------- % coalitions and group structure coalition(C):- c(C). c(C):- agents(N),select_n(C,N,K),K>0. all_coalitions(L):- findall(C,c(C),L). supergroup(C,D):- c_sup(C,D). subgroup(C,D):- c_sub(C,D). complementary_group(C,D):- c_comp(C,D). c_sup(C,D):- (var(C)->c(C);true),c(D),subset(C,D). c_sub(C,D):- (var(C)->c(C);true),c(D),subset(D,C). c_comp(C,D):- (var(C)->c(C);true),agents(N),subtract(N,C,D). % revised: 5 Jan 2007 c_union([],[]). c_union([C|D],E):- c_union(D,F),(var(C)->c(C);true),union(C,F,G),sort(G,E). % revised: 9 Jan 2007 c_meet([],[]). c_meet([C],C). c_meet([C|D],E):- c_meet(D,F),D\=[],(var(C)->c(C);true),intersection(C,F,E). %------------- % simple game : a family of winning coalitions :- dynamic win/2. winning(C):- var(C),win(C,yes). winning(C):- \+ var(C),sort(C,C1),win(C2,yes),sort(C2,C1). loosing(C):- var(C),win(C,no). loosing(C):- \+ var(C),sort(C,C1),win(C2,no),sort(C2,C1). all_win(L):- findall(C,win(C,yes),L). all_loose(L):- findall(C,win(C,no),L). axioms_for_win([ monotonic:_, proper:_, strong:_, 'not weak':_, essential:_ ]). antonym(monotonic,nonmonotonic). antonym(proper,improper). antonym(strong,'not strong'). antonym('not weak',weak(vetoers)). antonym(essential,inessential(dictator)). axiom_win(A):- axioms_for_win(X),oof(A:_,X). verify_axiom_win(A):- \+ not_win(A). % violations not_win(monotonic:(C,D)):- winning(C),supergroup(C,D),loosing(D). not_win(proper:C):- winning(C),c_comp(C,D),winning(D). not_win(strong:C):- loosing(C),c_comp(C,D),loosing(D). not_win('not weak':V):- setof(J,vetoer(J),V). not_win(essential:J):- min_win([[J]]). % THEOREM (Shapley,1952) No essential game is both weak and strong. not_win(nondictatorial:J):- setof(J,vetoer(J),[J]). vetoer(J):- j(J), \+ (win(C,yes), \+ oof(J,C)). dictator(J):- vetoer(J), \+ (vetoer(K),K\=J). all_supersets(C,L):- findall(D,supergroup(C,D),L). seteq(A,B):- subset(A,B),subset(B,A). % minimal winning coalitions filter_win(M):- all_win(W),select_n(M,W,_), findall(D, (oof(C,M),supergroup(C,D)), U), seteq(W,U). all_filter_win(L):- findall(M,filter_win(M),L). min_win(M):- all_filter_win(L),all_intersect(L,M). all_intersect([],[]). all_intersect([A],A). all_intersect([A|L],M):- all_intersect(L,Y),intersection(A,Y,M). dummy_j(J):- j(J),\+ (min_win(M),oof(C,M),oof(J,C)). all_dummy(L):- findall(J,dummy_j(J),L). %------------- % inspecting properties of simple game 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). inspect_win(A:Z):- not_win(A:V),!,Z=no(V). inspect_win(_:yes). verify_win(T,F):- findall(Y,(axiom_win(Y),inspect_win(Y:yes)),T), findall(Z:P,(axiom_win(Y),antonym(Y,Z),inspect_win(Y:no(P))),F). verify_win:- all_win(W),verify_win(T,F), nl,write(game:W),nl,tab(1),write('+':T),nl,tab(1),write('-':F). %------------- % generating simple games % initialize win/2 init_win(L):- abolish(win/2),(var(L)->all_coalitions(L);true), forall(oof(C,[[]|L]),assert(win(C,no))). nonempty_set_of_coalitions(W,LC):- select_n(W,LC,K),K>0. gen_win(W):- gen_win(W,[]). gen_win(W,CON):- all_coalitions(L),gen_win(W,L,CON). gen_win(W,L,CON):- axioms_for_win(Ax),subset(CON,Ax),init_win(L), nonempty_set_of_coalitions(W,L),update_win(W), \+ (oof(G:T,CON),\+ inspect_win(G:T)). update_win(W):- forall(win(C,A),update_win(C,W,A->_)). update_win(C,W,yes->yes):- oof(C,W). update_win(C,W,no->no):- \+ oof(C,W). update_win(C,W,no->yes):- oof(C,W),retract(win(C,no)),assert(win(C,yes)). update_win(C,W,yes->no):- \+ oof(C,W),retract(win(C,yes)),assert(win(C,no)). :- dynamic win_0/2. % for rescue: reserve-and-restore reserve_win:- abolish(win_0/2),forall(win(C,Y),assert(win_0(C,Y))). restore_win:- forall(win_0(C,Y),assert(win(C,Y))). display_win:- forall(winning(C),(write(C),write(;))). % demo /* ?- gen_win(W). W = [[1, 2], [1], [2]] Yes ?- display_win. [1, 2];[1];[2]; Yes ?- gen_win(W),nl,write(g:W),findall(C,winning(C),L),tab(1),write(w:L), findall(C,loosing(C),F),tab(1),write(l:F),fail. g:[[1, 2], [1], [2]] w:[[1, 2], [1], [2]] l:[] g:[[1, 2], [1]] w:[[1, 2], [1]] l:[[2]] g:[[1, 2], [2]] w:[[1, 2], [2]] l:[[1]] g:[[1, 2]] w:[[1, 2]] l:[[1], [2]] g:[[1], [2]] w:[[1], [2]] l:[[1, 2]] g:[[1]] w:[[1]] l:[[1, 2], [2]] g:[[2]] w:[[2]] l:[[1, 2], [1]] No ?- gen_win(W),nl,write(W),inspectall_win(S),write(S),fail. [[1, 2], [1], [2]][yes, no([1]), yes, yes, yes] [[1, 2], [1]][yes, yes, yes, no([1]), no((-weak, [1]))] [[1, 2], [2]][yes, yes, yes, no([2]), no((-weak, [2]))] [[1, 2]][yes, yes, no([1]), no([1, 2]), no((-strong, [1]))] [[1], [2]][no(([1], [1, 2])), no([1]), yes, yes, yes] [[1]][no(([1], [1, 2])), yes, yes, no([1]), no((-weak, [1]))] [[2]][no(([2], [1, 2])), yes, yes, no([2]), no((-weak, [2]))] No ?- gen_win(W,[]),min_win(M),all_dummy(D),nl,write(win:W-min:M:dummy:D), fail. win:[[1, 2], [1], [2]]-min:[[1], [2]]:dummy:[] win:[[1, 2], [1], [2]]-min:[]:dummy:[] win:[[1, 2], [1]]-min:[[1]]:dummy:[2] win:[[1, 2], [1]]-min:[]:dummy:[2] win:[[1, 2], [2]]-min:[[2]]:dummy:[1] win:[[1, 2], [2]]-min:[]:dummy:[1] win:[[1, 2]]-min:[[1, 2]]:dummy:[] win:[[1, 2]]-min:[]:dummy:[] win:[[1], [2]]-min:[]:dummy:[1, 2] win:[[1]]-min:[]:dummy:[1, 2] win:[[2]]-min:[]:dummy:[1, 2] No ?- gen_win(W,[]),verify_win,fail. game:[[1, 2], [1], [2]] + :[monotonic, strong, not weak, essential] - :[improper:[1]] game:[[1, 2], [1]] + :[monotonic, proper, strong] - :[weak(vetoers):[1], inessential(dictator):1] game:[[1, 2], [2]] + :[monotonic, proper, strong] - :[weak(vetoers):[2], inessential(dictator):2] game:[[1, 2]] + :[monotonic, proper, essential] - :[not strong:[1], weak(vetoers):[1, 2]] game:[[1], [2]] + :[not weak, essential] - :[nonmonotonic: ([1], [1, 2]), improper:[1], not strong:[]] game:[[1]] + :[proper, essential] - :[nonmonotonic: ([1], [1, 2]), not strong:[], weak(vetoers):[1]] game:[[2]] + :[proper, essential] - :[nonmonotonic: ([2], [1, 2]), not strong:[], weak(vetoers):[2]] No ?- % THEOREM (Shapley,1952) No essential game is both weak and strong. ?- gen_win(W,['not weak':no(_),strong:yes]),verify_win,fail. game:[[1, 2], [1]] + :[monotonic, proper, strong] - :[weak(vetoers):[1], inessential(dictator):1] game:[[1, 2], [2]] + :[monotonic, proper, strong] - :[weak(vetoers):[2], inessential(dictator):2] No ?- % THEOREM (Wilson,1972; Arrow, 1963) % No nondictatorial game is both proper and strong. ?- gen_win(W,[proper:yes,strong:yes]),verify_win,fail. game:[[1, 2], [1]] + :[monotonic, proper, strong] - :[weak(vetoers):[1], inessential(dictator):1] game:[[1, 2], [2]] + :[monotonic, proper, strong] - :[weak(vetoers):[2], inessential(dictator):2] No ?- */ %------------- % duality dual_win(D):- findall(C,(win(L,no),c_comp(L,C)),D). dual_win(W,D):- \+ var(W), findall(C,((L=[];c(L)),\+ oof(L,W),c_comp(L,C)),D). blocking(B):- loosing(C),c_comp(C,B),loosing(B). minimal_blocking(B):- min_block(B). min_block(B):- blocking(B),\+ (c_sub(B,D),\+ blocking(D)). % THEOREM (Shapley,1952) % (1) the dual of the dual of game W is W. % (2) the dual of game W is proper iff W is strong. % (3) the dual of game W is W iff W is strong and proper. % demo /* % proof of (1) ?- gen_win(W,[]),dual_win(D),dual_win(D,DD),nl, write(g:W:d:D:dd:DD),tab(1),(seteq(W,DD)->write(w=dd);true),fail. g:[[1, 2], [1], [2]]:d:[[1, 2]]:dd:[[1], [1, 2], [2]] w=dd g:[[1, 2], [1]]:d:[[1, 2], [1]]:dd:[[1], [1, 2]] w=dd g:[[1, 2], [2]]:d:[[1, 2], [2]]:dd:[[1, 2], [2]] w=dd g:[[1, 2]]:d:[[1, 2], [2], [1]]:dd:[[1, 2]] w=dd g:[[1], [2]]:d:[[1, 2], []]:dd:[[1], [2]] w=dd g:[[1]]:d:[[1, 2], [], [1]]:dd:[[1]] w=dd g:[[2]]:d:[[1, 2], [], [2]]:dd:[[2]] w=dd No ?- % proof of (2) ?- gen_win(W,[]),inspect_win(strong:S),dual_win(D),nl, write((g=W):(strong=S)),update_win(D),inspect_win(proper:P), tab(1),write((dual=D):(proper=P)),fail. (g=[[1, 2], [1], [2]]): (strong=yes) (dual=[[1, 2]]): (proper=yes) (g=[[1, 2], [1]]): (strong=yes) (dual=[[1, 2], [1]]): (proper=yes) (g=[[1, 2], [2]]): (strong=yes) (dual=[[1, 2], [2]]): (proper=yes) (g=[[1, 2]]): (strong=no([1])) (dual=[[1, 2], [2], [1]]): (proper=no([1])) (g=[[1], [2]]): (strong=no([])) (dual=[[1, 2], []]): (proper=no([])) (g=[[1]]): (strong=no([])) (dual=[[1], [1, 2], []]): (proper=no([])) (g=[[2]]): (strong=no([])) (dual=[[2], [1, 2], []]): (proper=no([])) No ?- % proof of (3) ?- gen_win(W,[proper:yes,strong:yes]),dual_win(D), nl,write(g:W:d:D),tab(1),(seteq(W,D)->write(w=dual);true),fail. g:[[1, 2], [1]]:d:[[1, 2], [1]] w=dual g:[[1, 2], [2]]:d:[[1, 2], [2]] w=dual No ?- gen_win(W,[]), \+ (inspect_win(proper:yes),inspect_win(strong:yes)),dual_win(D), nl,write(g:W:d:D),tab(1),(seteq(W,D)->write(w=dual);true),fail. g:[[1, 2], [1], [2]]:d:[[1, 2]] g:[[1, 2]]:d:[[1, 2], [2], [1]] g:[[1], [2]]:d:[[1, 2], []] g:[[1]]:d:[[1, 2], [], [1]] g:[[2]]:d:[[1, 2], [], [2]] No ?- */ % decisive set as xy-winning coalitions %------------- % The following program generates a collection of simple games % for each pair of alternatives respectively % (given a set of conditions). all_d_pairs(L):- findall(XY,d_pair(XY),L). all_dop(L):- findall(XY,dop(XY),L). :- dynamic win_b/2. gen_win_b(W):- gen_win_b(W,_,[]). gen_win_b(W,D):- gen_win_b(W,D,[]). gen_win_b(W,D,CON):- axioms_for_win(A),subset(CON,A), all_dop(ADP),(var(D)->D=ADP;subset(D,ADP)), all_coalitions(LC), gen_win_b_r(W,D,(LC,CON)). gen_win_b_r([],[],_). gen_win_b_r([XY:Wxy|WL],[XY|L],(LC,CON)):- gen_win_b_r(WL,L,(LC,CON)), gen_win(Wxy,CON). update_win_b(W):- abolish(win_b/2), forall(oof(XY:Wxy,W),assert(win_b(XY,Wxy))). % demo /* ?- gen_win_b(W,[proper:yes,strong:yes]), forall(oof(X,W),(nl,write(X))),!,fail. (a, b):[[1, 2], [1]] (a, c):[[1, 2], [1]] (b, c):[[1, 2], [1]] (b, a):[[1, 2], [1]] (c, a):[[1, 2], [1]] (c, b):[[1, 2], [1]] No ?- */ %------------- % essential decomposability (See Blair and Muller (1983)) r_j_xy(J,R,XY):- dop(XY),r_j_admitted(J,R),r(XY,R). p_j_xy(J,R,XY):- r_j_xy(J,R,XY),p(XY,R). xy_winning((X,Y),C):- win_b((X,Y),Wxy), oof(C,Wxy). % revised : 9 Jan 2007 % agreed preferences in a coalition at a profile c_agree(C,XY,RC):- c(C),dop(XY),c_agree_r(C,C,XY,RC). % dominative coalition at a profile c_agree_rr(C,XY,RR):- agents(N),dop(XY),c_agree_r(N,C,XY,RR),C\=[]. % recursive construction for (maximal) agreed coalition % revised: 7,10 Jan 2007 c_agree_r([],[],_,[]). c_agree_r([J|N],[J|C],XY,[Q|R]):- c_agree_r(N,C,XY,R),p_j_xy(J,Q,XY). c_agree_r([J|N],C,XY,[Q|R]):- c_agree_r(N,C,XY,R),r_j_admitted(J,Q).%,\+ p_j_xy(J,Q,XY). pivotal_j(J,(X,Y),C):- dop((X,Y)), p_j_xy(J,_,(X,Y)), p_j_xy(J,_,(Y,X)), xy_winning((X,Y),C),subtract(C,[J],B), \+ xy_winning((X,Y),B). c_sub_inhibited_triple((X,Y,Z),C,B):- (var(C)->c(C);true), findall(J,(oof(J,C), \+ (p_j_xy(J,_Dj,(X,Y)),p_j_xy(J,_Dj,(Y,Z))) ),B). % Definition: Assume strict orderings. % A set of ordered pairs of alternatives D is said % to be Essentially Decomposable w.r.t. a given profile P under % the individual admissible domain Di if for every ordered pair % (x,y) there exists a set of winning coalitions Wxy=W(x,y) % which satisifies the set of conditions from (ED1) to (ED4) % simultaneously. % (ed 1). If for all coalition C, % (for all i in C, Di contains xy) % & (for all j in N-C, Dj contains yx) % then Wxy contains C iff Wyx contains N-C. % Condition ed 1 implies that the ASWF is asymmetric and complete. not_ed(1,(X,Y),(C,B)):- dop((X,Y)), c_comp(C,B), \+ \+ c_agree(C,(X,Y),_), \+ \+ c_agree(B,(Y,X),_), \+ iff(xy_winning((X,Y),C),\+ xy_winning((Y,X),B)). % (ed 2). Wxy is monotone. % Condition ed 2 implies that the ASWF is monotonic. not_ed(2,XY,V):- win_b(XY,W),update_win(W),not_win(monotonic:V). % (ed 3). for all individual i, there exists a pair of % alternatives (xy) and a coalition C such that % (Di contains both xy and yx) & (Wxy contains C) % & (Wxy does not contain C-{i}) % Condition ed 3 implies that the ASWF is essential. % And together with ed 2 and the nonemptiness of Wxy, % it implies the Pareto condition. not_ed(3,_,J):- j(J),\+ (dop(XY),pivotal_j(J,XY,_)). % (ed 4). for all triple of alternative (x,y,z), % if (Wxy contains C) & (Wyz contains B) % & (for all i in C, Di contains xy) % & (for all j in B, Dj contains yz) % & (for all k in N-C-B, Dk contains zx) % then Wxz contains a coalition which is % the union of D,E, and meet(C,B), where % D:= {i in C| Di does not contain zxy}, and % E:= {j in B| Dj does not contain yzx}. % Condition ed 4 implies that the ASWF is transitive. not_ed(4,(X,Y),(Z,C,B,D,E,F)):- dot((X,Y,Z)), xy_winning((X,Y),C),xy_winning((Y,Z),B), \+ \+ c_agree(C,(X,Y),_),\+ \+ c_agree(B,(Y,Z),_), c_union([C,B],U),c_comp(U,NCB),\+ \+ c_agree(NCB,(Z,X),_), c_sub_inhibited_triple((Z,X,Y),C,D), c_sub_inhibited_triple((Y,Z,X),B,E), c_meet([C,B],CB),c_union([D,E,CB],F), \+ (F\=[],xy_winning((X,Z),F)). a_set_of_symmetric_dops(D):- all_d_pairs(L),select_n(P,L,_), P\=[],findall(XY,(oof((X,Y),P),oof(XY,[(X,Y),(Y,X)])),D). ed_win(W,D):- ed_win(W,D,[monotonic:yes]). ed_win(W,D,CON):- (var(CON)->CON=[monotonic:yes];true), % a_set_of_symmetric_dops(D), % all_dop(L),select_n(D,L,_), all_dop(D), gen_win_b(W,D,CON),update_win_b(W), \+ not_ed(_,_,_). %------------- % some test codes % overlooking a set of conditions in a list L. rlxd_ed_win(W,D,L):- \+ var(L), subset(L,[1,2,3,4]), % a_set_of_symmetric_dops(D), all_dop(D), gen_win_b(W,D),update_win_b(W), \+ (not_ed(K,_,_),\+ oof(K,L)). /* % a demo for relaxation ?- rlxd_ed_win(W,D,[1]),nl,write(D),display_win_xy(W). [ (a, b), (a, c), (b, c), (b, a), (c, a), (c, b)] (a, b):[[1, 2]] (a, c):[[1, 2]] (b, c):[[1, 2]] (b, a):[[1, 2]] (c, a):[[1, 2], [1], [2]] (c, b):[[1, 2], [1], [2]] W = [ (a, b):[[1, 2]], (a, c):[[1, 2]], (b, c):[[1, 2]], (b, a):[[1, 2]], (c, a):[[1, 2], [1], [...]], (c, b):[[1|...], [...]|...]] D = [ (a, b), (a, c), (b, c), (b, a), (c, a), (c, b)] Yes ?- */ %------------- % the derived essential monotonic social ordering (EM-SWF) : % xy iff Wxy contains coalition via which x dominates y. em_swf([],[]). em_swf([RR->Q|F],[RR|L]):- em_swf(F,L),axiom_em_swf(RR->Q). em_swf(F):-all_rr(L),em_swf(F,L). % axioms for em_swf axiom_em_swf(RR->Q):- l(Q),\+ (c_agree(_,XY,RR),\+ p(XY,Q)). %------------- % generating xy-dominative coalitions as xy-minimal winning % coalition based on an EM-SWF. em_win_xy(XY,C,F):- (var(F)->em_swf(F);true), dop(XY),oof(RR->R,F),p(XY,R),c_agree_rr(C,XY,RR). gen_em_win_xy(XY,L,F):- em_swf(F),setof(C,E^( em_win_xy(XY,E,F),c(C),subset(E,C) ),L1), agents(N), union(L1,[N],L). gen_em_win(W,F):- findall(XY:L,gen_em_win_xy(XY,L,F),W), update_win_b(W). em_swf_1([],[]). em_swf_1([RR->Q|F],[RR|L]):- em_swf_1(F,L),axiom_em_swf_1(RR->Q). em_swf_1(F):-all_rr(L),em_swf_1(F,L). axiom_em_swf_1(RR->Q):- l(Q),\+ (win_b(XY,C),c_agree(C,XY,RR),\+ p(XY,Q)). % The following clause uses udrr/4 from spcf06.pl % DEFINITION (Essential SWF): % An swf f on a linear ordering individual admissible domain % is essential iff for all agent i there exists a profile PP, % permissible ordering Qi and a pair (x,y) of alternatives, % such that f(PP) contains xy and f(PP/Qi) contains yx where % PP/Qi denotes the unilateral deviated profile. essential_swf(F):- if(j(J),essential_swf_j((J,_),_XY,F)). essential_swf_j((J,P,Q,RR,RQ),(X,Y),F):- dop((X,Y)), oof(RR->R,F),p((X,Y),R), oof(RQ->S,F),p((Y,X),S), udrr(RR,RQ,_,(J,P,Q)). % pivotality is a similar concept (w.r.t. xy-decisive coalition). % DEFINITION (Monotonic SWF): % An swf f on a linear ordering individual admissible domain % is monotonic iff for all pairs (x,y) of alternatives, and for % all coalitions C, if for every profile PP at which % x dominates y via C implies that f(PP) contains xy, % then for any profile QQ at which x dominates y via D s.t. % C is a subset of D implies f(QQ) still contains xy. mono_swf([],[]). mono_swf([RR->Q|F],[RR|L]):- mono_swf(F,L),axiom_mono_swf(RR->Q,F). mono_swf(F):-all_rr(L),mono_swf(F,L). % axioms for mono_swf axiom_mono_swf(RR->Q,F):- l(Q),\+ not_monotonic(RR->Q,F,_). not_monotonic(RR->Q,F,(XY,D,QQ->S)):- c_agree_rr(C,XY,RR),p(XY,Q),oof(QQ->S,F), c_agree_rr(D,XY,QQ),subset(C,D),D\=C,\+ p(XY,S). not_monotonic(RR->Q,F,(XY,D,QQ->S)):- c_agree_rr(C,XY,RR),\+ p(XY,Q),oof(QQ->S,F), c_agree_rr(D,XY,QQ),p(XY,S),subset(D,C),D\=C. % demo /* ?- L=[[+,+,-]],R=[[-,-,-]],mia_domain([1:L,2:R],free). L = [[+, +, -]] R = [[-, -, -]] Yes ?- F = [ ([[+, +, -], [-, -, -]]->[+, -, -])], em_win_xy(XY,W,F),nl,write(XY;W),fail. a, b;[1] c, a;[2] c, b;[1, 2] No ?- F = [ ([[+, +, -], [-, -, -]]->[+, -, -])], gen_em_win_xy(XY,W,F),nl,write(XY;W),fail. a, b;[[1], [1, 2]] c, a;[[2], [1, 2]] c, b;[[1, 2]] No ?- F = [ ([[+, +, -], [-, -, -]]->[+, -, -])], gen_em_win(W,F),display_each(W),fail. (a, b):[[1], [1, 2]] (c, a):[[2], [1, 2]] (c, b):[[1, 2]] No ?- em_swf(F). F = [ ([[+, +, -], [-, -, -]]->[+, +, -])] ; F = [ ([[+, +, -], [-, -, -]]->[+, -, -])] ; F = [ ([[+, +, -], [-, -, -]]->[-, -, -])] ; No ?- em_swf(F),swf(F,arrow(l)),\+ dictator(_,F). F = [ ([[+, +, -], [-, -, -]]->[+, -, -])] ; No ?- c_agree(A,B,C),nl,write(A;B;C),fail. [1, 2];c, b;[[+, +, -], [-, -, -]] [1];a, b;[[+, +, -]] [1];a, c;[[+, +, -]] [1];c, b;[[+, +, -]] [2];b, a;[[-, -, -]] [2];c, a;[[-, -, -]] [2];c, b;[[-, -, -]] No ?- win_b(A,B),nl,write(A;B),fail. a, b;[[1], [1, 2]] c, a;[[2], [1, 2]] c, b;[[1, 2]] No ?- em_swf_1(F),nl,write(F),fail. [ ([[+, +, -], [-, -, -]]->[+, +, +])] [ ([[+, +, -], [-, -, -]]->[-, +, +])] [ ([[+, +, -], [-, -, -]]->[-, -, +])] [ ([[+, +, -], [-, -, -]]->[+, +, -])] [ ([[+, +, -], [-, -, -]]->[+, -, -])] [ ([[+, +, -], [-, -, -]]->[-, -, -])] No ?- em_swf_1(F), essential_swf_j((J,P,Q,RR,RQ),(X,Y),F). No ?- L = [[+, +, -], [+, -, -]],R = [[+, -, -], [-, -, -]], mia_domain([1:L,2:R],free). L = [[+, +, -], [+, -, -]] R = [[+, -, -], [-, -, -]] Yes ?- swf(F,A), \+ mono_swf(F),display_swf_t2(F). swf:row col |ZN ab|+- ac|-- bc|-- -------------------------------------------------- [+, +, -]=T |AC +|-+ +|++ -|++ [+, -, -]=Z |AC +|-+ -|++ -|++ F = [ ([[+, +, -], [+, -, -]]->[-, +, +]), ([[+, -, -], [+, -, -]]->[-, +, +]), ([[+, +, -], [-, -, -]]->[+, +, +]), ([[+, -, -], [-, -|...]]->[+, +, +])] A = iia Yes ?- mono_swf(F),swf(F,iia),display_swf_t2(F). swf:row col |ZN ab|+- ac|-- bc|-- -------------------------------------------------- [+, +, -]=T |AA +|++ +|++ -|++ [+, -, -]=Z |AA +|++ -|++ -|++ F = [ ([[+, +, -], [+, -, -]]->[+, +, +]), ([[+, -, -], [+, -, -]]->[+, +, +]), ([[+, +, -], [-, -, -]]->[+, +, +]), ([[+, -, -], [-, -|...]]->[+, +, +])] Yes ?- mono_swf(F),\+ swf(F,iia),display_swf_t2(F). swf:row col |ZN ab|+- ac|-- bc|-- -------------------------------------------------- [+, +, -]=T |AT +|++ +|++ -|-+ [+, -, -]=Z |AA +|++ -|++ -|++ F = [ ([[+, +, -], [+, -, -]]->[+, +, -]), ([[+, -, -], [+, -, -]]->[+, +, +]), ([[+, +, -], [-, -, -]]->[+, +, +]), ([[+, -, -], [-, -|...]]->[+, +, +])] Yes ?- */ %------------- % proving Blair-Muller Theorem % THEOREM (Blair and Muller,1983) % The following three conditions are equivalent. % (1) a set of distinct alternatives D is essentially % decomposable wrt an individually admissible domain % (2) There is an essential monotonic Arrovian swf. % (3) There is a coalitional strategy-proof scf. display_win_xy:- forall(win(XY,C),(nl,write(XY:C))). display_win_xy(W):- \+ var(W),display_each(W). % demo /* % ------------- % Proving Blair-Muller theorem (for 2-agent 3-alternative case) % ------------- % setting the domain ?- [menu]. % menu compiled 0.00 sec, 18,696 bytes Yes ?- display_domain. current domain: ACITZN [base domain=l:linear] Yes ?- model(A,B). A = states:[a, b, c] B = agents:[1, 2] Yes ?- % Proving the equivalence for the Kalai-Muller theorem % for common admissible domains (similarly to the way of dcdi06) ?- restricted_domain(L,l,N), \+ iff(\+ ed_win(W,D),\+ (swf(F,arrow(l)),\+ dictator(_,F))). No ?- restricted_domain(L,l,N), \+ iff(\+ ed_win(W,D),\+ (swf(F,arrow(l)),\+ dictator(_,F),em_swf(F))). No ?- % a review of dcdi06.pl ?- restricted_domain(L,l,N), \+ iff(\+ cdi_pairs(_,_),\+ (swf(F,arrow(l)),\+ dictator(_,F))). No ?- % ------------- % proof for diagonals : % Another way to reproduce the Kalai-Muller theorem by % generating (assymetric) individual admissible domains % OBSERVATION. Assume symmetric admissible domains. % A domain is essentially decomposable iff % there exists a nondictatorial Arrovian SWF. ?- stopwatch((mia_domain([1:L,2:L],free),\+ iff(\+ ed_win(W,D), \+ (swf(F,arrow(l)),\+ dictator(_,F)) ));true,T). % time elapsed (sec): 171.562 L = _G158 W = _G172 D = _G173 F = _G179 T = 171.562 Yes % After revised c_meet/2 ?- stopwatch((mia_domain([1:L,2:L],free),\+ iff(\+ ed_win(W,D), \+ (swf(F,arrow(l)),\+ dictator(_,F)) ));true,T). % time elapsed (sec): 164.625 L = [[+, +, +], [-, +, +], [-, -, +], [+, +, -], [+, -, -], [-, -, -]] W = _G175 D = _G176 F = _G182 T = 164.625 Yes ?- % OBSERVATION. For common admissible domains, % essentiality is implied by nondictatorship. % (Generally essentiality implies nondictatorship.) ?- stopwatch((mia_domain([1:L,2:L],free),\+ iff(\+ ed_win(W,D), \+ (swf(F,arrow(l)),\+ dictator(_,F),essential_swf(F)) ));true,T). % time elapsed (sec): 171.61 L = _G158 W = _G172 D = _G173 F = _G179 T = 171.61 Yes % OBSERVATION. For common (symmetric) admissible domains, % every Arrovian SWF is monotonic. ?- stopwatch((mia_domain([1:L,2:L],free), swf(F,arrow(l)),\+ mono_swf(F));true,T). % time elapsed (sec): 116.25 L = _G158 F = _G174 T = 116.25 Yes % OBSERVATION. Dominance-based SWF provide the equivalent results % on behalf of the essentiality. ?- stopwatch((mia_domain([1:L,2:L],free),\+ iff(\+ ed_win(W,D), \+ (swf(F,arrow(l)),\+ dictator(_,F),em_swf(F)) ));true,T). % time elapsed (sec): 172.218 L = _G161 W = _G175 D = _G176 F = _G182 T = 172.218 Yes % OBSERVATION. Monotonicity implied by IIA-Pareto SWF ?- stopwatch((mia_domain([1:L,2:R],free),L@ (monotone) essential swf exists. ?- stopwatch((mia_domain([1:L,2:R],free),L@ nondictatorial swf exists % In asymmetric admissible domains, essential decomposability % is sufficient (but not necessary) for the exsistence of % a non-dictatorial Arrovian SWF. ?- stopwatch((mia_domain([1:L,2:R],free),L@[+, -, -])] Yes % NOTE: Because of a violation to the 3rd condition under bi-singlton % domain (L,R) above, it (F) can not be an essential swf. % DEBUG. A counter example against that (e.d. <- essential swf)?? % ---the result below was caused by % former codes of both c_agree_rr and c_meet/2. % individual admissible domain consists of (or contains) % two latin squares. ?- L = [[+, +, +], [-, -, +], [+, -, -]], R = [[-, +, +], [+, +, -], [-, -, -]], mia_domain([1:L,2:R],free),L@[+, +, +]), ([[-, -, +], [-, +, +]]->[-, +, +]), ([[+, -, -], [-, +, +]]->[+, +, +]), ([[+, +, +], [+, +|...]]->[+, +, +]), ([[-, -|...], [+|...]]->[+, +, +]), ([[+|...], [...|...]]->[+, +|...]), ([[...|...]|...]->[+|...]), ([...|...]->[...|...]), (... ->...)] Yes ?- % DEBUG. After correction for c_meet, the code below has intended % to generate the xy-winning coalitions as the decisive set. ?- L = [[+, +, +], [-, -, +], [+, -, -]], R = [[-, +, +], [+, +, -], [-, -, -]], mia_domain([1:L,2:R],free),swf(F,arrow(l)),essential_swf(F), gen_em_win(W,F),display_win_xy(W),!,fail. 1.(a, b):[[1], [2], [1, 2]] 2.(a, c):[[1], [2], [1, 2]] 3.(b, c):[[1], [2], [1, 2]] 4.(b, a):[[1], [2], [1, 2]] 5.(c, a):[[1], [2], [1, 2]] 6.(c, b):[[1], [2], [1, 2]] No ?- not_ed(A,B,C). A = 1 B = a, b C = [1], [2] Yes ?- % DEBUG. before the revision, the following results has come % by same code as above. ?- L = [[+, +, -], [+, -, -]],R = [[+, -, -], [-, -, -]], mia_domain([1:L,2:R],free), \+ (swf(F,arrow(l)),mono_swf(F),essential_swf(F)), ed_win(W,D),display_win_xy(W),nl,write(D). (a, b):[[1, 2], [2]] (a, c):[[1, 2], [2]] (b, c):[[1, 2], [1], [2]] (b, a):[[1, 2], [1], [2]] (c, a):[[1, 2], [1], [2]] (c, b):[[1, 2], [1], [2]] [ (a, b), (a, c), (b, c), (b, a), (c, a), (c, b)] L = [[+, +, -], [+, -, -]] R = [[+, -, -], [-, -, -]] F = _G180 W = [ (a, b):[[1, 2], [2]], (a, c):[[1, 2], [2]], (b, c):[[1, 2], [1], [2]], (b, a):[[1, 2], [1], [2]], (c, a):[[1, 2], [1], [...]], (c, b):[[1|...], [...]|...]] D = [ (a, b), (a, c), (b, c), (b, a), (c, a), (c, b)] Yes ?- (...try and error, many times ) % ADDENDUM. proving for domains of equal-length (a result) ?- restricted_domain(L,l,2). L = [[+, +, +], [-, +, +]] Yes ?- stopwatch((mia_domain(L,len(N)), \+ iff(\+ ed_win(W,D),\+ (swf(F,arrow(l)),\+ dictator(_,F))));true,T). % time elapsed (sec): 93.188 L = _G159 N = _G157 W = _G162 D = _G163 F = _G169 T = 93.188 Yes ?- */ %------------- % another derived social ordering (SWF) based on dominance relation : % xy iff there is no Wxy which contains coalition via which y dominates x. t_swf([],[]). t_swf([RR->Q|F],[RR|L]):- t_swf(F,L),axiom_t_swf(RR->Q). t_swf(F):-all_rr(L),t_swf(F,L). % axioms for transitive swf axiom_t_swf(RR->Q):- o(Q), \+ (dop((X,Y)),\+ iff(\+ c_agree(_,(Y,X),RR),r((X,Y),Q))). % demo /* ?- t_swf(F),display_swf_t2(F),fail. swf:row col |ACITZN ab|+--++- ac|++-+-- bc|+++--- -------------------------------------------------- [+, +, +]=A |ABEJMO +|+00++0 +|++0+00 +|+++000 [-, +, +]=C |BCFKOP -|0--00- +|++0+00 +|+++000 [-, -, +]=I |EFIORS -|0--00- -|00-0-- +|+++000 [+, +, -]=T |JKOTWX +|+00++0 +|++0+00 -|000--- [+, -, -]=Z |MORWZn +|+00++0 -|00-0-- -|000--- [-, -, -]=N |OPSXnN -|0--00- -|00-0-- -|000--- No ?- */ %------------- % Necessary and sufficient condition of transitivity % for dominance relations (See Kaneko(1975)) % DEF. For a triple t=(X,Y,Z), W_t (resp. k_t) is the collection % of dominative coalitions (resp. dominance relations) % for all pairs of X, Y, Z. dop_in_triple((U,V),(X,Y,Z)):- dop((U,V)),subset([U,V],[X,Y,Z]). d_pair_in_triple((U,V),(X,Y,Z)):- d_pair((U,V)),subset([U,V],[X,Y,Z]). all_dop_in_triple(L,T):- dot(T),findall(U,dop_in_triple(U,T),L). all_d_pairs_in_triple(L,T):- dot(T),findall(U,d_pair_in_triple(U,T),L). % dominance relation 3: agreed preferences in a winning coalition w_dom(C,(X,Y),RR,+):- c_agree_rr(C,(X,Y),RR),winning(C). w_dom(C,(X,Y),RR,-):- w_dom(C,(Y,X),RR,+). w_dom(C,(X,Y),RR):- w_dom(C,(Y,X),RR,+). % transitivity of dominance relation w_dom trans_w_dom(RR,B):- rr(RR),findall(X>Y,w_dom(_,(X,Y),RR),B1),sort(B1,B),trans(B). intrans_w_dom(RR,B,T):- rr(RR),findall(X>Y,w_dom(_,(X,Y),RR),B1),sort(B1,B),intrans(T,B). % derived preference relation r_dom((X,Y),RR):- rr(RR),dop((X,Y)),\+ w_dom(_,(Y,X),RR,+). % CLAIM. % r_dom can be seen as a variant of Arrovian swf on admissible domains. % And it is nondictatorial if \+ w_dom([J],XY,RR,+). % transitivity of r_dom trans_r_dom(RR,B):- rr(RR),findall(X>Y,r_dom((X,Y),RR),B),trans(B). intrans_r_dom(RR,B,T):- rr(RR),findall(X>Y,r_dom((X,Y),RR),B),intrans(T,B). w_t_r(_,_,[],[],[]). w_t_r((X,Y,Z),R,[S:XY:C|K],W,[XY|L]):- w_t_r((X,Y,Z),R,K,W0,L),w_dom(C,XY,R,S), (oof(C,W0)->W=W0;W=[C|W0]). w_t_r((X,Y,Z),R,K,W,[XY|L]):- w_t_r((X,Y,Z),R,K,W,L),\+ w_dom(_,XY,R,_). w_t(XYZ,R,K,W):- all_d_pairs_in_triple(L,XYZ),w_t_r(XYZ,R,K,W,L). % demo /* ?- init_me. (...) Yes ?- gen_win(W). W = [[1, 2], [1], [2]] Yes ?- w_t((a,b,c),R,K,W),length(W,N). R = [[+, +, +], [+, +, +]] K = [+ : (a, b):[1, 2], + : (a, c):[1, 2], + : (b, c):[1, 2]] W = [[1, 2]] N = 1 ; R = [[+, +, +], [+, +, +]] K = [+ : (a, b):[1], + : (a, c):[1, 2], + : (b, c):[1, 2]] W = [[1], [1, 2]] Yes ?- make_n_agents(3). Yes ?- w_t((a,b,c),R,K,W),length(W,N). R = [[+, +, +], [+, +, +], [+, +, +]] K = [+ : (a, b):[1, 2], + : (a, c):[1, 2], + : (b, c):[1, 2]] W = [[1, 2]] N = 1 ; R = [[+, +, +], [+, +, +], [+, +, +]] K = [+ : (a, b):[1], + : (a, c):[1, 2], + : (b, c):[1, 2]] W = [[1], [1, 2]] N = 2 ; Yes % REMARK. W_t has at most three coalitions (Kaneko(1975), p.387) ?- w_t((a,b,c),R,K,W),length(W,N),N>3. No ?- */ % DEF. For a triple t=(X,Y,Z), % U_t is an empty set if W_t is a singlton set or an empty set; % if W_t consists of two dominative coalitions, then the union; % if W_t consists of three dominative coalitions, then the union of % the meet of each pair of dominative coalitions. u_t((T,RR,WL),WT,U):- w_t(T,RR,WL,WT),u_t_1(WT,U). u_t_1([],[]). u_t_1([_],[]). u_t_1([S,T],U):- c_union([S,T],U). u_t_1([S,T,V],U):- c_meet([S,T],ST),c_meet([T,V],TV),c_meet([V,S],VS), c_union([ST,TV,VS],U). % Condition T (Condition 2.5 in Kaneko(1975)): % for any distinct triple of alternatives t=(X,Y,Z), one of the % following conditions is true for every agent in U_t. % (1) Some A in {X,Y,Z} is not worst in the triple. That is one % of the remaining two is strictly preferred to A. % (2) Some A in {X,Y,Z} is not best in the triple. That is A % is strictly preferred to one of the remaining two. oof_triple(A,T):- dot(T),T=(X,Y,Z),oof(A,[X,Y,Z]). % Condition T for the transitivity of dominance relations % where value/4 from drsc06 t_value((RR,T,U),-Value,A):- u_t((T,RR,_),_,U), oof(Value,[worst,best]),oof_triple(A,T), \+ (oof(J,U),r_j(J,RR,R),value(Value:A,T,R)). t_value(fail,(RR,T)):- rr(RR),d_triple(T), \+ t_value((RR,T,_),_,_). t_value(RR):- rr(RR),\+ t_value(fail,(RR,_)). % THEOREM (Kaneko,1975). % Assume a proper (monotone) simple game. The dominance relation % (w_dom_rr in our implementation) is transitive % iff Condition T holds. % demo /* ?- display_domain. current domain: ACITZN [base domain=l:linear] Yes ?- make_n_agents(2). Yes ?- init_r_admission. Yes ?- r_j_admission(J,R),name_domain(S,R),nl,write(J:S),fail. 1:ACITZN 2:ACITZN No ?- gen_win(W). W = [[1, 2], [1], [2]] Yes ?- trans_w_dom(RR,B),nl,write(RR:B),fail. [[+, +, +], [+, +, +]]:[b>a, c>a, c>b] [[-, +, +], [+, +, +]]:[b>a, c>a, c>b, a>b] [[+, +, -], [+, +, +]]:[b>a, c>a, c>b, b>c] [[-, -, -], [+, +, +]]:[b>a, c>a, c>b, a>b, a>c, b>c] [[+, +, +], [-, +, +]]:[b>a, c>a, c>b, a>b] [[-, +, +], [-, +, +]]:[c>a, c>b, a>b] [[-, -, +], [-, +, +]]:[c>a, c>b, a>b, a>c] [[+, -, -], [-, +, +]]:[b>a, c>a, c>b, a>b, a>c, b>c] [[-, +, +], [-, -, +]]:[c>a, c>b, a>b, a>c] [[-, -, +], [-, -, +]]:[c>b, a>b, a>c] [[+, +, -], [-, -, +]]:[b>a, c>a, c>b, a>b, a>c, b>c] [[-, -, -], [-, -, +]]:[c>b, a>b, a>c, b>c] [[+, +, +], [+, +, -]]:[b>a, c>a, c>b, b>c] [[-, -, +], [+, +, -]]:[b>a, c>a, c>b, a>b, a>c, b>c] [[+, +, -], [+, +, -]]:[b>a, c>a, b>c] [[+, -, -], [+, +, -]]:[b>a, c>a, a>c, b>c] [[-, +, +], [+, -, -]]:[b>a, c>a, c>b, a>b, a>c, b>c] [[+, +, -], [+, -, -]]:[b>a, c>a, a>c, b>c] [[+, -, -], [+, -, -]]:[b>a, a>c, b>c] [[-, -, -], [+, -, -]]:[b>a, a>b, a>c, b>c] [[+, +, +], [-, -, -]]:[b>a, c>a, c>b, a>b, a>c, b>c] [[-, -, +], [-, -, -]]:[c>b, a>b, a>c, b>c] [[+, -, -], [-, -, -]]:[b>a, a>b, a>c, b>c] [[-, -, -], [-, -, -]]:[a>b, a>c, b>c] No ?- gen_win(W). W = [[1, 2], [1], [2]] ; W = [[1, 2], [1]] Yes ?- trans_w_dom(RR,B),nl,write(RR:B),fail. [[+, +, +], [+, +, +]]:[b>a, c>a, c>b] [[-, +, +], [+, +, +]]:[c>a, c>b, a>b] [[-, -, +], [+, +, +]]:[c>b, a>b, a>c] [[+, +, -], [+, +, +]]:[b>a, c>a, b>c] [[+, -, -], [+, +, +]]:[b>a, a>c, b>c] [[-, -, -], [+, +, +]]:[a>b, a>c, b>c] [[+, +, +], [-, +, +]]:[b>a, c>a, c>b] [[-, +, +], [-, +, +]]:[c>a, c>b, a>b] [[-, -, +], [-, +, +]]:[c>b, a>b, a>c] [[+, +, -], [-, +, +]]:[b>a, c>a, b>c] [[+, -, -], [-, +, +]]:[b>a, a>c, b>c] [[-, -, -], [-, +, +]]:[a>b, a>c, b>c] [[+, +, +], [-, -, +]]:[b>a, c>a, c>b] [[-, +, +], [-, -, +]]:[c>a, c>b, a>b] [[-, -, +], [-, -, +]]:[c>b, a>b, a>c] [[+, +, -], [-, -, +]]:[b>a, c>a, b>c] [[+, -, -], [-, -, +]]:[b>a, a>c, b>c] [[-, -, -], [-, -, +]]:[a>b, a>c, b>c] [[+, +, +], [+, +, -]]:[b>a, c>a, c>b] [[-, +, +], [+, +, -]]:[c>a, c>b, a>b] [[-, -, +], [+, +, -]]:[c>b, a>b, a>c] [[+, +, -], [+, +, -]]:[b>a, c>a, b>c] [[+, -, -], [+, +, -]]:[b>a, a>c, b>c] [[-, -, -], [+, +, -]]:[a>b, a>c, b>c] [[+, +, +], [+, -, -]]:[b>a, c>a, c>b] [[-, +, +], [+, -, -]]:[c>a, c>b, a>b] [[-, -, +], [+, -, -]]:[c>b, a>b, a>c] [[+, +, -], [+, -, -]]:[b>a, c>a, b>c] [[+, -, -], [+, -, -]]:[b>a, a>c, b>c] [[-, -, -], [+, -, -]]:[a>b, a>c, b>c] [[+, +, +], [-, -, -]]:[b>a, c>a, c>b] [[-, +, +], [-, -, -]]:[c>a, c>b, a>b] [[-, -, +], [-, -, -]]:[c>b, a>b, a>c] [[+, +, -], [-, -, -]]:[b>a, c>a, b>c] [[+, -, -], [-, -, -]]:[b>a, a>c, b>c] [[-, -, -], [-, -, -]]:[a>b, a>c, b>c] No ?- gen_win([[1]]). Yes ?- trans_w_dom(RR,B),nl,write(RR:B),fail. [[+, +, +], [+, +, +]]:[b>a, c>a, c>b] [[-, +, +], [+, +, +]]:[a>b, c>a, c>b] [[-, -, +], [+, +, +]]:[a>b, a>c, c>b] [[+, +, -], [+, +, +]]:[b>a, b>c, c>a] [[+, -, -], [+, +, +]]:[a>c, b>a, b>c] [[-, -, -], [+, +, +]]:[a>b, a>c, b>c] [[+, +, +], [-, +, +]]:[b>a, c>a, c>b] [[-, +, +], [-, +, +]]:[a>b, c>a, c>b] [[-, -, +], [-, +, +]]:[a>b, a>c, c>b] [[+, +, -], [-, +, +]]:[b>a, b>c, c>a] [[+, -, -], [-, +, +]]:[a>c, b>a, b>c] [[-, -, -], [-, +, +]]:[a>b, a>c, b>c] [[+, +, +], [-, -, +]]:[b>a, c>a, c>b] [[-, +, +], [-, -, +]]:[a>b, c>a, c>b] [[-, -, +], [-, -, +]]:[a>b, a>c, c>b] [[+, +, -], [-, -, +]]:[b>a, b>c, c>a] [[+, -, -], [-, -, +]]:[a>c, b>a, b>c] [[-, -, -], [-, -, +]]:[a>b, a>c, b>c] [[+, +, +], [+, +, -]]:[b>a, c>a, c>b] [[-, +, +], [+, +, -]]:[a>b, c>a, c>b] [[-, -, +], [+, +, -]]:[a>b, a>c, c>b] [[+, +, -], [+, +, -]]:[b>a, b>c, c>a] [[+, -, -], [+, +, -]]:[a>c, b>a, b>c] [[-, -, -], [+, +, -]]:[a>b, a>c, b>c] [[+, +, +], [+, -, -]]:[b>a, c>a, c>b] [[-, +, +], [+, -, -]]:[a>b, c>a, c>b] [[-, -, +], [+, -, -]]:[a>b, a>c, c>b] [[+, +, -], [+, -, -]]:[b>a, b>c, c>a] [[+, -, -], [+, -, -]]:[a>c, b>a, b>c] [[-, -, -], [+, -, -]]:[a>b, a>c, b>c] [[+, +, +], [-, -, -]]:[b>a, c>a, c>b] [[-, +, +], [-, -, -]]:[a>b, c>a, c>b] [[-, -, +], [-, -, -]]:[a>b, a>c, c>b] [[+, +, -], [-, -, -]]:[b>a, b>c, c>a] [[+, -, -], [-, -, -]]:[a>c, b>a, b>c] [[-, -, -], [-, -, -]]:[a>b, a>c, b>c] No ?- gen_win(W),nl,display_win,nl, intrans_w_dom(RR,B,T),name_domain(S,RR),write(S),write(;),fail. [1, 2];[1];[2]; IA;ZA;TC;NC;AI;ZI;CT;NT;AZ;IZ;CN;TN; [1, 2];[1]; [1, 2];[2]; [1, 2]; [1];[2]; IA;ZA;TC;NC;AI;ZI;CT;NT;AZ;IZ;CN;TN; [1]; [2]; No ?- gen_win(W,[proper:yes]),nl,display_win,nl, intrans_w_dom(RR,B,T),name_domain(S,RR),write(S),write(;),fail. [1, 2];[1]; [1, 2];[2]; [1, 2]; [1]; [2]; No ?- gen_win(W,[monotonic:yes,proper:yes]),nl,display_win,nl, intrans_w_dom(RR,B,T),name_domain(S,RR),write(S),write(;),fail. [1, 2];[1]; [1, 2];[2]; [1, 2]; No ?- mia_domain([1:L,2:R],free), gen_win(W,[proper:yes]),\+ intrans_r_dom(_,_,_). L = [[-, -, -]] R = [[-, -, -]] W = [[1, 2], [1]] Yes ?- t_value(fail,_). No ?- mia_domain([1:L,2:R],free),L@=c, b>c] A = _G196 Yes ?- mia_domain([1:L,2:R],free),L@=c, b>c] A = _G196 B = _G200 No ?- */ % An additional observation of transitivity. /* ?- L = [[+, +, -]],R = [[-, -, -]],W = [[1, 2], [1]], mia_domain([1:L,2:R],free),L@= Condition T. ?- stopwatch(( mia_domain([1:L,2:R],free),L@=b, a>c, b>a, b>c, c>a] XYZ = [c, a, b] Time = 1.344 Yes ?- W = [[1, 2, 3], [1, 2], [1], [2]], gen_win(W,[monotonic:yes,proper:yes]). No ?- % a proof of only-if paet when n=3 %(12 Jan 2007. I used a relatively slow machine in the experiment.) ?- stopwatch(( mia_domain([1:L,2:R,3:S],free),L@= Condition T. ?- stopwatch(( mia_domain([1:L,2:R],free),L@=b, a>c, b>a, c>a, c>b] XYZ = [b, a, c] T = 0.0469999 Yes ?- w_dom(C,X,L,+). C = [1, 2] X = c, b L = [[+, +, -], [-, -, -]] ; No ?- stopwatch(( mia_domain([1:L,2:R],free),L@=b, a>c, b>a, c>a, c>b] XYZ = [b, a, c] T = 0.0469999 Yes ?- w_dom(C,X,L,+). C = [1, 2] X = c, b L = [[+, +, -], [-, -, -]] ; No ?- w_t((a,b,c),R,K,W),length(W,N). R = [[+, +, -], [-, -, -]] K = [- : (b, c):[1, 2]] W = [[1, 2]] N = 1 ; No ?- u_t(((a,b,c),R,K),W,U). R = [[+, +, -], [-, -, -]] K = [- : (b, c):[1, 2]] W = [[1, 2]] U = [] Yes ?- gen_win(W),nl,display_win,nl, intrans_r_dom(RR,B,T),name_domain(S,RR),write(S),write(;),fail. [1, 2];[1];[2]; [1, 2];[1]; [1, 2];[2]; [1, 2]; TN; [1];[2]; [1]; [2]; No ?- */ % Other observations about r_dom and its transitivity /* ?- init_r_admission. Yes ?- display_win. [1, 2];[1];[2]; Yes ?- trans_r_dom(RR,B),nl,write(RR:B),fail. [[+, +, +], [+, +, +]]:[a>b, a>c, b>c] [[-, +, +], [+, +, +]]:[a>c, b>c] [[-, -, +], [+, +, +]]:[b>c] [[+, +, -], [+, +, +]]:[a>b, a>c] [[+, -, -], [+, +, +]]:[a>b] [[-, -, -], [+, +, +]]:[] [[+, +, +], [-, +, +]]:[a>c, b>c] [[-, +, +], [-, +, +]]:[a>c, b>c, b>a] [[-, -, +], [-, +, +]]:[b>c, b>a] [[+, +, -], [-, +, +]]:[a>c] [[+, -, -], [-, +, +]]:[] [[-, -, -], [-, +, +]]:[b>a] [[+, +, +], [-, -, +]]:[b>c] [[-, +, +], [-, -, +]]:[b>c, b>a] [[-, -, +], [-, -, +]]:[b>c, b>a, c>a] [[+, +, -], [-, -, +]]:[] [[+, -, -], [-, -, +]]:[c>a] [[-, -, -], [-, -, +]]:[b>a, c>a] [[+, +, +], [+, +, -]]:[a>b, a>c] [[-, +, +], [+, +, -]]:[a>c] [[-, -, +], [+, +, -]]:[] [[+, +, -], [+, +, -]]:[a>b, a>c, c>b] [[+, -, -], [+, +, -]]:[a>b, c>b] [[-, -, -], [+, +, -]]:[c>b] [[+, +, +], [+, -, -]]:[a>b] [[-, +, +], [+, -, -]]:[] [[-, -, +], [+, -, -]]:[c>a] [[+, +, -], [+, -, -]]:[a>b, c>b] [[+, -, -], [+, -, -]]:[a>b, c>a, c>b] [[-, -, -], [+, -, -]]:[c>a, c>b] [[+, +, +], [-, -, -]]:[] [[-, +, +], [-, -, -]]:[b>a] [[-, -, +], [-, -, -]]:[b>a, c>a] [[+, +, -], [-, -, -]]:[c>b] [[+, -, -], [-, -, -]]:[c>a, c>b] [[-, -, -], [-, -, -]]:[b>a, c>a, c>b] No ?- trans_r_dom(RR,[]),!,w_dom(C,XY,RR,+),nl,write(RR:C:XY),fail. [[-, -, -], [+, +, +]]:[2]: (a, b) [[-, -, -], [+, +, +]]:[2]: (a, c) [[-, -, -], [+, +, +]]:[2]: (b, c) [[-, -, -], [+, +, +]]:[1]: (b, a) [[-, -, -], [+, +, +]]:[1]: (c, a) [[-, -, -], [+, +, +]]:[1]: (c, b) No ?- trans_r_dom(RR,[]),!,c_agree_rr(C,XY,RR),nl,write(RR:XY:C),fail. [[-, -, -], [+, +, +]]: (a, b):[2] [[-, -, -], [+, +, +]]: (a, c):[2] [[-, -, -], [+, +, +]]: (b, c):[2] [[-, -, -], [+, +, +]]: (b, a):[1] [[-, -, -], [+, +, +]]: (c, a):[1] [[-, -, -], [+, +, +]]: (c, b):[1] No ?- intrans_r_dom(RR,B,V),name_domain(S,RR),nl,write(S:V),fail. No ?- gen_win(W),nl,display_win,nl, intrans_r_dom(RR,B,T),name_domain(S,RR),write(S),write(;),fail. [1, 2];[1];[2]; [1, 2];[1]; [1, 2];[2]; [1, 2]; IA;ZA;TC;NC;AI;ZI;CT;NT;AZ;IZ;CN;TN; [1];[2]; [1]; [2]; No ?- gen_win(W,[proper:yes]),nl,display_win,nl, intrans_r_dom(RR,B,T),name_domain(S,RR),write(S),write(;),fail. [1, 2];[1]; [1, 2];[2]; [1, 2]; IA;ZA;TC;NC;AI;ZI;CT;NT;AZ;IZ;CN;TN; [1]; [2]; No ?- mia_domain([1:L,2:R],free), gen_win(W,[proper:yes]),\+ intrans_r_dom(_,_,_). L = [[-, -, -]] R = [[-, -, -]] W = [[1, 2], [1]] Yes ?- t_value(fail,_). No ?- mia_domain([1:L,2:R],free),L@=