% arrow52.pl
% 28 Feb 2010


% preference ordering
p( x, y, i).
p( y, x, n-i).
p( y, z, n).

p( Y, Z, i):-  p( Y, Z, n).
p( Y, Z, n-i):-  p( Y, Z, n).

p( x, z, i). % by transitivity

p( x, y, s):- p( x, y, i), p( y, x, n-i). % assumption
p( Y, Z, s):- p( Y, Z, n). % Pareto condition
p( X, Z, s):- p( X, Y, s), p( Y, Z, s). % transitivity

% Note: a loop if transitivity condition added.

/*
?- U=[X,Y,Z],p(X,Y,Z),nl,write(U),fail.

[x, y, i]
[y, x, n-i]
[y, z, n]
[y, z, i]
[y, z, n-i]
[x, z, i]
false.

?- p(X,Y,s).
X = x,
Y = y ;
X = y,
Y = z ;
X = x,
Y = z ;

*/

% propagation of decisiveness

d( ( X, Y) -> ( X, Z)) :- t( X, Y, Z).
d( ( X, Y) -> ( Z, Y)) :- t( X, Y, Z).

t( X, Y, Z):- permutation( [X,Y,Z], [x,y,z]).

/*

 ?- d(X->Y),d( Y->Z),d( Z->A),d( A->B), d(B->C), sort( [X,Y,Z,A,B,C],L), length(L,6),nl,write([X,Y,Z,A,B,C]),fail.

[ (x, y), (x, z), (y, z), (y, x), (z, x), (z, y)]
[ (y, x), (y, z), (x, z), (x, y), (z, y), (z, x)]
[ (z, x), (z, y), (x, y), (x, z), (y, z), (y, x)]
[ (x, z), (x, y), (z, y), (z, x), (y, x), (y, z)]
[ (y, z), (y, x), (z, x), (z, y), (x, y), (x, z)]
[ (z, y), (z, x), (y, x), (y, z), (x, z), (x, y)]
[ (x, y), (z, y), (z, x), (y, x), (y, z), (x, z)]
[ (y, x), (z, x), (z, y), (x, y), (x, z), (y, z)]
[ (z, x), (y, x), (y, z), (x, z), (x, y), (z, y)]
[ (x, z), (y, z), (y, x), (z, x), (z, y), (x, y)]
[ (y, z), (x, z), (x, y), (z, y), (z, x), (y, x)]
[ (z, y), (x, y), (x, z), (y, z), (y, x), (z, x)]
false.

% This completes the proof of that any
% decisive set for a binary comparison is decisive. 

*/

% alternative program with reasons

% i is assumed to be decisive for x against y.
d( x, y, i).

% decisiveness 
w( X, Y, i):- p( X, Y, i), p( Y, X, n-i), d( X, Y, i).

% Pareto condition
w( Y, Z, n):- p( Y, Z, n).

% transitivity
w( X, Z, t(A,B)):- w( X, Y, A), w( Y, Z, B).

%d_bar( X, Y):- p( X, Y, i), w( X, Y, _). 
%d( X, Y):- p( X, Y, i), p( Y, X, n-i), w( X, Y, _). 

/*

 ?- w(X, Y, Decisive).
X = x,
Y = y,
Decisive = i ;
X = y,
Y = z,
Decisive = n ;
X = x,
Y = z,
Decisive = t(i, n) ;
ERROR: Out of local stack

*/

/*
%
d( x, y).
d( X, Y):- d_bar( X, Y).
d_bar( x, z):- d( x, y).
d_bar( z, y):- d( x, y).
%
d_bar( y, z):- d( x, z).
d_bar( y, x):- d( y, z).
d_bar( y, x):- d( x, y).
%
d_bar( y, z):- d( y, x).
d_bar( z, x):- d( y, x).
d_bar( x, y):- d( y, x).
*/

a( x).
a( y).
a( z).
b( X, Y):- a( X), a( Y).


/*

 ?- b(X,Y),\+ d_bar(X,Y),nl.
X = x,
Y = x ;

X = y,
Y = y ;

X = z,
Y = z.

*/