You selected kglp01.pl

title([
   '%---------------------------------------------------%'
  ,'% logic programming for knowledge and games (KGLP) '
],['%---------------------------------------------------%'
  ,'% file: kglp01.pl'
  ,'% language: SWI-Prolog (Version 5.0.10)'
  ,'% date: 27 Jan -- 4 Feb 2005 (before rationality)'
  ,'% date: 4 -- 17 Feb 2005 (on and after rationality part)'
  ,'% author: Kenryo INDO (Kanto Gakuen University)'
  ,'% reference:'
  ,'% [1] Aumann, R.J. Backward induction and common knowledge.'
  ,'% Games and Economic Behavior 8 (1995): 6-19.'
  ,'% [2] Aumann, R.J. On the centipade game.'
  ,'% Games and Economic Behavior 23 (1998): 97-105.'
]).

initialize_program:-
   title(A,_),fig_game3(B),append(A,B,C),
   forall(member(X,C),(nl,write(X))),
   ['would1.txt'],
   generate_states(_,_,_).

%---------------------------------------------------%
% 1. Perfect information game and inductive choice
%---------------------------------------------------%
% 27 Jan 2005.

% ` the players as attaching automata to their 
% vertices, if reached.' (Aumann(1995), p.12)


/*************************************************
% example 1.
% a two player stage game in Aumann(1995).

%  ann    bob
%  *----->*------>3,3
%  |      |
%  v      v
%  2,2    1,1

player(ann).
player(bob).
vertex(1).
vertex(2).
terminal(1).
terminal(2).
terminal(3).
move(vertex(1),player(ann)).
move(vertex(2),player(bob)).
act(down,vertex(1)->terminal(1)).
act(right,vertex(1)->vertex(2)).
act(down,vertex(2)->terminal(2)).
act(right,vertex(2)->terminal(3)).
payoff(terminal(1),player(ann),2).
payoff(terminal(1),player(bob),2).
payoff(terminal(2),player(ann),1).
payoff(terminal(2),player(bob),1).
payoff(terminal(3),player(ann),3).
payoff(terminal(3),player(bob),3).

*************************************************/


% In the program hereafter, a game below would be focused.

fig_game3([
  '%---------------------------------------------------%'
  ,'% a perfect information game:'
  ,'% Aumann(1995), Game 3.'
  ,''
  ,'%  ann    bob    ann    bob    ann          '
  ,'%  *----->*----->*----->*----->*------>5,8  '
  ,'%  |      |      |      |      |            '
  ,'%  v      v      v      v      v            '
  ,'%  2,1    1,4    4,3    3,6    6,5          '
  ,'%'
]).

player(ann).
player(bob).
vertex(N):-member(N,[1,2,3,4,5]). 
terminal(N):-member(N,[1,2,3,4,5,6]).
last_terminal(6).

move(vertex(N),player(ann)):-member(N,[1,3,5]).
move(vertex(N),player(bob)):-member(N,[2,4]).

act(down,vertex(N)->terminal(N)):-member(N,[1,2,3,4,5]).
act(right,vertex(N)->vertex(N1)):-member(N,[1,2,3,4]),N1 is N + 1.
act(right,vertex(K)->terminal(N)):-last_terminal(N), K is N-1.

payoff(terminal(1),player(ann),2).
payoff(terminal(1),player(bob),1).
payoff(terminal(2),player(ann),1).
payoff(terminal(2),player(bob),4).
payoff(terminal(3),player(ann),4).
payoff(terminal(3),player(bob),3).
payoff(terminal(4),player(ann),3).
payoff(terminal(4),player(bob),6).
payoff(terminal(5),player(ann),6).
payoff(terminal(5),player(bob),5).
payoff(terminal(6),player(ann),5).
%payoff(terminal(6),player(ann),7).
payoff(terminal(6),player(bob),8).


all_vertices(Vs):-
   V=vertex(_),
   findall(V,V,Vs).


% the binary order of vertices
%---------------------------------------------------%

comes_after(W > V):-
   W=vertex(_I),
   V=vertex(_J),
   W, V,
   V \= W,
   \+ (
     play_goes_through(W,X),
     \+ play_goes_through(V,X)
   ).

play_goes_through(W,V):-
   play_goes_through(W,V,_).

play_goes_through(W,W,[]):-
   W=vertex(_),
   W.

play_goes_through(W,V,[A|X]):-
   V=vertex(_J),
   Y=vertex(_K),
   V, Y,
   act(A,Y->V),
   W=vertex(_I),
   W,
   play_goes_through(W,Y,X).


% inductive choice 
%---------------------------------------------------%
% revised: 29 Jan 2005.

% ` (Then) the inductive choice b~v at v is defined as the
% action that maximizes i's payoff when all players make 
% the inductive choices at all vertices after v.'
% (Aumann, 1995 p.8) 


inductive_pattern([(V,Player,act(A),payoff(U))|F],Z):-
   act(A,V->Next),
   inductive_choice(at(Next),F,Z),
   payoff(Z,Player,U).

inductive_pattern([(V,Player,act(Act),payoff(U))],Z):-
   Z=terminal(_),
   final_decision(
     at(V),
     by(Player),
     act(Act),
     payoff(U),
     Z
   ).

inductive_choice(at(V),[X|H],Z):-
   V=vertex(_),
   V,
   Player=player(_),
   move(V,Player),
   Z=terminal(_),
   X=(V,Player,_A,payoff(U)),
   max(U,
     inductive_pattern([X|H],Z)
   ).

final_decision(at(V),by(Player),act(Act),payoff(U),Z):-
   V=vertex(_),
   V,
   Player=player(_),
   move(V,Player),
   Z=terminal(_),
   max(U,
    (
     act(Act,V->Z),
     payoff(Z,Player,U)
    )
   ).


% a solver cited from math1.pl (2004.8.8.)
%---------------------------------------------------%

min(X,Goal):-
  max(Z,(Goal,Z is -X)).

max(X,Goal):-
  % X: the objective variable,
  % Goal: the objective function and constraints,
  setof((X,Goal),Goal,Z),
  member((X,Goal),Z),
  \+ (
    member((Y,_),Z),
    Y > X
  ).


/*************************************************

?- inductive_choice(A,B,C),
   forall(member(X,[[A,C]|B]),(nl,write(X))),fail.

[at(vertex(1)), terminal(1)]
vertex(1), player(ann), act(down), payoff(2)
[at(vertex(2)), terminal(2)]
vertex(2), player(bob), act(down), payoff(4)
[at(vertex(3)), terminal(3)]
vertex(3), player(ann), act(down), payoff(4)
[at(vertex(4)), terminal(4)]
vertex(4), player(bob), act(down), payoff(6)
[at(vertex(5)), terminal(5)]
vertex(5), player(ann), act(down), payoff(6)

No
?- 

% If we change a payoff of ann at the last terminal
% node, to 7, from 5 originally, then the execution
% results as follows.

% payoff(terminal(6),player(ann),7).

?- inductive_choice(A,B,C),
   forall(member(X,[[A,C]|B]),(nl,write(X))),fail.

[at(vertex(1)), terminal(6)]
vertex(1), player(ann), act(right), payoff(7)
vertex(2), player(bob), act(right), payoff(8)
vertex(3), player(ann), act(right), payoff(7)
vertex(4), player(bob), act(right), payoff(8)
vertex(5), player(ann), act(right), payoff(7)
[at(vertex(2)), terminal(6)]
vertex(2), player(bob), act(right), payoff(8)
vertex(3), player(ann), act(right), payoff(7)
vertex(4), player(bob), act(right), payoff(8)
vertex(5), player(ann), act(right), payoff(7)
[at(vertex(3)), terminal(6)]
vertex(3), player(ann), act(right), payoff(7)
vertex(4), player(bob), act(right), payoff(8)
vertex(5), player(ann), act(right), payoff(7)
[at(vertex(4)), terminal(6)]
vertex(4), player(bob), act(right), payoff(8)
vertex(5), player(ann), act(right), payoff(7)
[at(vertex(5)), terminal(6)]
vertex(5), player(ann), act(right), payoff(7)

No
?- 

*************************************************/



% strategy profile of inductive choice 
%---------------------------------------------------%
% added: 5 Feb 2005.

inductive_choice_in_profile(Id,B,D):-
   findall((V,J,A),
     inductive_choice(at(V),[(V,J,A,_)|_],_),
   B),
   findall((N,I,C),
     member((vertex(N),player(I),act(C)),B),
   D),
   strategy_profile(Id,B,D).


/*************************************************

?- inductive_choice_in_profile(Id,B,D).

Id = 1
B = [ (vertex(1), player(ann), act(down)), (vertex(2), player(bob), act(down)), (vertex(3), player(ann), act(down)), (vertex(4), player(bob), act(down)), (vertex(5), player(ann), act(down))]
D = [ (1, ann, down), (2, bob, down), (3, ann, down), (4, bob, down), (5, ann, down)] ;

No
?- 

*************************************************/


% choices at each vertex
%---------------------------------------------------%

choice(at(V),[(V,Player,act(A),payoff(U))|H],Z):-
   V=vertex(_),
   V,
   Player=player(_),
   move(V,Player),
   Z=terminal(_),
   act(A,V->Next),
   choice(at(Next),H,Z),
   payoff(Z,Player,U).

choice(A,H,Z):-
   choice_0(A,H,Z).

choice_0(at(V),[(V,Player,act(Act),payoff(U))],Z):-
   V=vertex(_),
   V,
   Player=player(_),
   move(V,Player),
   Z=terminal(_),
   act(Act,V->Z),
   payoff(Z,Player,U).


/************************************************

?- choice(at(vertex(5)),X,Z).

X = [ (vertex(5), player(ann), act(down), payoff(6))]
Z = terminal(5) ;

X = [ (vertex(5), player(ann), act(right), payoff(5))]
Z = terminal(6) ;

No
?- choice(at(vertex(4)),X,Z).

X = [ (vertex(4), player(bob), act(right), payoff(5)), (vertex(5), player(ann), act(down), payoff(6))]
Z = terminal(5) ;

X = [ (vertex(4), player(bob), act(right), payoff(8)), (vertex(5), player(ann), act(right), payoff(5))]
Z = terminal(6) ;

X = [ (vertex(4), player(bob), act(down), payoff(6))]
Z = terminal(4) ;

No
?- 

************************************************/


% strategies, and their profile
%---------------------------------------------------%

% ` A strategy of Player i is a function s_i that assigns 
% to each vertex v of i an action at that vertex.'
% (Aumann, 1995 p.8)

% a strategy:  Player x Vertices--> Acts
% a strategy profile:
%  collection of choices for each vertex and the player.

strategy_profile_1([],[],[]).

strategy_profile_1([X|H],[V|S],[(K,I,A)|Y]):-
   (var(S)->all_vertices([V|S]);true),
   strategy_profile_1(H,S,Y),
   V=vertex(K),
   act(A,V->_),
   move(V,player(I)),
   X=(vertex(K),player(I),act(A)).

strategy_profile_1(H,Y):-
   all_vertices(VS),
   strategy_profile_1(H,VS,Y).


% strategy_profile/3 
%---------------------------------------------------%
% The predicate hereafter will be used, accompanied with 
% strategy_profile_0/3, in the program consistently.
% edited: 14 Feb 2005.

% Id: id of strategy profile (= the state No.)
% LP: the long profile
% SP: the short profile; [(Vertex_No,Player,Choice)]

strategy_profile(Id,LP,SP):-
   clause(
     strategy_profile_0(Id,LP,SP),
   true).

strategy_profile(Id,LP,SP):-
   \+ clause(
     strategy_profile_0(_,_,_),
   true),
   factualize_strategies,!,
   strategy_profile(Id,LP,SP).


/************************************************

?- strategy_profile_1(A,Y),forall_write_goals(X,(member(X,A))).

(vertex(1), player(ann), act(right), payoff(6)):terminal(5)
(vertex(2), player(bob), act(right), payoff(5)):terminal(5)
(vertex(3), player(ann), act(right), payoff(6)):terminal(5)
(vertex(4), player(bob), act(right), payoff(5)):terminal(5)
(vertex(5), player(ann), act(down), payoff(6)):terminal(5)
complete

A = [ (vertex(1), player(ann), act(right), payoff(6)):terminal(5), (vertex(2), player(bob), act(right), payoff(5)):terminal(5), (vertex(3), player(ann), act(right), payoff(6)):terminal(5), (vertex(4), player(bob), act(right), payoff(5)):terminal(5), (vertex(5), player(ann), act(...), payoff(...)):terminal(5)]
Y = [ (1, ann, right), (2, bob, right), (3, ann, right), (4, bob, right), (5, ann, down)]
X = _G163  ;

(vertex(1), player(ann), act(right), payoff(5)):terminal(6)
(vertex(2), player(bob), act(right), payoff(5)):terminal(5)
(vertex(3), player(ann), act(right), payoff(6)):terminal(5)
(vertex(4), player(bob), act(right), payoff(5)):terminal(5)
(vertex(5), player(ann), act(down), payoff(6)):terminal(5)
complete

A = [ (vertex(1), player(ann), act(right), payoff(5)):terminal(6), (vertex(2), player(bob), act(right), payoff(5)):terminal(5), (vertex(3), player(ann), act(right), payoff(6)):terminal(5), (vertex(4), player(bob), act(right), payoff(5)):terminal(5), (vertex(5), player(ann), act(...), payoff(...)):terminal(5)]
Y = [ (1, ann, right), (2, bob, right), (3, ann, right), (4, bob, right), (5, ann, down)]
X = _G163 

Yes
?- 

*************************************************/



% a script : generating strategy profiles as facts
%---------------------------------------------------%

:- dynamic id_0/1.
:- dynamic strategy_profile_0/3.

update_id_0(ID):-
   retract(id_0(ID_0)),
   ID is ID_0 +1,
   assert(id_0(ID)).

factualize_strategies:-
   abolish(id_0/1),
   abolish(strategy_profile_0/3),
   assert(id_0(0)),
   fail.

factualize_strategies:-
   strategy_profile_1(W,Y),
   update_id_0(ID),
   assert(strategy_profile_0(ID,W,Y)),
   fail.

factualize_strategies:-
   findall(Y,
     strategy_profile_0(_,_,Y),
   L),
   length(L,N),
   findall(Y,
     member(Y,L),
   L1),
   length(L1,N1),
   nl,
   write(complete),
   nl,
   write((total:N,sorted:N1)),
   write(' strategy profiles have asserted.').


/************************************************

?- factualize_strategies.

complete
total:32, sorted:32 strategy profiles have asserted.

Yes
?- findall(Y,
    strategy_profile_0(_,_,Y),L),length(L,N).

Y = _G161
L = [[ (1, ann, right), (2, bob, right), (3, ann, right), (4, bob, right), (5, ann, down)], [ (1, ann, right), (2, bob, right), (3, ann, right), (4, bob, right), (5, ann, down)], [ (1, ann, right), (2, bob, right), (3, ann, right), (4, bob, right), (5, ..., ...)], [ (1, ann, right), (2, bob, right), (3, ann, right), (4, ..., ...), (..., ...)], [ (1, ann, right), (2, bob, right), (3, ..., ...), (..., ...)|...], [ (1, ann, down), (2, ..., ...), (..., ...)|...], [ (1, ..., ...), (..., ...)|...], [ (..., ...)|...], [...|...]|...]
N = 32 

Yes
?- 


*************************************************/




% synonym for strategy profiles
% and conditional choices for down-or-right games
%---------------------------------------------------%
% added : 3 Feb 2005
% revised: 6 Feb 2005

strategy_description(X,C,Name,Name1):-
   strategy_description(X,_,C,Name,Name1).

strategy_description(X,B,C,Name,Name1):-
   (var(C)
    ->strategy_profile(X,B,C)
   ;true),
   findall(A,member((_,_,A),C),Name),
   brief_name_of_strategies_1(Name,Name1).

brief_name_of_strategies_1(Name,Name1):-
   findall(B,
    (
     member(N,Name),
     member((N,B),[(right,r),(down,d)])
    ),
   Name1).

choice_description(At,HB,Z,Name,Name1,Name2):-
   choice(At,HB,Z),
   X= (vertex(V),player(I),act(D),_),
   findall((V,I,D),
    (
     member(X,HB)
    ),
   Name),
   findall(D,member((_,_,D),Name),Name1),
   brief_name_of_strategies_1(Name1,Name2).


/*************************************************

?- strategy_description(X,C,Name,Name1).

X = 1
C = [ (1, ann, down), (2, bob, down), (3, ann, down), (4, bob, down), (5, ann, down)]
Name = [down, down, down, down, down]
Name1 = [d, d, d, d, d] 

Yes
?- choice_description(A,_,C,D,E,F).

A = at(vertex(1))
C = terminal(5)
D = [ (1, ann, right), (2, bob, right), (3, ann, right), (4, bob, right), (5, ann, down)]
E = [right, right, right, right, down]
F = [r, r, r, r, d] ;

A = at(vertex(1))
C = terminal(6)
D = [ (1, ann, right), (2, bob, right), (3, ann, right), (4, bob, right), (5, ann, right)]
E = [right, right, right, right, right]
F = [r, r, r, r, r] 

Yes
?- 

*************************************************/



%---------------------------------------------------%
% conditional payoffs and counterfactuals
%---------------------------------------------------%
% added: 3-4 Feb 2005.
% revised: 16 Feb 2005.

%  A player i's conditional payoff h(i,v)(s)
% for a strategy profile, s, at a vertex, v,
% is defined as his/her payoff at the leaf to which 
% the players are led if starting at v, they play s.
%  But if v is not reached, i's conditional payoff 
% is different from his/her actual payoff.
% (see the test run below.) 

root_of_tree(Root):-
   Root=vertex(_),
   Root,
   \+ comes_after(Root>_W).

track_back_history(V,H):-
   V=vertex(_),
   V,
   root_of_tree(Root),
   play_goes_through(Root,V,H).

strategy_profile_with_time_view(I,H,S,V,Past,Future):-
   strategy_profile(I,H,S),
   V=vertex(_),
   V,
   W=vertex(K),
   X=(K,_,_),
   findall(X,
    (
     member(X,S),
     comes_after(V>W)
    ),
   Past),
   subtract(S,Past,Future).

strategy_profile_after(V,PH,(I,S),Future):-
   strategy_profile_with_time_view(I,_,S,V,Past,Future),
 %% track_back_history(V,PH),  
   X=(_,_,A),
   findall(A,member(X,Past),PH).


conditional_choice_at(V,SP,Z):-
   choice(at(V),H,Z),
   X=(vertex(W),player(JDoe),act(A),_),
   findall((W,JDoe,A),member(X,H),SP).


% revised: 16 Feb 2005.
%  a play history PH should have been a virtual path 
%  at the given starting vertex to which the player would have reached.

conditional_outcome(V,PH,(I,S),Z):-
   conditional_choice_at(V,CCAV,Z),
   strategy_profile_after(V,_PH_in_real,(I,S),SPAV),
   subset(CCAV,SPAV),
   track_back_history(V,PH).

conditional_payoff([V,PH,(I,S),Z],Player,payoff(U)):-
   conditional_outcome(V,PH,(I,S),Z),
   payoff(Z,Player,U).


% three demonstrations about substative consitionals.
/*************************************************

% demonstration (1):
% the history and termination in reality
%---------------------------------------------------%

?- conditional_choice_at(vertex(1),SP,Z).

SP = [ (1, ann, right), (2, bob, right), (3, ann, right), (4, bob, right), (5, ann, down)]
Z = terminal(5) ;

SP = [ (1, ann, right), (2, bob, right), (3, ann, right), (4, bob, right), (5, ann, right)]
Z = terminal(6) ;

SP = [ (1, ann, right), (2, bob, right), (3, ann, right), (4, bob, down)]
Z = terminal(4) ;

SP = [ (1, ann, right), (2, bob, right), (3, ann, down)]
Z = terminal(3) ;

SP = [ (1, ann, right), (2, bob, down)]
Z = terminal(2) ;

SP = [ (1, ann, down)]
Z = terminal(1) ;

No
?-

/*************************************************



*************************************************/

% demonstration (2):
% some substantive conditional outcomes (and payoffs)
% not but that they are consistent with the realities
%---------------------------------------------------%


?- conditional_outcome(vertex(1),PH,(I,CS),Z),
strategy_description(I,_,S,_).

PH = []
I = 16
CS = [ (1, ann, right), (2, bob, right), (3, ann, right), (4, bob, right), (5, ann, down)]
Z = terminal(5)
S = [right, right, right, right, down] ;

PH = []
I = 32
CS = [ (1, ann, right), (2, bob, right), (3, ann, right), (4, bob, right), (5, ann, right)]
Z = terminal(6)
S = [right, right, right, right, right] 

PH = []
I = 8
CS = [ (1, ann, right), (2, bob, right), (3, ann, right), (4, bob, down), (5, ann, down)]
Z = terminal(4)
S = [right, right, right, down, down] 

Yes
?- findall(I,conditional_outcome(vertex(1),_,(I,_),_),L),
sort(L,L1),event_description(L1,N,P),hexa_event(L1,_,HX).

I = _G162
L = [16, 32, 8, 24, 4, 12, 20, 28, 2|...]
L1 = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
N = 32
P = [[down, right], [down, right], [down, right], [down, right], [down, right]]
HX = ffffffff 

Yes
?- 

/*************************************************



*************************************************/

% demonstration (3):
% counterfactuals 
%---------------------------------------------------%
% `When v is not reached, the value of conditional payoff 
% may different from that of his/her actual payoff. '
% (Aumann,1995 footnote 3).

% For example, the backtrackings of conditional_payoff/3 
% if vertex 5 were reached shown below, yield
% counterfactual payoffs 6 and 5 to ann and bob 
% respectively but 2 and 1 in reality since a down 
% was chosen by ann at her first vertex (under 
% the true strategy profile 1).


?- conditional_payoff([vertex(5),PH,(I,CS),Z],Player,Payoff),
strategy_description(I,_,S,_).

PH = [right, right, right, right]
I = 1
CS = [ (1, ann, down), (2, bob, down), (3, ann, down), (4, bob, down), (5, ann, down)]
Z = terminal(5)
Player = player(ann)
Payoff = payoff(6)
S = [down, down, down, down, down] ;

PH = [right, right, right, right]
I = 1
CS = [ (1, ann, down), (2, bob, down), (3, ann, down), (4, bob, down), (5, ann, down)]
Z = terminal(5)
Player = player(bob)
Payoff = payoff(5)
S = [down, down, down, down, down] ;

Yes
?- 

*************************************************/



%---------------------------------------------------%
% 2. State space for perfect information games 
%---------------------------------------------------%
% 28-29,31 Jan 2005.

% revised : 17 Feb 2005 

:- dynamic all_states_0/1.

generate_states(A,X,N):-
   findall(W,strategy_profile(W,_,_),O),
   event_templete(A,X,N,O),
   abolish(all_states_0/1),
   assert(all_states_0(A)).

% Note:
% event_templete/3 is a similar vein of event/3
% instead of subset_of(A,N,O) which is not efficient for a longer list.
% But until the state setup done, you must use it.
% Where no state is, there the event goes out.


event_templete(A,X,N,O):-
   var(A),
   length(O,L),
   choose_N_units_among(L,N,X),
   list_projection(X,O,A).

event_templete(A,X,N,O):-
   \+ var(A),
   list_projection(X,O,A),
   length(A,N).


state(W):-clause(all_states_0(A),_),member(W,A).

%state(W):-member(W,[1,2,3,4]). % for a debug.

%state(1). % a trivial case of non-empty CKR, in Theorem B.

%state(W):-strategy_profile(W,_,_).  % full states which consist of all profiles.



state_description(W,D):-
   state(W),
   strategy_profile(W,_,D).

% revised: 14 Feb
% transfered the jurisdication to strategy_profile/3.
% old:
  % state(W):-
  %  (clause(strategy_profile_0(_,_,_),_)
  %   ->true; factualize_strategies)),
  %  strategy_profile_0(W,_,_).
  %
  % state_description(W,D):-
  %   strategy_profile_0(W,_,D).

% added : 3 Feb 2005. state_description/3.

state_description(W,S,C):-
   strategy_description(W,S,_,C).

all_states(S):-
   X=state(I),
   findall(I,X,S).



/*************************************************

?- state(W).

W = 1 ;

W = 2 

Yes
?- findall(W,state(W),L),length(L,N).

W = _G160
L = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
N = 32 

Yes
?- state_description(A,B).

A = 1
B = [ (1, ann, down), (2, bob, down), (3, ann, down), (4, bob, down), (5, ann, down)] 

Yes
?- state_description(A,B,C).

A = 1
B = [ (1, ann, down), (2, bob, down), (3, ann, down), (4, bob, down), (5, ann, down)]
C = [d, d, d, d, d] ;

A = 2
B = [ (1, ann, right), (2, bob, down), (3, ann, down), (4, bob, down), (5, ann, down)]
C = [r, d, d, d, d] 

Yes
?- 


*************************************************/


% events 
%---------------------------------------------------%%
% revised: 31 Jan 2005.

% naive versions
%----------------

event_def(E):-
   all_states(O),
   subset(E,O).

event_def_0(E):-
   all_states(O),
   subset_of(E,_N,O).


% computationally improved versions
%-----------------------------------

event(E):-
   var(E),
   event(E,_N).

event(E):-
   \+ var(E),
   event_def(E).

% generating a list of the given length
%--------------------------------------

event(E,N):-
   \+ var(E),
   event_def(E),
   length(E,N).

event(E,N):-
   var(E),
   event(E,_P,N).

event(E,P,N):-
   \+ var(E),
   all_states(O),
   list_projection(P,O,E),
   length(E,N).

event(E,P,N):-
   var(E),
   all_states(O),
   length(O,U),
   choose_N_units_among(U,N,P),
   list_projection(P,O,E).


% other naive versions for events
%--------------------------------

% ascending order version

event_1_a(E,N):-
   all_states(O),
   event_1_a(E,O,N).

event_1_a([],[],0).
event_1_a(E,[S|O],N):-
   event_1_a(E,O,N),
   state(S).
event_1_a([S|E],[S|O],N1):-
   event_1_a(E,O,N),
   state(S),
   N1 is N + 1.

% descending order version

event_1_d(E):-
   all_states(O),
   event_1_d(E,O,_).

event_1_d([],[],0).
event_1_d([C|B],[C|A],N):-
   event_1_d(B,A,N1),
   N is N1 + 1.
event_1_d(B,[_|A],N):-
   event_1_d(B,A,N).



% computing event from strategic description.
%----------------------------------
% added: 14 Feb 2005


event_description_1(E,D,Hx,CD):-
   var(D),
   CD=[_X1,_X2,_X3,_X4,_X5],
   findall(W,state_description(W,_,CD),E),
   event_description(E,_,D),
   hexa_event(E,_,Hx).


/*************************************************

?- event_description_1(E,D,Hx,[r,d|_]).

E = [2, 6, 10, 14, 18, 22, 26, 30]
D = [[right], [down], [down, right], [down, right], [down, right]]
Hx = '44444444' ;

No
?-

*************************************************/


% event description via straytegies 
%----------------------------------
% 3 Feb 2005

% E: an event
% N: the cardinality 
% D: the strategic description


event_description(E,N,D):-
   strategy_profiles_in_event(E,N,Profiles),
   findall(V,vertex(V),SV),
   collect_actions_for_vertices(SV,Profiles,D).

% Caution: 
% You had better to use event/3, or event/2,
% in order to generate a specific length of event.
% If such is the case, especially of long list,
% we won't recommend you try (to) event_description/3 below.


strategy_profiles_in_event(E,N,Profiles):-
   event(E,_XE,N),
   findall(S,
    (
     member(I,E),
     strategy_profile(I,_,S)
    ),
   Collection),
   flatten(Collection,Profiles).

collect_actions_for_a_vertex(V,Profiles,Collection,Acts):-
   \+ var(Profiles),
   vertex(V),
   findall(A,
    (
     member((V,_J,A),Profiles)
    ),
   Collection),
   sort(Collection,Acts).

collect_actions_for_vertices([],_,[]).
collect_actions_for_vertices([V|G],Profiles,[A|W]):-
   collect_actions_for_a_vertex(V,Profiles,Collected,A),
   subtract(Profiles,Collected,NewPro),
   collect_actions_for_vertices(G,NewPro,W).


/*************************************************

?- event_description(A,B,C).

A = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
B = 32
C = [[down, right], [down, right], [down, right], [down, right], [down, right]] ;

A = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
B = 31
C = [[down, right], [down, right], [down, right], [down, right], [down, right]] ;

A = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
B = 31
C = [[down, right], [down, right], [down, right], [down, right], [down, right]] 

Yes
?- event_description(A,2,C).

A = [1, 2]
C = [[down, right], [down], [down], [down], [down]] ;

A = [1, 3]
C = [[down], [down, right], [down], [down], [down]] ;

A = [1, 4]
C = [[down, right], [down, right], [down], [down], [down]] 

Yes
?- event_description(A,1,C).

A = [1]
C = [[down], [down], [down], [down], [down]] ;

A = [2]
C = [[right], [down], [down], [down], [down]] 

Yes
?- 

*************************************************/

% Hexa reprsentation for events
%---------------------------------------------------%
% added: 5-6 Feb 2005

hexa_event(E,X,Hx):-
   event(E,X,_NE),  % NE: length of E \= NX 
   hexa_list(X,_NX,GangOfFour),
   concat_list(Hx,GangOfFour).

% hexa_list/3  ---> common programs


% complementation
%---------------------------------------------------%
% added: 4 Feb 2005

complement(E,N,C):-
   all_states(O),
   event(E,X,N),
   c_list_projection(X,O,C).

% super/sub events
%---------------------------------------------------%
% added: 31 Jan 2005.
% modified: 1 Feb 2005.

super_event(E,F,N):-
   super_event_with_length((E,N),(F,_M)).

super_event_with_length((X,N),(Y,M)):-
   (var(X)->fail;true),
   event(Y,M),
   subset(Y,X),
   length(X,N).

super_event_with_length((E,N),(F,L)):-
   (var(E)->true;fail),
   integer(N),
   event(F,XF,L),
   %nl,write([N,L:F]),
   !,
   L =< N,
   super_projection_of_length((XE,N),(XF,L)),
  % sup_projection(XE,XF),
   event(E,XE,N),
   subset(F,E).

super_event_with_length((E,N),(P,L)):-
   (var(E)->true;fail),
   var(N),
   event(P,XP,L),
   reverse(XP,RXP),
   sup_projection(RXE,RXP),
   reverse(RXE,XE),
   event(E,XE,N).

super_projection_of_length((XE,N),(XF,L)):-
   integer(N),
   sum(XF,L),
   length(XF,U),
   length(XE,U),
   K is N - L,  % K: additional units required.
   M is U - L,  % M: the current number of zeros.
   choose_N_units_among(M,K,Xadd),
   findall(I,nth1(I,XF,0),Xzeros),
   make_pairs(Xsubst,Xzeros,Xadd),
   findall(Z,
    (
     nth1(I,XF,X),
     (member((I-Y),Xsubst)->
     Z is X + Y;Z = X)
    ),
   XE).


% Note:
% The following test patterns has run over 32 states.

/*************************************************

?- super_event_with_length((E,N),(P,2)).

E = [1, 2]
N = 2
P = [1, 2] ;

E = [1, 2, 3]
N = 3
P = [1, 2] ;

E = [1, 2, 4]
N = 3
P = [1, 2] 

Yes
?- super_event_with_length((E,5),(P,2)).

E = [1, 2, 3, 4, 5]
P = [1, 2] ;

E = [1, 2, 3, 4, 6]
P = [1, 2] ;

E = [1, 2, 3, 4, 7]
P = [1, 2] 

Yes
?- super_projection_of_length((XE,3),([0,1,1],2)).

XE = [1, 1, 1] ;

No
?- super_projection_of_length((XE,3),([0,1,1,0],2)).

XE = [1, 1, 1, 0] ;

XE = [0, 1, 1, 1] ;

No
?-
*************************************************/


% an earlier version (not used currently)

super_event_with_difference(E,D,P):-
   (var(E)->fail;true), % do this at first.
   event(P),
   subset(P,E),
   subtract(E,P,D).

super_event_with_difference(E,D,P):-
   (var(E)->true;fail),
   event(P),
   all_states(O),
   subtract(O,P,C),
   subset_of(CC,_,C),
   subtract(C,CC,D),
   union(P,D,F),
   sort(F,E).

sub_event(E,P):-
   (var(P)->event(P);true),
   subset_of(E,_,P).


% partitions
%---------------------------------------------------%
% revised: 3 Feb 2005.

:- dynamic partition_0/3.

% K: a (coloring) number of cells in the partition
% O: all states 
% A: the assignment (coloring)

partitioning(K,O,A):-
   (var(K)->K=2;true),
   inductive_numbers([K|M]),
   all_states(O),
   length(O,N),
   bag0(A,M,N).
   %variation_seek_sequence(A,M,N). % instead of bag0(A,M,N).

assert_players_partition(I,K,O,A):-
   player(I),
   partitioning(K,O,A),
   make_pairs(P,O,A),
   PI0=partition_0(player(I),_,_),
   forall(PI0,retract(PI0)),
   assert(partition_0(player(I),colors,K)),
   forall(member(X-Y,P),
     assert(partition_0(player(I),state(X),Y))
   ).


% P: a partiton which consists of strategy profiles.
% K: the identification number of partiton.

partition(player(I),P,K):-
   setof(S,
     partition_0(player(I),state(S),K),
   P).


/*
% cf., an avoidance (cited from kalp01)

partitioning_of_states([[S|E]|H],[S|O]):-
   (var(O)->all_states([S|O]);true),
   event(E),
   subset(E,O),
   subtract(O,E,R),
   partitioning_of_states(H,R).

*/


/*************************************************

?- partitioning(K,O,A).

complete
total:32, sorted:32 strategy profiles have asserted.

K = 2
O = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
A = [1, 0, 1, 0, 1, 0, 1, 0, 1|...] 

Yes
?- 
?- partitioning(K,O,A).

K = 2
O = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
A = [1, 0, 1, 0, 1, 0, 1, 0, 1|...] ;

K = 2
O = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
A = [1, 0, 1, 0, 1, 0, 1, 0, 1|...] ;

K = 2
O = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
A = [1, 0, 1, 0, 1, 0, 1, 0, 1|...] ;

K = 2
O = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
A = [1, 0, 1, 0, 1, 0, 1, 0, 1|...] 

Yes
?- assert_players_partition(I,K,O,A).

I = ann
K = 2
O = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
A = [1, 0, 1, 0, 1, 0, 1, 0, 1|...] ;

I = ann
K = 2
O = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
A = [1, 0, 1, 0, 1, 0, 1, 0, 1|...] ;

I = ann
K = 2
O = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
A = [1, 0, 1, 0, 1, 0, 1, 0, 1|...] ;

I = ann
K = 2
O = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
A = [1, 0, 1, 0, 1, 0, 1, 0, 1|...] 

Yes
?- assert_players_partition(bob,K,O,A).

K = 2
O = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
A = [1, 0, 1, 0, 1, 0, 1, 0, 1|...] 

Yes
?- partition(I,K,O).

I = player(ann)
K = [1, 3, 5, 7, 9, 11, 13, 15, 17|...]
O = 1 ;

I = player(ann)
K = [2, 4, 6, 8, 10, 12, 14, 16, 18|...]
O = 0 ;

I = player(bob)
K = [1, 3, 5, 7, 9, 11, 13, 15, 17|...]
O = 1 ;

I = player(bob)
K = [2, 4, 6, 8, 10, 12, 14, 16, 18|...]
O = 0 ;

No
?- 


*************************************************/



% strategies and their relation to events
%---------------------------------------------------%
% 29,31 Jan 2005

% I: a name of player
% SI: player I's strategy for each of his/her vertices.
% X: the profile identification number which subsumes the pattern SI.


strategy_of_player(I,X,SI):-
   player(I),
   strategy_profile(X,_,SP),
   findall((V,A),
     member((V,I,A),SP),
   SI).

strategies_in_event(E,player(J),SPI):-
   player(J),
   event(E),
   findall(SI,
    (
     member(X,E),
     strategy_of_player(J,X,SI)
    ),
   L),
   sort(L,SPI).


strategies_in_partition(of(K,I),on(J),SPI):-
   partition(player(I),P,K),
   strategies_in_event(P,player(J),SPI).

own_strategies_in_partition(K,player(I),SPI):-
   strategies_in_partition(of(K,I),on(I),SPI).



/*************************************************

?- strategy_of_player(ann,B,C),nl,write(B:C),fail.

1:[ (1, down), (3, down), (5, down)]
2:[ (1, right), (3, down), (5, down)]
3:[ (1, down), (3, down), (5, down)]
4:[ (1, right), (3, down), (5, down)]
5:[ (1, down), (3, right), (5, down)]
6:[ (1, right), (3, right), (5, down)]
7:[ (1, down), (3, right), (5, down)]
8:[ (1, right), (3, right), (5, down)]
9:[ (1, down), (3, down), (5, down)]
10:[ (1, right), (3, down), (5, down)]
11:[ (1, down), (3, down), (5, down)]
12:[ (1, right), (3, down), (5, down)]
13:[ (1, down), (3, right), (5, down)]
14:[ (1, right), (3, right), (5, down)]
15:[ (1, down), (3, right), (5, down)]
16:[ (1, right), (3, right), (5, down)]
17:[ (1, down), (3, down), (5, right)]
18:[ (1, right), (3, down), (5, right)]
19:[ (1, down), (3, down), (5, right)]
20:[ (1, right), (3, down), (5, right)]
21:[ (1, down), (3, right), (5, right)]
22:[ (1, right), (3, right), (5, right)]
23:[ (1, down), (3, right), (5, right)]
24:[ (1, right), (3, right), (5, right)]
25:[ (1, down), (3, down), (5, right)]
26:[ (1, right), (3, down), (5, right)]
27:[ (1, down), (3, down), (5, right)]
28:[ (1, right), (3, down), (5, right)]
29:[ (1, down), (3, right), (5, right)]
30:[ (1, right), (3, right), (5, right)]
31:[ (1, down), (3, right), (5, right)]
32:[ (1, right), (3, right), (5, right)]

No
?- strategy_of_player(bob,B,C),nl,write(B:C),fail.

1:[ (2, down), (4, down)]
2:[ (2, down), (4, down)]
3:[ (2, right), (4, down)]
4:[ (2, right), (4, down)]
5:[ (2, down), (4, down)]
6:[ (2, down), (4, down)]
7:[ (2, right), (4, down)]
8:[ (2, right), (4, down)]
9:[ (2, down), (4, right)]
10:[ (2, down), (4, right)]
11:[ (2, right), (4, right)]
12:[ (2, right), (4, right)]
13:[ (2, down), (4, right)]
14:[ (2, down), (4, right)]
15:[ (2, right), (4, right)]
16:[ (2, right), (4, right)]
17:[ (2, down), (4, down)]
18:[ (2, down), (4, down)]
19:[ (2, right), (4, down)]
20:[ (2, right), (4, down)]
21:[ (2, down), (4, down)]
22:[ (2, down), (4, down)]
23:[ (2, right), (4, down)]
24:[ (2, right), (4, down)]
25:[ (2, down), (4, right)]
26:[ (2, down), (4, right)]
27:[ (2, right), (4, right)]
28:[ (2, right), (4, right)]
29:[ (2, down), (4, right)]
30:[ (2, down), (4, right)]
31:[ (2, right), (4, right)]
32:[ (2, right), (4, right)]

No
?- strategies_in_partition(K,on(bob),SPI).

K = of(1, ann)
SPI = [[ (2, down), (4, down)], [ (2, down), (4, right)], [ (2, right), (4, down)], [ (2, right), (4, right)]] ;

K = of(0, ann)
SPI = [[ (2, down), (4, down)], [ (2, down), (4, right)], [ (2, right), (4, down)], [ (2, right), (4, right)]] ;

K = of(1, bob)
SPI = [[ (2, down), (4, down)], [ (2, down), (4, right)], [ (2, right), (4, down)], [ (2, right), (4, right)]] ;

K = of(0, bob)
SPI = [[ (2, down), (4, down)], [ (2, down), (4, right)], [ (2, right), (4, down)], [ (2, right), (4, right)]] ;

No
?- own_strategies_in_partition(K,player(I),S).

K = 1
I = ann
S = [[ (1, down), (3, down), (5, down)], [ (1, down), (3, down), (5, right)], [ (1, down), (3, right), (5, down)], [ (1, down), (3, right), (5, right)]] ;

K = 0
I = ann
S = [[ (1, down), (3, right), (5, right)], [ (1, right), (3, down), (5, down)], [ (1, right), (3, down), (5, right)], [ (1, right), (3, right), (5, down)], [ (1, right), (3, right), (5, right)]] ;

K = 1
I = bob
S = [[ (2, down), (4, down)], [ (2, down), (4, right)], [ (2, right), (4, down)], [ (2, right), (4, right)]] ;

K = 0
I = bob
S = [[ (2, down), (4, down)], [ (2, down), (4, right)], [ (2, right), (4, down)], [ (2, right), (4, right)]] ;

No
?- 

*************************************************/



%---------------------------------------------------%
% 3. Knowledge system of game players
%---------------------------------------------------%
% 31 Jan -- 4 Feb 2005.

% `A knowledge system (for the given game) consists of 
%    a set Omega (the states of the world, or simply states),
%    a function [s] from Omega to x_i S_i,
% and for each player i,
%    a partition >K<_i of Omega (i's information partition). 
% (Aumann, 1995 pp.8)


% measurability of strategies with respect to partition
%---------------------------------------------------%

% `We asssume that 
%     s_i is measurable with respect to >K<_i,
% which means that [s]_i(w)=[s]_i(v) whnever w and v are
% in the same element of >K<_i.'
% (Aumann, 1995 pp.8--9)


% the coarsest partition w.r.t. 
% which own strategy function is measurable

maximal_partition_for_measurability(I,P,S):-
   event_of_a_strategy_of_player(I,P,S).

% Instead of bracket notation in the literature,
% for example, [starategy_of_player(i)=s],
% We give a predicate model as follows.

event_of_a_strategy_of_player(I,Event,Strategy):-
   player(I),
   setof(W,
    (
     state(W),
     strategy_of_player(I,W,Strategy)
    ),
   Event).


/*************************************************
     
?- maximal_partition_for_measurability(ann,P,S).

P = [1, 3, 9, 11]
S = [ (1, down), (3, down), (5, down)] ;

P = [2, 4, 10, 12]
S = [ (1, right), (3, down), (5, down)] ;

P = [5, 7, 13, 15]
S = [ (1, down), (3, right), (5, down)] ;

P = [6, 8, 14, 16]
S = [ (1, right), (3, right), (5, down)] ;

P = [17, 19, 25, 27]
S = [ (1, down), (3, down), (5, right)] ;

P = [18, 20, 26, 28]
S = [ (1, right), (3, down), (5, right)] ;

P = [21, 23, 29, 31]
S = [ (1, down), (3, right), (5, right)] ;

P = [22, 24, 30, 32]
S = [ (1, right), (3, right), (5, right)] ;

No
?- maximal_partition_for_measurability(bob,P,S).

P = [1, 2, 5, 6, 17, 18, 21, 22]
S = [ (2, down), (4, down)] ;

P = [3, 4, 7, 8, 19, 20, 23, 24]
S = [ (2, right), (4, down)] ;

P = [9, 10, 13, 14, 25, 26, 29, 30]
S = [ (2, down), (4, right)] ;

P = [11, 12, 15, 16, 27, 28, 31, 32]
S = [ (2, right), (4, right)] ;

No
?- 

*************************************************/


% measurability w.r.t. partition, and 
% a script for generate partition by means of which 
% players' strategies are measurable.
%---------------------------------------------------%

is_measurable_wrt_partition(K,P,SPI,player(I),Y):-
   is_a_cell_of_partiton(player(I),K),
   partition(player(I),P,K),
   own_strategies_in_partition(K,player(I),SPI),
   (length(SPI,1)->Y=true;Y=false).

is_a_cell_of_partiton(player(I),K):-
   partition_0(player(I),colors,C),
   (inductive_numbers([C|M])->true),
   member(K,M).

verify_measurability(I,L,X):-
   player(I),
   findall((I,S,Y),
    (
     is_a_cell_of_partiton(player(I),K),
     is_measurable_wrt_partition(K,_,S,player(I),Y)
    ),
   L),
   ( member((I,S,false),L)->X=false;X=true).


make_strategies_measurable(I):-
   player(I),
   findall((P,S),
     maximal_partition_for_measurability(I,P,S),
   L),
   length(L,K),
   PI0=partition_0(player(I),_,_),
   forall(PI0,retract(PI0)),
   assert(partition_0(player(I),colors,K)),
   forall(
    (
     nth0(Y,L,(P,S)),
     member(X,P)
    ),
     assert(partition_0(player(I),state(X),Y))
   ).


/*************************************************

?- is_measurable_wrt_partition(K,P,S,player(I),Y).


K = 1
P = [1, 3, 5, 7, 9, 11, 13, 15, 17|...]
S = [[ (1, right), (3, down), (5, down)], [ (1, right), (3, down), (5, right)], [ (1, right), (3, right), (5, down)], [ (1, right), (3, right), (5, right)]]
I = ann
Y = false ;

K = 0
P = [2, 4, 6, 8, 10, 12, 14, 16, 18|...]
S = [[ (1, down), (3, down), (5, down)], [ (1, down), (3, down), (5, right)], [ (1, down), (3, right), (5, down)], [ (1, down), (3, right), (5, right)], [ (1, right), (3, down), (5, down)], [ (1, right), (3, down), (..., ...)], [ (1, right), (..., ...)|...], [ (..., ...)|...]]
I = ann
Y = false ;

K = 1
P = [1, 3, 5, 7, 9, 11, 13, 15, 17|...]
S = [[ (2, down), (4, down)], [ (2, down), (4, right)], [ (2, right), (4, down)], [ (2, right), (4, right)]]
I = bob
Y = false ;

K = 0
P = [2, 4, 6, 8, 10, 12, 14, 16, 18|...]
S = [[ (2, down), (4, down)], [ (2, down), (4, right)], [ (2, right), (4, down)], [ (2, right), (4, right)]]
I = bob
Y = false ;

No
?- make_strategies_measurable(I).

I = ann ;

I = bob ;

No
?- partition(A,B,C),hexa_event(B,_,H),event_description(B,_,D),
 nl,write(A:partition(C):H:B:D),fail.

player(ann):partition(0):a0a00000:[1, 3, 9, 11]:[[down], [down, right], [down], [down, right], [down]]
player(ann):partition(1):50500000:[2, 4, 10, 12]:[[right], [down, right], [down], [down, right], [down]]
player(ann):partition(2):0a0a0000:[5, 7, 13, 15]:[[down], [down, right], [right], [down, right], [down]]
player(ann):partition(3):05050000:[6, 8, 14, 16]:[[right], [down, right], [right], [down, right], [down]]
player(ann):partition(4):0000a0a0:[17, 19, 25, 27]:[[down], [down, right], [down], [down, right], [right]]
player(ann):partition(5):00005050:[18, 20, 26, 28]:[[right], [down, right], [down], [down, right], [right]]
player(ann):partition(6):00000a0a:[21, 23, 29, 31]:[[down], [down, right], [right], [down, right], [right]]
player(ann):partition(7):00000505:[22, 24, 30, 32]:[[right], [down, right], [right], [down, right], [right]]
player(bob):partition(0):cc00cc00:[1, 2, 5, 6, 17, 18, 21, 22]:[[down, right], [down], [down, right], [down], [down, right]]
player(bob):partition(1):33003300:[3, 4, 7, 8, 19, 20, 23, 24]:[[down, right], [right], [down, right], [down], [down, right]]
player(bob):partition(2):00cc00cc:[9, 10, 13, 14, 25, 26, 29, 30]:[[down, right], [down], [down, right], [right], [down, right]]
player(bob):partition(3):00330033:[11, 12, 15, 16, 27, 28, 31, 32]:[[down, right], [right], [down, right], [right], [down, right]]

No
?- is_measurable_wrt_partition(K,P,S,player(I),Y).

K = 7
P = [22, 24, 30, 32]
S = [[ (1, right), (3, right), (5, right)]]
I = ann
Y = true ;

K = 6
P = [21, 23, 29, 31]
S = [[ (1, down), (3, right), (5, right)]]
I = ann
Y = true ;

K = 5
P = [18, 20, 26, 28]
S = [[ (1, right), (3, down), (5, right)]]
I = ann
Y = true 

Yes
?- verify_measurability(I,L,X).

I = ann
L = [ (ann, [[ (1, down), (3, down), (5, right)]], true), (ann, [[ (1, right), (3, down), (5, right)]], true), (ann, [[ (1, down), (3, right), (..., ...)]], true), (ann, [[ (1, right), (..., ...)|...]], true), (ann, [[ (..., ...)|...]], true), (ann, [[...|...]], true), (ann, [...], true), (ann, ..., ...)]
X = true ;

I = bob
L = [ (bob, [[ (2, down), (4, down)]], true), (bob, [[ (2, right), (4, down)]], true), (bob, [[ (2, down), (4, right)]], true), (bob, [[ (2, right), (..., ...)]], true)]
X = true ;

No
?- 


*************************************************/



% Scipts for knowledge systems and their epistemic properties
%---------------------------------------------------%
% 31 Jan -- 4 Feb 2005.

preliminary_for_epistemic_analysis:-
   clause(partition_0(_,_,_),_),
   !.

preliminary_for_epistemic_analysis:-
   \+ clause(partition_0(_,_,_),_),
   forall(
     player(I),
     make_strategies_measurable(I)
   ).

:- preliminary_for_epistemic_analysis.


% individual knowledge 
%---------------------------------------------------%

event_known_by(E,player(J),par(K,P),len(N)):-
   preliminary_for_epistemic_analysis,
   partition(player(J),P,K),
   super_event(E,P,N).

knowledge_operator(KE,E,len(N),player(J),Partitions):-
   player(J),
   event(E,_,N),
   findall((K,P),
    (
     partition(player(J),P,K),
     subset(P,E)
    ),
   FocalSets),
   findall(K,member((K,P),FocalSets),Partitions),
   findall(P,member((K,P),FocalSets),Disjunction),
   flatten(Disjunction,D1),
   sort(D1,KE).

% projection to the strategy space of a player.

know_that(player(J),par(K,P),That):-
   preliminary_for_epistemic_analysis,
   partition(player(J),P,K),
   strategies_in_partition(of(K,J),on(He),B),
   That=plays(He,B).


% an ignorance operator (added: 5-6 Feb 2005.) 

does_not_know(DKE,E,Len,PL,Partitions):-
   knowledge_operator(KE,E,Len,PL,Partitions),
   complement(KE,_,DKE),
   !.
  %<-- notice: it causes unintended backtrack if 
  %    complement(DKE,_,DKE).


/*************************************************


?- event_known_by(E,player(J),par(K,P),len(N)).

E = [1, 3, 9, 11]
J = ann
K = 0
P = [1, 3, 9, 11]
N = 4 ;

E = [1, 2, 3, 9, 11]
J = ann
K = 0
P = [1, 3, 9, 11]
N = 5 

Yes
?- knowledge_operator(KE,E,len(N),player(ann),Partitions).

KE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
E = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
N = 32
Partitions = [0, 1, 2, 3, 4, 5, 6, 7] ;

KE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
E = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
N = 31
Partitions = [0, 1, 2, 3, 4, 5, 6] 

Yes
?- knowledge_operator(KE,E,len(N),player(bob),Partitions).

KE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
E = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
N = 32
Partitions = [0, 1, 2, 3] ;

KE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
E = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
N = 31
Partitions = [0, 1, 2] 

Yes
?- inductive_numbers([32|M]),member(N,M),
    knowledge_operator(KE,E,len(N),player(bob),[]),
    event_description(E,_,D).

M = [31, 30, 29, 28, 27, 26, 25, 24, 23|...]
N = 28
KE = []
E = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
D = [[down, right], [down, right], [down, right], [down, right], [down, right]] 

Yes
?- know_that(player(ann),par(2,P),That).

P = [5, 7, 13, 15]
That = plays(ann, [[ (1, down), (3, right), (5, down)]]) ;

P = [5, 7, 13, 15]
That = plays(bob, [[ (2, down), (4, down)], [ (2, down), (4, right)], [ (2, right), (4, down)], [ (2, right), (4, right)]]) ;

No
?- know_that(player(bob),par(3,P),That).

P = [11, 12, 15, 16, 27, 28, 31, 32]
That = plays(ann, [[ (1, down), (3, down), (5, down)], [ (1, down), (3, down), (5, right)], [ (1, down), (3, right), (5, down)], [ (1, down), (3, right), (5, right)], [ (1, right), (3, down), (..., ...)], [ (1, right), (..., ...)|...], [ (..., ...)|...], [...|...]]) ;

P = [11, 12, 15, 16, 27, 28, 31, 32]
That = plays(bob, [[ (2, right), (4, right)]]) ;

No
?- knowledge_operator(KE,E,len(N),player(bob),[3]),
event_description(KE,_,D).

KE = [11, 12, 15, 16, 27, 28, 31, 32]
E = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
N = 29
D = [[down, right], [right], [down, right], [right], [down, right]] 

Yes
?- 

*************************************************/




% mutual knowledge of first order
%---------------------------------------------------%

meet_of_partition(Meet,[(ann,Ha,Pa),(bob,Hb,Pb)]):-
   partition(player(ann),Pa,Ha),
   partition(player(bob),Pb,Hb),
   union(Pa,Pb,UP),
   sort(UP,Meet).

knowledge_profile(E,[(ann,SPa,KaE),(bob,SPb,KbE)]):-
   (A,B)=(player(ann),player(bob)),
   knowledge_operator(KaE,E,len(N),A,SPa),
   knowledge_operator(KbE,E,len(N),B,SPb).

mutual_knowledge(KE,on(E),[(ann,SPa,KaE),(bob,SPb,KbE)]):-
   knowledge_profile(E,[(ann,SPa,KaE),(bob,SPb,KbE)]),
   intersection(KaE,KbE,KE).

mutual_conjectures_about(player(J),[(ann,Ca,Ia,Pa),(bob,Cb,Ib,Pb)]):-
   Wa=plays(J,Ca),
   Wb=plays(J,Cb),
   know_that(player(ann),par(Ia,Pa),Wa),
   know_that(player(bob),par(Ib,Pb),Wb).


mutually_know_about(player(J),D,[uni(M),int(H),(ann,Ca),(bob,Cb)]):-
   mutual_conjectures_about(player(J),[(ann,Ca,_,Pa),(bob,Cb,_,Pb)]),
   intersection(Pa,Pb,H),
   union(Pa,Pb,M),
   event_description(M,_,D).
   

/*************************************************

?- meet_of_partition(Meet,[(ann,Ha,Pa),(bob,Hb,Pb)]).

Meet = [1, 2, 3, 5, 6, 9, 11, 17, 18|...]
Ha = 0
Pa = [1, 3, 9, 11]
Hb = 0
Pb = [1, 2, 5, 6, 17, 18, 21, 22] ;

Meet = [1, 3, 4, 7, 8, 9, 11, 19, 20|...]
Ha = 0
Pa = [1, 3, 9, 11]
Hb = 1
Pb = [3, 4, 7, 8, 19, 20, 23, 24] 

Yes
?- knowledge_profile(E,[(ann,Pa,KaE),(bob,Pb,KbE)]).

E = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
Pa = [0, 1, 2, 3, 4, 5, 6, 7]
KaE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
Pb = [0, 1, 2, 3]
KbE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...] ;

E = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
Pa = [0, 1, 2, 3, 4, 5, 6]
KaE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
Pb = [0, 1, 2]
KbE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...] 

Yes
?- mutual_knowledge(KE,on(E),[(ann,A,KaE),(bob,B,KbE)]),
length(E,LE),length(KE,LKE).

KE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
E = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
A = [0, 1, 2, 3, 4, 5, 6, 7]
KaE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
B = [0, 1, 2, 3]
KbE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
LE = 32
LKE = 32 ;

KE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
E = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
A = [0, 1, 2, 3, 4, 5, 6]
KaE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
B = [0, 1, 2]
KbE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
LE = 31
LKE = 21 

Yes
?- mutual_conjectures_about(player(J),[(ann,Ca,_),(bob,Cb,_)]).

J = ann
Ca = [[ (1, down), (3, down), (5, down)]]
Cb = [[ (1, down), (3, down), (5, down)], [ (1, down), (3, down), (5, right)], [ (1, down), (3, right), (5, down)], [ (1, down), (3, right), (5, right)], [ (1, right), (3, down), (5, down)], [ (1, right), (3, down), (..., ...)], [ (1, right), (..., ...)|...], [ (..., ...)|...]] ;

J = ann
Ca = [[ (1, down), (3, down), (5, down)]]
Cb = [[ (1, down), (3, down), (5, down)], [ (1, down), (3, down), (5, right)], [ (1, down), (3, right), (5, down)], [ (1, down), (3, right), (5, right)], [ (1, right), (3, down), (5, down)], [ (1, right), (3, down), (..., ...)], [ (1, right), (..., ...)|...], [ (..., ...)|...]] ;

J = ann
Ca = [[ (1, down), (3, down), (5, down)]]
Cb = [[ (1, down), (3, down), (5, down)], [ (1, down), (3, down), (5, right)], [ (1, down), (3, right), (5, down)], [ (1, down), (3, right), (5, right)], [ (1, right), (3, down), (5, down)], [ (1, right), (3, down), (..., ...)], [ (1, right), (..., ...)|...], [ (..., ...)|...]] 

Yes
?- mutual_conjectures_about(player(J),[(ann,Ca,_),(bob,Ca,_)]).

No
?- mutually_know_about(player(J),D,[M,H,A,B]).

J = ann
D = [[down, right], [down, right], [down, right], [down, right], [down, right]]
M = uni([1, 3, 9, 11, 12, 15, 16, 27|...])
H = int([11])
A = ann, [[ (1, down), (3, down), (5, down)]]
B = bob, [[ (1, down), (3, down), (5, down)], [ (1, down), (3, down), (5, right)], [ (1, down), (3, right), (5, down)], [ (1, down), (3, right), (5, right)], [ (1, right), (3, down), (..., ...)], [ (1, right), (..., ...)|...], [ (..., ...)|...], [...|...]] 

Yes
?- mutually_know_about(player(J),D,_).

J = ann
D = [[down, right], [down, right], [down, right], [down, right], [down, right]] ;

J = bob
D = [[down, right], [down, right], [down, right], [down, right], [down, right]] ;

J = ann
D = [[down, right], [down, right], [down, right], [down, right], [down, right]] ;

J = bob
D = [[down, right], [down, right], [down, right], [down, right], [down, right]] ;

No
?-

*************************************************/



% higher order mutual knowledges and 
% (approximated) common knowledge
%---------------------------------------------------%

mutual_knowledge_of_order(0,E,on(E),[]).

mutual_knowledge_of_order(N,KKnE,on(E),[A|B]):-
   length([_|B],N),
   mutual_knowledge_of_order(_,KnE,on(E),B),
   ((KnE==[];N>=10)->!;true),
   mutual_knowledge(KKnE,on(KnE),A).

% approximate common knowledge
% in truncated hierarchies of mutual knowledge.

common_knowledge(CKE,on(E),(N,C)):-
   event_description(E,N,C),
   max(D,mutual_knowledge_of_order(D,CKE,on(E),_)).



/*************************************************
% test case (1) :
% iterative use of the first order mutual knowledges.

?- mutual_knowledge(KE,on(E),_).

KE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
E = [1, 2, 3, 4, 5, 6, 7, 8, 9|...] 

Yes
?- mutual_knowledge(KE,on(E),_),
   mutual_knowledge(KKE,on(KE),_).

KE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
E = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
KKE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...] ;

KE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
E = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
KKE = [] ;

KE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
E = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
KKE = [] 

Yes
?- event(E,31),mutual_knowledge(KE,on(E),_),
   mutual_knowledge(KKE,on(KE),_),KKE\=[].

No
?- mutual_knowledge(KE,on(E),_),KE,on(E),_),
   mutual_knowledge(KKE,on(KE),_),
   mutual_knowledge(KKKE,on(KKE),_).

KE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
E = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
KKE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
KKKE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...] ;

KE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
E = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
KKE = []
KKKE = [] ;

KE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
E = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
KKE = []
KKKE = [] 

Yes

*************************************************/



/*************************************************
% test case (2) :
% higher order mutual knowledges.

?- event(E,N,C),mutual_knowledge_of_order(2,MKE,on(E),A),MKE\=[].

E = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
N = [1, 1, 1, 1, 1, 1, 1, 1, 1|...]
C = 32
MKE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
A = [[ (ann, [0, 1, 2, 3, 4|...], [1, 2, 3, 4, 5|...]), (bob, [0, 1, 2, 3], [1, 2, 3, 4|...])], [ (ann, [0, 1, 2, 3|...], [1, 2, 3, 4|...]), (bob, [0, 1, 2|...], [1, 2, 3|...])]] ;

No
?- mutual_knowledge_of_order(3,MKE,on(E),A).

MKE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
E = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
A = [[ (ann, [0, 1, 2, 3, 4|...], [1, 2, 3, 4, 5|...]), (bob, [0, 1, 2, 3], [1, 2, 3, 4|...])], [ (ann, [0, 1, 2, 3|...], [1, 2, 3, 4|...]), (bob, [0, 1, 2|...], [1, 2, 3|...])], [ (ann, [0, 1, 2|...], [1, 2, 3|...]), (bob, [0, 1|...], [1, 2|...])]] ;

No
?- event_description(E,32,C),
mutual_knowledge_of_order(2,MKE,on(E),A),MKE\=[].

E = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
C = [[down, right], [down, right], [down, right], [down, right], [down, right]]
MKE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
A = [[ (ann, [0, 1, 2, 3, 4|...], [1, 2, 3, 4, 5|...]), (bob, [0, 1, 2, 3], [1, 2, 3, 4|...])], [ (ann, [0, 1, 2, 3|...], [1, 2, 3, 4|...]), (bob, [0, 1, 2|...], [1, 2, 3|...])]] ;

No
?- event_description(E,31,C),
mutual_knowledge_of_order(2,MKE,on(E),A),MKE\=[].

No
?- event_description(E,32,C),
mutual_knowledge_of_order(20,MKE,on(E),_),MKE\=[].

E = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
C = [[down, right], [down, right], [down, right], [down, right], [down, right]]
MKE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]

Yes

/*************************************************




*************************************************/
% test case (3) :
% common knowledges.

?- common_knowledge(CKE,on(E),A).

CKE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
E = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
A = 32, [[down, right], [down, right], [down, right], [down, right], [down, right]] ;

CKE = []
E = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
A = 31, [[down, right], [down, right], [down, right], [down, right], [down, right]] ;

CKE = []
E = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
A = 31, [[down, right], [down, right], [down, right], [down, right], [down, right]] 

Yes
?- common_knowledge(CKE,on(E),(1,A)).

CKE = []
E = [1]
A = [[down], [down], [down], [down], [down]] ;

CKE = []
E = [2]
A = [[right], [down], [down], [down], [down]] 

Yes
?- 

*************************************************/



%---------------------------------------------------%
% 4. Rationality and substantive conditionals
%---------------------------------------------------%
% 4-16 Feb 2005.


% knowledge of inductive choice at vertices
%---------------------------------------------------%
% revised version added: 13 Feb 2005

% The following corresponds to B_i^v  in the proof of 
% Lemma 10 (Auman,1995 p.11), which is the set of 
% strategies s_i of i for which s_i^v=b^v (i.e., a choice 
% which is in accordance with backward induction play 
% at the vertex) and the player's knowledge.


inductive_choice_compatibles((V,J,A),BI_choices,E,DE):-
   inductive_choice_in_profile(_BI_id,_,BI_choices),
   vertex(V),
   member((V,J,A),BI_choices),
   findall(W,
    (
     strategy_profile(W,_,Choices),
     member((V,J,A),Choices)
    ),
   E),
   event_description(E,_,DE).

% knowledge of inductive play at the last vertex.

knowledge_of_inductive_choice((V,J,A),BIC,(E,D),(KE,DK)):-
   inductive_choice_compatibles((V,J,A),BIC,E,D),
   knowledge_operator(KE,E,_,player(J),_),
   event_description(KE,_,DK).


/*************************************************

% Although it may be of somewhat trivial under the measurability
% assumption, i.e., self-reflective knowledge of choice,
% the followings are intended to verify a case of Lemma 10.


?- knowledge_of_inductive_choice(KJA,BI_choices,(_,E),(_,KE)),
nl,write(KJA),nl,write(E),nl,write(KE),fail.

1, ann, down
[[down], [down, right], [down, right], [down, right], [down, right]]
[[down], [down, right], [down, right], [down, right], [down, right]]
2, bob, down
[[down, right], [down], [down, right], [down, right], [down, right]]
[[down, right], [down], [down, right], [down, right], [down, right]]
3, ann, down
[[down, right], [down, right], [down], [down, right], [down, right]]
[[down, right], [down, right], [down], [down, right], [down, right]]
4, bob, down
[[down, right], [down, right], [down, right], [down], [down, right]]
[[down, right], [down, right], [down, right], [down], [down, right]]
5, ann, down
[[down, right], [down, right], [down, right], [down, right], [down]]
[[down, right], [down, right], [down, right], [down, right], [down]]

No
?- 

% comparison with a yet another alternative 

?- event_description_1(E,D,Hx,[d|_]),
knowledge_operator(KE,E,_,player(ann),_),
hexa_event(KE,_,H).

E = [1, 3, 5, 7, 9, 11, 13, 15, 17|...]
D = [[down], [down, right], [down, right], [down, right], [down, right]]
Hx = aaaaaaaa
KE = [1, 3, 5, 7, 9, 11, 13, 15, 17|...]
H = aaaaaaaa ;

No
?-

*************************************************/


% added: 15 Feb 2005.

non_inductive_strategies_at(V,E,DE):-
   inductive_choice_in_profile(_BI_id,_,BI_choices),
   V=vertex(K),
   member((K,J,Bv),BI_choices),
   findall(W,
    (
     strategy_profile(W,_,Choices),
     member((K,J,Av),Choices),
     Av \= Bv
    ),
   E),
   event_description(E,_,DE).


/*************************************************

?- non_inductive_strategies_at(V,E,DE).

V = 1
E = [2, 4, 6, 8, 10, 12, 14, 16, 18|...]
DE = [[right], [down, right], [down, right], [down, right], [down, right]] ;

V = 2
E = [3, 4, 7, 8, 11, 12, 15, 16, 19|...]
DE = [[down, right], [right], [down, right], [down, right], [down, right]] ;

V = 3
E = [5, 6, 7, 8, 13, 14, 15, 16, 21|...]
DE = [[down, right], [down, right], [right], [down, right], [down, right]] ;

V = 4
E = [9, 10, 11, 12, 13, 14, 15, 16, 25|...]
DE = [[down, right], [down, right], [down, right], [right], [down, right]] ;

V = 5
E = [17, 18, 19, 20, 21, 22, 23, 24, 25|...]
DE = [[down, right], [down, right], [down, right], [down, right], [right]] ;

No
?- 

*************************************************/



% knowledge of inductive choice only at the vertex
%---------------------------------------------------%
% old version added: 11 Feb 2005

knowledge_of_inductive_choice_at_vertex(K,J,S,E,KE):-
   length(S,5),
   member((K,J),[(5,ann),(4,bob),(3,ann),(2,bob),(1,ann)]),
   nth1(K,S,d),
   findall(W,state_description(W,_,S),E),
   knowledge_operator(KE,E,_,player(J),_).


intersection_of_knowledges_of_inductive_choice(P,Q,R):-
   findall(KE,
     knowledge_of_inductive_choice_at_vertex(_,_,_,_,KE)
   ,P),
   intersection_of_lists(P,Q),
   event_description(Q,_,R).


/*************************************************

?- knowledge_of_inductive_choice_at_vertex(K,J,S,E,KE),
event_description(KE,_,DK),
nl,write(K;J;S),nl,write('E'=E),nl,write('KE'=KE),
fail.

5;ann;[_G582, _G585, _G588, _G591, d]
E=[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16]
KE=[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16]
4;bob;[_G582, _G585, _G588, d, _G594]
E=[1, 2, 3, 4, 5, 6, 7, 8, 17, 18, 19, 20, 21, 22, 23, 24]
KE=[1, 2, 3, 4, 5, 6, 7, 8, 17, 18, 19, 20, 21, 22, 23, 24]
3;ann;[_G582, _G585, d, _G591, _G594]
E=[1, 2, 3, 4, 9, 10, 11, 12, 17, 18, 19, 20, 25, 26, 27, 28]
KE=[1, 2, 3, 4, 9, 10, 11, 12, 17, 18, 19, 20, 25, 26, 27, 28]
2;bob;[_G582, d, _G588, _G591, _G594]
E=[1, 2, 5, 6, 9, 10, 13, 14, 17, 18, 21, 22, 25, 26, 29, 30]
KE=[1, 2, 5, 6, 9, 10, 13, 14, 17, 18, 21, 22, 25, 26, 29, 30]
1;ann;[d, _G585, _G588, _G591, _G594]
E=[1, 3, 5, 7, 9, 11, 13, 15, 17, 19, 21, 23, 25, 27, 29, 31]
KE=[1, 3, 5, 7, 9, 11, 13, 15, 17, 19, 21, 23, 25, 27, 29, 31]

No
?- intersection_of_knowledges_of_inductive_choice(P,Q,R).

P = [[1, 2, 3, 4, 5, 6, 7, 8|...], [1, 2, 3, 4, 5, 6, 7|...], [1, 2, 3, 4, 9, 10|...], [1, 2, 5, 6, 9|...], [1, 3, 5, 7|...]]
Q = [1]
R = [[down], [down], [down], [down], [down]] 

Yes
?


*************************************************/



%---------------------------------------------------%
% conditional payoffs and substantive rationality
%---------------------------------------------------%
% the event conditional payoff would have been higher
% if he had chosen the strategy t[i] rather than 
% what he did choose. 
% (The correspondent to h^v_i([s]) in the literature.)


:- dynamic would_have_yielded_higher_payoff_0/5.

% prepare_whyhp/0 
% added: 15 Feb 2005 

prepare_whyhp:-
   abolish(would_have_yielded_higher_payoff_0/5),
   tell_goal('would1.txt',forall,
     would_have_yielded_higher_payoff(_,_,_,_,_)
   ),
   nl,
   write('complete.'),
   nl,
   write(' please edit would.txt in the working directory,'), 
   nl,
   write(' replace each'), 
   nl,
   write('    would_have_yielded_higher_payoff('),
   nl,
   write(' with'),
   nl,
   write('    would_have_yielded_higher_payoff_0('),
   nl,
   write(' then do [kglp01]. '),
   nl,
   write(' Thanks.').


would_have_yielded_higher_payoff(SW,PL,at(V,PH),D1,D,Tj,Sj):-
   would_have_yielded_higher_payoff(SW,PL,at(V,PH),D1,D),
   PL =player(J),
   D=[_,(strategy(_Id),S)],
   D1=[_,(strategy(_Id1),T)],
   findall((N,A),member((N,J,A),S),Sj),
   findall((N,A),member((N,J,A),T),Tj).
  %strategy_of_player(J,Id,Sj),
  %strategy_of_player(J,Id1,Tj).


% would_have_yielded_higher_payoff/5
% revied: 14 Feb 2005  (move/2 had missed his cue.)
% revied: 15 Feb 2005  (aftereffects of the revision of conditional_payoff/3.)
% revied: 17 Feb 2005  (aftereffects of the revision of state/1.)

would_have_yielded_higher_payoff(SW,PL,at(V,PH),D1,D):-
   clause(
     would_have_yielded_higher_payoff_0(SW,PL,at(V,PH),D1,D),
   true),
   move(V,PL),
   SW=given_state(W),
   state(W).

would_have_yielded_higher_payoff(SW,PL,at(V,PH),Dt,D):-
   \+ clause(would_have_yielded_higher_payoff_0(_,_,_,_,_),true),
   SW=given_state(W),
   state_description(W,S),
   PL =player(_J),
   V =vertex(_),
   move(V,PL),
   D=[(payoff(U),Z),(strategy(I),S)],
   Dt=[(payoff(Ut),Zt),(strategy(It),T)],
   X =[V,PH,(I,S),Z],
   Xt =[V,PH,(It,T),Zt],
   conditional_payoff(X,PL,payoff(U)),
   conditional_payoff(Xt,PL,payoff(Ut)),
   Ut > U,
   verify_unilateral_deviance_by(PL,S,T).

verify_unilateral_deviance_by(player(J),S,T):-
   subtract(T,S,Difference),
   \+ (
     member((_,OP,_),Difference),
     OP\=J
   ).



/*************************************************

?- would_have_yielded_higher_payoff(SW,PL,at(V,PH),[Z1,T],[Z,S]).

SW = given_state(2)
PL = player(ann)
V = vertex(1)
PH = []
Z1 = payoff(2), terminal(1)
T = strategy(1), [ (1, ann, down), (2, bob, down), (3, ann, down), (4, bob, down), (5, ann, down)]
Z = payoff(1), terminal(2)
S = strategy(2), [ (1, ann, right), (2, bob, down), (3, ann, down), (4, bob, down), (5, ann, down)] ;

SW = given_state(2)
PL = player(ann)
V = vertex(1)
PH = []
Z1 = payoff(2), terminal(1)
T = strategy(5), [ (1, ann, down), (2, bob, down), (3, ann, right), (4, bob, down), (5, ann, down)]
Z = payoff(1), terminal(2)
S = strategy(2), [ (1, ann, right), (2, bob, down), (3, ann, down), (4, bob, down), (5, ann, down)] 

Yes
?- V=vertex(5),
   would_have_yielded_higher_payoff(SW,PL,at(V,PH),[Z1,T],[Z,S]).

SW = given_state(17)
PL = player(ann)
PH = [right, right, right, right]
Z1 = payoff(6), terminal(5)
T = strategy(1), [ (1, ann, down), (2, bob, down), (3, ann, down), (4, bob, down), (5, ann, down)]
Z = payoff(5), terminal(6)
S = strategy(17), [ (1, ann, down), (2, bob, down), (3, ann, down), (4, bob, down), (5, ann, right)] ;

V = vertex(5)
SW = given_state(17)
PL = player(ann)
PH = [right, right, right, right]
Z1 = payoff(6), terminal(5)
T = strategy(2), [ (1, ann, right), (2, bob, down), (3, ann, down), (4, bob, down), (5, ann, down)]
Z = payoff(5), terminal(6)
S = strategy(17), [ (1, ann, down), (2, bob, down), (3, ann, down), (4, bob, down), (5, ann, right)] 

Yes
?- 

*************************************************/


% an experimental code added: 14 Feb 2004

verify_beneficial_deviances_at(V,PL,state(W),R,DR):-
   T=strategy(It),S=strategy(_Is),
   PL=player(_J),V=vertex(_K),
   SW=given_state(W),state(W),
   findall(It,
     would_have_yielded_higher_payoff(
       SW,PL,at(V,_PH),[_Z1,(T,_)],[_Z,(S,_)]
     ),
   L),
   sort(L,R),
   event_description(R,_,DR).

verify_beneficial_deviances_at(V,PL,state(W)):-
   verify_beneficial_deviances_at(V,PL,state(W),R,_),
   nl,write(W;R),fail.



/*************************************************

% The following experimentations added: 14--15 Feb 2004

% The skimmings of beneficial deviances.
%---------------------------------------------------%

?- PL=player(ann),V=vertex(1),SW=given_state(W),
 findall(W,
   would_have_yielded_higher_payoff(SW,PL,at(V,_),_,_),
 R),
 all_states(O),subtract(O,R,P),event_description(P,_,Q),
 forall(member(X,P),(strategy_description(X,_,_,Y),nl,write(X:Y))).

1:[d, d, d, d, d]
4:[r, r, d, d, d]
5:[d, d, r, d, d]
9:[d, d, d, r, d]
13:[d, d, r, r, d]
16:[r, r, r, r, d]
17:[d, d, d, d, r]
20:[r, r, d, d, r]
21:[d, d, r, d, r]
25:[d, d, d, r, r]
29:[d, d, r, r, r]

PL = player(ann)
V = vertex(1)
SW = given_state(_G170)
W = _G170
R = [2, 2, 2, 2, 3, 3, 3, 3, 6|...]
O = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
P = [1, 4, 5, 9, 13, 16, 17, 20, 21|...]
Q = [[down, right], [down, right], [down, right], [down, right], [down, right]]
X = _G198
Y = _G204 

?- 

?- K=1, J=ann,
verify_beneficial_deviances_at(vertex(K),player(J),state(W)).

1;[]
2;[1, 5, 17, 21]
3;[4, 8, 20, 24]
4;[]
5;[]
6;[1, 5, 17, 21]
7;[4, 8, 20, 24]
8;[4, 20]
9;[]
10;[9, 13, 25, 29]
11;[12, 16, 28, 32]
12;[16, 32]
13;[]
14;[9, 13, 25, 29]
15;[12, 16, 28, 32]
16;[]
17;[]
18;[1, 5, 17, 21]
19;[4, 8, 20, 24]
20;[]
21;[]
22;[1, 5, 17, 21]
23;[4, 8, 20, 24]
24;[4, 20]
25;[]
26;[9, 13, 25, 29]
27;[12, 16, 28, 32]
28;[16, 32]
29;[]
30;[9, 13, 25, 29]
31;[12, 16, 28, 32]
32;[16]

No
?- state_description(2,_,C).

C = [r, d, d, d, d] 

Yes
?- state_description(A,_,[d,r,d,d,d]).

A = 3

Yes
?- member(X,[4,8,20,24]),state_description(X,_,C).

X = 4
C = [r, r, d, d, d] ;

X = 8
C = [r, r, r, d, d] ;

X = 20
C = [r, r, d, d, r] ;

X = 24
C = [r, r, r, d, r] ;

No
?- K=4, J=bob,
verify_beneficial_deviances_at(vertex(K),player(J),state(W)).

1;[]
2;[]
3;[]
4;[]
5;[]
6;[]
7;[]
8;[]
9;[1, 3]
10;[2, 4]
11;[1, 3]
12;[2, 4]
13;[5, 7]
14;[6, 8]
15;[5, 7]
16;[6, 8]
17;[25, 27]
18;[26, 28]
19;[25, 27]
20;[26, 28]
21;[29, 31]
22;[30, 32]
23;[29, 31]
24;[30, 32]
25;[]
26;[]
27;[]
28;[]
29;[]
30;[]
31;[]
32;[]

No
?- state_description(1,_,D).

D = [d, d, d, d, d] 

Yes
?- state_description(9,_,D).

D = [d, d, d, r, d] 

Yes

% more eraborate descriptions on the beneficial deviances.
%---------------------------------------------------%

?- V=vertex(5),T=(strategy(It),_),S=(strategy(Is),_),
   would_have_yielded_higher_payoff(SW,PL,at(V,PH),[Z1,T],[Z,S]),
   strategy_description(It,_,_,Dt),strategy_description(Is,_,_,Ds),
   Dt=[X1,X2,X3,X4,_X5],Ds=[X1,X2,X3,X4,_Y5],
   nl,write(V;(Is:Ds)->(It:Dt);Z->Z1),fail.

vertex(5);17:[d, d, d, d, r]->1:[d, d, d, d, d];payoff(5), terminal(6)->payoff(6), terminal(5)
vertex(5);18:[r, d, d, d, r]->2:[r, d, d, d, d];payoff(5), terminal(6)->payoff(6), terminal(5)
vertex(5);19:[d, r, d, d, r]->3:[d, r, d, d, d];payoff(5), terminal(6)->payoff(6), terminal(5)
vertex(5);20:[r, r, d, d, r]->4:[r, r, d, d, d];payoff(5), terminal(6)->payoff(6), terminal(5)
vertex(5);21:[d, d, r, d, r]->5:[d, d, r, d, d];payoff(5), terminal(6)->payoff(6), terminal(5)
vertex(5);22:[r, d, r, d, r]->6:[r, d, r, d, d];payoff(5), terminal(6)->payoff(6), terminal(5)
vertex(5);23:[d, r, r, d, r]->7:[d, r, r, d, d];payoff(5), terminal(6)->payoff(6), terminal(5)
vertex(5);24:[r, r, r, d, r]->8:[r, r, r, d, d];payoff(5), terminal(6)->payoff(6), terminal(5)
vertex(5);25:[d, d, d, r, r]->9:[d, d, d, r, d];payoff(5), terminal(6)->payoff(6), terminal(5)
vertex(5);26:[r, d, d, r, r]->10:[r, d, d, r, d];payoff(5), terminal(6)->payoff(6), terminal(5)
vertex(5);27:[d, r, d, r, r]->11:[d, r, d, r, d];payoff(5), terminal(6)->payoff(6), terminal(5)
vertex(5);28:[r, r, d, r, r]->12:[r, r, d, r, d];payoff(5), terminal(6)->payoff(6), terminal(5)
vertex(5);29:[d, d, r, r, r]->13:[d, d, r, r, d];payoff(5), terminal(6)->payoff(6), terminal(5)
vertex(5);30:[r, d, r, r, r]->14:[r, d, r, r, d];payoff(5), terminal(6)->payoff(6), terminal(5)
vertex(5);31:[d, r, r, r, r]->15:[d, r, r, r, d];payoff(5), terminal(6)->payoff(6), terminal(5)
vertex(5);32:[r, r, r, r, r]->16:[r, r, r, r, d];payoff(5), terminal(6)->payoff(6), terminal(5)

No
?- V=vertex(4),T=(strategy(It),_),S=(strategy(Is),_),
   would_have_yielded_higher_payoff(SW,PL,at(V,PH),[Z1,T],[Z,S]),
   strategy_description(It,_,_,Dt),strategy_description(Is,_,_,Ds),
   Dt=[X1,X2,X3,_X4,_X5],Ds=[X1,X2,X3,_Y4,_Y5],
   nl,write(V;(Is:Ds)->(It:Dt);Z->Z1),fail.

vertex(4);9:[d, d, d, r, d]->1:[d, d, d, d, d];payoff(5), terminal(5)->payoff(6), terminal(4)
vertex(4);10:[r, d, d, r, d]->2:[r, d, d, d, d];payoff(5), terminal(5)->payoff(6), terminal(4)
vertex(4);11:[d, r, d, r, d]->3:[d, r, d, d, d];payoff(5), terminal(5)->payoff(6), terminal(4)
vertex(4);12:[r, r, d, r, d]->4:[r, r, d, d, d];payoff(5), terminal(5)->payoff(6), terminal(4)
vertex(4);13:[d, d, r, r, d]->5:[d, d, r, d, d];payoff(5), terminal(5)->payoff(6), terminal(4)
vertex(4);14:[r, d, r, r, d]->6:[r, d, r, d, d];payoff(5), terminal(5)->payoff(6), terminal(4)
vertex(4);15:[d, r, r, r, d]->7:[d, r, r, d, d];payoff(5), terminal(5)->payoff(6), terminal(4)
vertex(4);16:[r, r, r, r, d]->8:[r, r, r, d, d];payoff(5), terminal(5)->payoff(6), terminal(4)
vertex(4);17:[d, d, d, d, r]->25:[d, d, d, r, r];payoff(6), terminal(4)->payoff(8), terminal(6)
vertex(4);18:[r, d, d, d, r]->26:[r, d, d, r, r];payoff(6), terminal(4)->payoff(8), terminal(6)
vertex(4);19:[d, r, d, d, r]->27:[d, r, d, r, r];payoff(6), terminal(4)->payoff(8), terminal(6)
vertex(4);20:[r, r, d, d, r]->28:[r, r, d, r, r];payoff(6), terminal(4)->payoff(8), terminal(6)
vertex(4);21:[d, d, r, d, r]->29:[d, d, r, r, r];payoff(6), terminal(4)->payoff(8), terminal(6)
vertex(4);22:[r, d, r, d, r]->30:[r, d, r, r, r];payoff(6), terminal(4)->payoff(8), terminal(6)
vertex(4);23:[d, r, r, d, r]->31:[d, r, r, r, r];payoff(6), terminal(4)->payoff(8), terminal(6)
vertex(4);24:[r, r, r, d, r]->32:[r, r, r, r, r];payoff(6), terminal(4)->payoff(8), terminal(6)

No
?- V=vertex(3),T=(strategy(It),_),S=(strategy(Is),_),
   would_have_yielded_higher_payoff(SW,PL,at(V,PH),[Z1,T],[Z,S]),
   strategy_description(It,_,_,Dt),strategy_description(Is,_,_,Ds),
   Dt=[X1,X2,_X3,_X4,_X5],Ds=[X1,X2,_Y3,_Y4,_Y5],
   nl,write(V;(Is:Ds)->(It:Dt);Z->Z1),fail.

vertex(3);5:[d, d, r, d, d]->1:[d, d, d, d, d];payoff(3), terminal(4)->payoff(4), terminal(3)
vertex(3);5:[d, d, r, d, d]->17:[d, d, d, d, r];payoff(3), terminal(4)->payoff(4), terminal(3)
vertex(3);6:[r, d, r, d, d]->2:[r, d, d, d, d];payoff(3), terminal(4)->payoff(4), terminal(3)
vertex(3);6:[r, d, r, d, d]->18:[r, d, d, d, r];payoff(3), terminal(4)->payoff(4), terminal(3)
vertex(3);7:[d, r, r, d, d]->3:[d, r, d, d, d];payoff(3), terminal(4)->payoff(4), terminal(3)
vertex(3);7:[d, r, r, d, d]->19:[d, r, d, d, r];payoff(3), terminal(4)->payoff(4), terminal(3)
vertex(3);8:[r, r, r, d, d]->4:[r, r, d, d, d];payoff(3), terminal(4)->payoff(4), terminal(3)
vertex(3);8:[r, r, r, d, d]->20:[r, r, d, d, r];payoff(3), terminal(4)->payoff(4), terminal(3)
vertex(3);9:[d, d, d, r, d]->13:[d, d, r, r, d];payoff(4), terminal(3)->payoff(6), terminal(5)
vertex(3);9:[d, d, d, r, d]->29:[d, d, r, r, r];payoff(4), terminal(3)->payoff(5), terminal(6)
vertex(3);10:[r, d, d, r, d]->14:[r, d, r, r, d];payoff(4), terminal(3)->payoff(6), terminal(5)
vertex(3);10:[r, d, d, r, d]->30:[r, d, r, r, r];payoff(4), terminal(3)->payoff(5), terminal(6)
vertex(3);11:[d, r, d, r, d]->15:[d, r, r, r, d];payoff(4), terminal(3)->payoff(6), terminal(5)
vertex(3);11:[d, r, d, r, d]->31:[d, r, r, r, r];payoff(4), terminal(3)->payoff(5), terminal(6)
vertex(3);12:[r, r, d, r, d]->16:[r, r, r, r, d];payoff(4), terminal(3)->payoff(6), terminal(5)
vertex(3);12:[r, r, d, r, d]->32:[r, r, r, r, r];payoff(4), terminal(3)->payoff(5), terminal(6)
vertex(3);21:[d, d, r, d, r]->1:[d, d, d, d, d];payoff(3), terminal(4)->payoff(4), terminal(3)
vertex(3);21:[d, d, r, d, r]->17:[d, d, d, d, r];payoff(3), terminal(4)->payoff(4), terminal(3)
vertex(3);22:[r, d, r, d, r]->2:[r, d, d, d, d];payoff(3), terminal(4)->payoff(4), terminal(3)
vertex(3);22:[r, d, r, d, r]->18:[r, d, d, d, r];payoff(3), terminal(4)->payoff(4), terminal(3)
vertex(3);23:[d, r, r, d, r]->3:[d, r, d, d, d];payoff(3), terminal(4)->payoff(4), terminal(3)
vertex(3);23:[d, r, r, d, r]->19:[d, r, d, d, r];payoff(3), terminal(4)->payoff(4), terminal(3)
vertex(3);24:[r, r, r, d, r]->4:[r, r, d, d, d];payoff(3), terminal(4)->payoff(4), terminal(3)
vertex(3);24:[r, r, r, d, r]->20:[r, r, d, d, r];payoff(3), terminal(4)->payoff(4), terminal(3)
vertex(3);25:[d, d, d, r, r]->13:[d, d, r, r, d];payoff(4), terminal(3)->payoff(6), terminal(5)
vertex(3);25:[d, d, d, r, r]->29:[d, d, r, r, r];payoff(4), terminal(3)->payoff(5), terminal(6)
vertex(3);26:[r, d, d, r, r]->14:[r, d, r, r, d];payoff(4), terminal(3)->payoff(6), terminal(5)
vertex(3);26:[r, d, d, r, r]->30:[r, d, r, r, r];payoff(4), terminal(3)->payoff(5), terminal(6)
vertex(3);27:[d, r, d, r, r]->15:[d, r, r, r, d];payoff(4), terminal(3)->payoff(6), terminal(5)
vertex(3);27:[d, r, d, r, r]->31:[d, r, r, r, r];payoff(4), terminal(3)->payoff(5), terminal(6)
vertex(3);28:[r, r, d, r, r]->16:[r, r, r, r, d];payoff(4), terminal(3)->payoff(6), terminal(5)
vertex(3);28:[r, r, d, r, r]->32:[r, r, r, r, r];payoff(4), terminal(3)->payoff(5), terminal(6)
vertex(3);29:[d, d, r, r, r]->13:[d, d, r, r, d];payoff(5), terminal(6)->payoff(6), terminal(5)
vertex(3);30:[r, d, r, r, r]->14:[r, d, r, r, d];payoff(5), terminal(6)->payoff(6), terminal(5)
vertex(3);31:[d, r, r, r, r]->15:[d, r, r, r, d];payoff(5), terminal(6)->payoff(6), terminal(5)
vertex(3);32:[r, r, r, r, r]->16:[r, r, r, r, d];payoff(5), terminal(6)->payoff(6), terminal(5)


*************************************************/


exisit_would_have_yielded_higher_payoff(X):-
   X=[SW, PL, at(V,H), D, D1],
   would_have_yielded_higher_payoff(
       SW, PL, at(V,H), D, D1
   )
   ->true.

exisit_would_have_yielded_higher_payoff(X,Tj,Sj):-
   X=[SW, PL, at(V,H), D, D1],
   would_have_yielded_higher_payoff(
       SW, PL, at(V,H), D, D1,Tj,Sj
   )
   ->true.

% not correct modeling but it may be seen as a weaker notion.

event_would_have_been_higher(LWS,at(V),PL):-
   V=vertex(_),
   PL =player(_),
   move(V,PL),
   SW=given_state(W),
   X=[SW, PL, at(V,_H), _D, _D1],
   findall(W,
    (
     state(W),
     exisit_would_have_yielded_higher_payoff(X)
    ),
   LWS).

:- dynamic  event_would_have_yielded_higher_0/4.

event_would_have_been_higher(LWS,At,PL,Str):-
   clause(event_would_have_been_higher_0(LWS,At,PL,Str),true).

event_would_have_been_higher(LWS,at(V),PL,strategy(Id,Tj)):-
   \+ clause(event_would_have_been_higher_0(_,_,_,_),true),
   V=vertex(_),
   PL =player(J),
   move(V,PL),
   SW=given_state(W),
   X=[SW, PL, at(V,_H), _D1, _D],
   strategy_of_player(J,Id,Tj),
   findall(W,
    (
     state(W),
     exisit_would_have_yielded_higher_payoff(X,Tj,_Sj)
    ),
   LWS).


knowledge_of_would_have_been_higher((DK,KE),(D,E),at(V),PL,strategy(Id,Tj)):-
   event_would_have_been_higher(E,at(V),PL,strategy(Id,Tj)),
   knowledge_operator(KE,E,_,PL,_),
   event_description(E,_,D),
   event_description(KE,_,DK).



/*************************************************

?- event_would_have_been_higher(NR,at(V),PL,SL),NR\=[].

NR = [2, 6, 10, 14, 18, 22, 26, 30]
V = vertex(1)
PL = player(ann)
SL = strategy(1, [ (1, down), (3, down), (5, down)]) ;

NR = [3, 7, 8, 11, 15, 19, 23, 24, 27|...]
V = vertex(1)
PL = player(ann)
SL = strategy(2, [ (1, right), (3, down), (5, down)]) ;

NR = [2, 6, 10, 14, 18, 22, 26, 30]
V = vertex(1)
PL = player(ann)
SL = strategy(3, [ (1, down), (3, down), (5, down)]) ;

NR = [3, 7, 8, 11, 15, 19, 23, 24, 27|...]
V = vertex(1)
PL = player(ann)
SL = strategy(4, [ (1, right), (3, down), (5, down)]) 

Yes

?- event_would_have_been_higher(LWS,AT,PL),hexa_event(LWS,_,Hx),nl,write(AT:PL:Hx:LWS),fail.

at(vertex(1)):player(ann):67766777:[2, 3, 6, 7, 8, 10, 11, 12, 14, 15, 18, 19, 22, 23, 24, 26, 27, 28, 30, 31, 32]
at(vertex(3)):player(ann):0ff00fff:[5, 6, 7, 8, 9, 10, 11, 12, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32]
at(vertex(5)):player(ann):0000ffff:[17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32]
at(vertex(2)):player(bob):3c3f3f3c:[3, 4, 5, 6, 11, 12, 13, 14, 15, 16, 19, 20, 21, 22, 23, 24, 27, 28, 29, 30]
at(vertex(4)):player(bob):00ffff00:[9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24]

No
?- 

*************************************************/


% inferiors to the inductive choice
%---------------------------------------------------%
% added: 14--15 Feb 2004

% The following corresponds to [h_i^v([s];b_i) > h_i^v([s])].

inferior_set_of_inductive_choice(DE,E,at(V),PL,strategy(Bid,Tj)):-
   inductive_choice_in_profile(Bid,_,_),
   event_would_have_been_higher(E,at(V),PL,strategy(Bid,Tj)),
   event_description(E,_,DE).



/*************************************************

?- inferior_set_of_inductive_choice(DE,E,at(V),PL,strategy(Bid,Tj)),
 nl,write(V;PL;DE;E),fail.

vertex(1);player(ann);[[right], [down], [down, right], [down, right], [down, right]];[2, 6, 10, 14, 18, 22, 26, 30]
vertex(3);player(ann);[[down, right], [down, right], [right], [down], [down, right]];[5, 6, 7, 8, 21, 22, 23, 24]
vertex(5);player(ann);[[down, right], [down, right], [down, right], [down, right], [right]];[17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32]
vertex(2);player(bob);[[down, right], [right], [down], [down, right], [down, right]];[3, 4, 11, 12, 19, 20, 27, 28]
vertex(4);player(bob);[[down, right], [down, right], [down, right], [right], [down]];[9, 10, 11, 12, 13, 14, 15, 16]

No
?- inferior_set_of_inductive_choice(DE,E,at(V),PL,strategy(Bid,Tj)),
move(V,PL),
knowledge_operator(KE,E,_,PL,_),hexa_event(E,_,H),hexa_event(KE,_,Hk),
nl,write(V;PL),nl,write(inf:E;H),nl,write(know:KE;Hk),fail.

dvertex(1);player(ann)
inf:[2, 6, 10, 14, 18, 22, 26, 30];44444444
know:[];00000000
vertex(3);player(ann)
inf:[5, 6, 7, 8, 21, 22, 23, 24];0f000f00
know:[];00000000
vertex(5);player(ann)
inf:[17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32];0000ffff
know:[17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32];0000ffff
vertex(2);player(bob)
inf:[3, 4, 11, 12, 19, 20, 27, 28];30303030
know:[];00000000
vertex(4);player(bob)
inf:[9, 10, 11, 12, 13, 14, 15, 16];00ff0000
know:[];00000000

No
?-

*************************************************/


% an experimental code added: 15 Feb 2004

test_inductive_constraints:-
   bag0(A,[d,r],5),
   findall((V,R),inductive_schema(V,A,R),L),
   nl,write(A;L),
   fail.

inductive_schema(vertex(5),[d,_,d,_,X5],F5):-
   X5=d->F5=1;F5=0.
inductive_schema(vertex(4),[_,d,_,X4,d],F4):-
   X4=d->F4=1;F4=0.
inductive_schema(vertex(3),[d,_,X3,d,X5],F3):-
   (X3=d,X5=d)->F3=1;F3=0.
inductive_schema(vertex(2),[_,X2,d,X4,_],F2):-
   (X2=d,X4=d)->F2=1;F2=0.
inductive_schema(vertex(1),[X1,d,X3,_,X5],F1):-
   (X1=d,X3=d,X5=d)->F1=1;F1=0.
 

/*************************************************

?- test_inductive_constraints.

[d, d, d, d, d];[ (vertex(5), 1), (vertex(4), 1), (vertex(3), 1), (vertex(2), 1), (vertex(1), 1)]
[r, d, d, d, d];[ (vertex(4), 1), (vertex(2), 1), (vertex(1), 0)]
[d, r, d, d, d];[ (vertex(5), 1), (vertex(3), 1), (vertex(2), 0)]
[r, r, d, d, d];[ (vertex(2), 0)]
[d, d, r, d, d];[ (vertex(4), 1), (vertex(3), 0), (vertex(1), 0)]
[r, d, r, d, d];[ (vertex(4), 1), (vertex(1), 0)]
[d, r, r, d, d];[ (vertex(3), 0)]
[r, r, r, d, d];[]
[d, d, d, r, d];[ (vertex(5), 1), (vertex(4), 0), (vertex(2), 0), (vertex(1), 1)]
[r, d, d, r, d];[ (vertex(4), 0), (vertex(2), 0), (vertex(1), 0)]
[d, r, d, r, d];[ (vertex(5), 1), (vertex(2), 0)]
[r, r, d, r, d];[ (vertex(2), 0)]
[d, d, r, r, d];[ (vertex(4), 0), (vertex(1), 0)]
[r, d, r, r, d];[ (vertex(4), 0), (vertex(1), 0)]
[d, r, r, r, d];[]
[r, r, r, r, d];[]
[d, d, d, d, r];[ (vertex(5), 0), (vertex(3), 0), (vertex(2), 1), (vertex(1), 0)]
[r, d, d, d, r];[ (vertex(2), 1), (vertex(1), 0)]
[d, r, d, d, r];[ (vertex(5), 0), (vertex(3), 0), (vertex(2), 0)]
[r, r, d, d, r];[ (vertex(2), 0)]
[d, d, r, d, r];[ (vertex(3), 0), (vertex(1), 0)]
[r, d, r, d, r];[ (vertex(1), 0)]
[d, r, r, d, r];[ (vertex(3), 0)]
[r, r, r, d, r];[]
[d, d, d, r, r];[ (vertex(5), 0), (vertex(2), 0), (vertex(1), 0)]
[r, d, d, r, r];[ (vertex(2), 0), (vertex(1), 0)]
[d, r, d, r, r];[ (vertex(5), 0), (vertex(2), 0)]
[r, r, d, r, r];[ (vertex(2), 0)]
[d, d, r, r, r];[ (vertex(1), 0)]
[r, d, r, r, r];[ (vertex(1), 0)]
[d, r, r, r, r];[]
[r, r, r, r, r];[]

No
?- 

*************************************************/


% The following corresponds to [h_i^v(b) > h_i^v(b;[s]^v)].

event_inferior_to_inductive_choice_at(V,E,DE):-
   V =vertex(K),
   PL =player(J),
   move(V,PL),
   non_inductive_strategies_at(V,NIS,_),
   findall(W,
    (
     would_have_been_lower_than_inductive_payoff(_,_,(K,J,A)),
     member(W,NIS),
     state_description(W,KJAs,_),
     member((K,J,A),KJAs)
    ),
   F),
   sort(F,E),
   event_description(E,_,DE).

would_have_been_lower_than_inductive_payoff(Db,Dt,(K,J,A)):-
   inductive_choice_in_profile(Ib,_,_),
   PL =player(J),
   V =vertex(K),
   move(V,PL),
   Db=[(payoff(Ub),Zb),(strategy(Ib),B)],
   Dt=[(payoff(Ut),Zt),(strategy(It),T)],
   Xb =[V,PH,(Ib,B),Zb],
   Xt =[V,PH,(It,T),Zt],
   conditional_payoff(Xb,PL,payoff(Ub)),
   conditional_payoff(Xt,PL,payoff(Ut)),
   Ut < Ub,
   deviate_only_at(V,PL,B,T,(K,J,A)).

deviate_only_at(vertex(K),player(J),S,T,(K,J,A)):-
   subtract(T,S,[(K,J,A)]).


/*************************************************

?- would_have_been_lower_than_inductive_payoff(_,_,C).

C = 1, ann, right ;

C = 3, ann, right ;

C = 5, ann, right ;

C = 2, bob, right ;

C = 4, bob, right ;

No
?- event_inferior_to_inductive_choice_at(V,E,DE),move(V,PL),
knowledge_operator(KE,E,_,PL,_),hexa_event(E,_,H),hexa_event(KE,_,Hk),
nl,write(V;PL),nl,write(inf:E;H),nl,write(know:KE;Hk),fail.

vertex(1);player(ann)
inf:[2, 4, 6, 8, 10, 12, 14, 16, 18, 20, 22, 24, 26, 28, 30, 32];55555555
know:[2, 4, 6, 8, 10, 12, 14, 16, 18, 20, 22, 24, 26, 28, 30, 32];55555555
vertex(3);player(ann)
inf:[5, 6, 7, 8, 13, 14, 15, 16, 21, 22, 23, 24, 29, 30, 31, 32];0f0f0f0f
know:[5, 6, 7, 8, 13, 14, 15, 16, 21, 22, 23, 24, 29, 30, 31, 32];0f0f0f0f
vertex(5);player(ann)
inf:[17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32];0000ffff
know:[17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32];0000ffff
vertex(2);player(bob)
inf:[3, 4, 7, 8, 11, 12, 15, 16, 19, 20, 23, 24, 27, 28, 31, 32];33333333
know:[3, 4, 7, 8, 11, 12, 15, 16, 19, 20, 23, 24, 27, 28, 31, 32];33333333
vertex(4);player(bob)
inf:[9, 10, 11, 12, 13, 14, 15, 16, 25, 26, 27, 28, 29, 30, 31, 32];00ff00ff
know:[9, 10, 11, 12, 13, 14, 15, 16, 25, 26, 27, 28, 29, 30, 31, 32];00ff00ff

No
?- findall(DK,(
     event_inferior_to_inductive_choice_at(V,E,DE),move(V,PL),
     knowledge_operator(KE,E,_,PL,_),complement(KE,_,DK)),
  L),
  intersection_of_lists(L,P),event_description(P,_,Q).

DK = _G172
V = _G157
E = _G158
DE = _G159
PL = _G162
KE = _G164
L = [[1, 3, 5, 7, 9, 11, 13, 15|...], [1, 2, 3, 4, 9, 10, 11|...], [1, 2, 3, 4, 5, 6|...], [1, 2, 5, 6, 9|...], [1, 2, 3, 4|...]]
P = [1]
Q = [[down], [down], [down], [down], [down]] 

Yes
?- inferior_set_of_inductive_choice(DE,E,at(V),PL,_),
event_inferior_to_inductive_choice_at(V,Ea,DEa),
hexa_event(E,_,H),hexa_event(Ea,_,Ha),
subtract(Ea,E,Dif),subtract(E,Ea,Dif1),
event_description(Dif,_,DD),
nl,write(V;PL),
nl,write(inf:H;DE;E),
nl,write(inf_atv:Ha;DEa;Ea),
nl,write(diff:Dif1;Dif;DD),
fail.

vertex(1);player(ann)
inf:44444444;[[right], [down], [down, right], [down, right], [down, right]];[2, 6, 10, 14, 18, 22, 26, 30]
inf_atv:55555555;[[right], [down, right], [down, right], [down, right], [down, right]];[2, 4, 6, 8, 10, 12, 14, 16, 18, 20, 22, 24, 26, 28, 30, 32]
diff:[];[4, 8, 12, 16, 20, 24, 28, 32];[[right], [right], [down, right], [down, right], [down, right]]
vertex(3);player(ann)
inf:0f000f00;[[down, right], [down, right], [right], [down], [down, right]];[5, 6, 7, 8, 21, 22, 23, 24]
inf_atv:0f0f0f0f;[[down, right], [down, right], [right], [down, right], [down, right]];[5, 6, 7, 8, 13, 14, 15, 16, 21, 22, 23, 24, 29, 30, 31, 32]
diff:[];[13, 14, 15, 16, 29, 30, 31, 32];[[down, right], [down, right], [right], [right], [down, right]]
vertex(5);player(ann)
inf:0000ffff;[[down, right], [down, right], [down, right], [down, right], [right]];[17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32]
inf_atv:0000ffff;[[down, right], [down, right], [down, right], [down, right], [right]];[17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32]
diff:[];[];[[], [], [], [], []]
vertex(2);player(bob)
inf:30303030;[[down, right], [right], [down], [down, right], [down, right]];[3, 4, 11, 12, 19, 20, 27, 28]
inf_atv:33333333;[[down, right], [right], [down, right], [down, right], [down, right]];[3, 4, 7, 8, 11, 12, 15, 16, 19, 20, 23, 24, 27, 28, 31, 32]
diff:[];[7, 8, 15, 16, 23, 24, 31, 32];[[down, right], [right], [right], [down, right], [down, right]]
vertex(4);player(bob)
inf:00ff0000;[[down, right], [down, right], [down, right], [right], [down]];[9, 10, 11, 12, 13, 14, 15, 16]
inf_atv:00ff00ff;[[down, right], [down, right], [down, right], [right], [down, right]];[9, 10, 11, 12, 13, 14, 15, 16, 25, 26, 27, 28, 29, 30, 31, 32]
diff:[];[25, 26, 27, 28, 29, 30, 31, 32];[[down, right], [down, right], [down, right], [right], [right]]

No
?-

% an old result (when path assumed real)

vertex(1);player(ann)
inf:[[right], [down], [down, right], [down, right], [down, right]];44444444;[2, 6, 10, 14, 18, 22, 26, 30]
inf_atv:[[right], [down, right], [down, right], [down, right], [down, right]];55555555;[2, 4, 6, 8, 10, 12, 14, 16, 18, 20, 22, 24, 26, 28, 30, 32]
diff:[];[4, 8, 12, 16, 20, 24, 28, 32];[[right], [right], [down, right], [down, right], [down, right]]
vertex(3);player(ann)
inf:[[down], [down, right], [right], [down], [down, right]];0a000a00;[5, 7, 21, 23]
inf_atv:[[down, right], [down, right], [right], [down, right], [down, right]];0f0f0f0f;[5, 6, 7, 8, 13, 14, 15, 16, 21, 22, 23, 24, 29, 30, 31, 32]
diff:[];[6, 8, 13, 14, 15, 16, 22, 24, 29, 30, 31, 32];[[down, right], [down, right], [right], [down, right], [down, right]]
vertex(5);player(ann)
inf:[[down], [down, right], [down], [down, right], [right]];0000a0a0;[17, 19, 25, 27]
inf_atv:[[down, right], [down, right], [down, right], [down, right], [right]];0000ffff;[17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32]
diff:[];[18, 20, 21, 22, 23, 24, 26, 28, 29, 30, 31, 32];[[down, right], [down, right], [down, right], [down, right], [right]]
vertex(2);player(bob)
inf:[[down, right], [right], [down], [down, right], [down, right]];30303030;[3, 4, 11, 12, 19, 20, 27, 28]
inf_atv:[[down, right], [right], [down, right], [down, right], [down, right]];33333333;[3, 4, 7, 8, 11, 12, 15, 16, 19, 20, 23, 24, 27, 28, 31, 32]
diff:[];[7, 8, 15, 16, 23, 24, 31, 32];[[down, right], [right], [right], [down, right], [down, right]]
vertex(4);player(bob)
inf:[[down, right], [down], [down, right], [right], [down]];00cc0000;[9, 10, 13, 14]
inf_atv:[[down, right], [down, right], [down, right], [right], [down, right]];00ff00ff;[9, 10, 11, 12, 13, 14, 15, 16, 25, 26, 27, 28, 29, 30, 31, 32]
diff:[];[11, 12, 15, 16, 25, 26, 27, 28, 29, 30, 31, 32];[[down, right], [down, right], [down, right], [right], [down, right]]


*************************************************/


% (ex post) rationality of players
%---------------------------------------------------%

% `In a given state w of the world, call i 
% rational at v if there is no strategy 
% that i knows would have yielded him 
% a conditional payoff at v larger than that
% which in fact he gets.'
% `I.e., larger than i's conditional payoff at v 
% for [s](w).' (Aumann,1995 p.9, and footnote 4.)


rational_choice_wrt(SLA,V,PL,NR,R):-
   PL =player(_J),
   V =vertex(_),
   SLA=strategy(_Id,_T),
   event_would_have_been_higher(NR,at(V),PL,SLA),
   does_not_know(R,NR,_,PL,_).

is_rational_at(V,PL,SLR1,Rv):-
   PL =player(_),
   V=vertex(_),
   move(V,PL),
   findall([SL,R,Hx],rational_choice_wrt_hx(SL,V,PL,_,R,Hx),SLR1),
   sort(SLR1,SLR2),
  %findall([SL,Hx],member([SL,R,Hx],SLR2),SLR),
   findall(R,member([SL,R,Hx],SLR2),RVS),
   intersection_of_lists(RVS,Rv).

is_rational(R,Hx,D):-
   findall(Rv,is_rational_at(_V,_PL,_,Rv),RvS),
   intersection_of_lists(RvS,R),
   hexa_event(R,_,Hx),
   event_description(R,_,D).

% synonyms of hexa representation.

rational_choice_wrt_hx(SLA,V,PL,NR,R,[Hnx,Hrx]):-
   rational_choice_wrt(SLA,V,PL,NR,R),
   hexa_event(NR,_,Hnx),
   hexa_event(R,_,Hrx).

rational_choice_wrt_hx_1(SLA,V,PL,NR,R,[Hx2,NRS,RS]):-
   rational_choice_wrt_hx(SLA,V,PL,NR,R,Hx2),
   event_description(NR,_,NRS),
   event_description(R,_,RS).

is_rational_at_hx(V,PL,SLR,R,Hx):-
   is_rational_at(V,PL,SLR,R),
   hexa_event(R,_,Hx).

is_rational_at_hx_1(V,PL,SLR,R,[Hx,Strategies]):-
   is_rational_at_hx(V,PL,SLR,R,Hx),
   event_description(R,_,Strategies).




% Following two simulations are done under the partition 
% in which both players know only about own strategy 
% and totally ignorant about what the strategy of opponent is.
% --- so `nomadic', which I will call later. 

/*************************************************

% simulation (1): 
% states consist of the whole strategy profiles and 
% partitions wrt which the strategies are measurable
% for each player but not measurable for any strategies 
% of the opponent.

?- generate_states(A,X,N).

A = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
X = [1, 1, 1, 1, 1, 1, 1, 1, 1|...]
N = 32 

Yes
?- is_rational(A,B,C),common_knowledge(CKR,on(A),S).

A = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
B = ffff0000
C = [[down, right], [down, right], [down, right], [down, right], [down]]
CKR = []
S = 16, [[down, right], [down, right], [down, right], [down, right], [down]] 

Yes
?-


?- rational_choice_wrt_hx_1(Thres,vertex(1),player(ann),NR,R,[H,DNR,DR]).

Thres = strategy(1, [ (1, down), (3, down), (5, down)])
NR = [2, 6, 10, 14, 18, 22, 26, 30]
R = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
H = ['44444444', ffffffff]
DNR = [[right], [down], [down, right], [down, right], [down, right]]
DR = [[down, right], [down, right], [down, right], [down, right], [down, right]] ;

Thres = strategy(2, [ (1, right), (3, down), (5, down)])
NR = [3, 7, 8, 11, 15, 19, 23, 24, 27|...]
R = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
H = ['23222322', ffffffff]
DNR = [[down, right], [right], [down, right], [down, right], [down, right]]
DR = [[down, right], [down, right], [down, right], [down, right], [down, right]] 

Yes
?- rational_choice_wrt_hx_1(Thres,vertex(5),player(ann),NR,R,[H,DNR,DR]).

Thres = strategy(1, [ (1, down), (3, down), (5, down)])
NR = [17, 18, 19, 20, 21, 22, 23, 24, 25|...]
R = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
H = ['0000ffff', ffff0000]
DNR = [[down, right], [down, right], [down, right], [down, right], [right]]
DR = [[down, right], [down, right], [down, right], [down, right], [down]] ;

Thres = strategy(2, [ (1, right), (3, down), (5, down)])
NR = [17, 18, 19, 20, 21, 22, 23, 24, 25|...]
R = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
H = ['0000ffff', ffff0000]
DNR = [[down, right], [down, right], [down, right], [down, right], [right]]
DR = [[down, right], [down, right], [down, right], [down, right], [down]] 

Yes
?-


?- is_rational_at_hx_1(V,PL,SLR,R,[Hx,Sp]),
nl,write(V;PL;Hx;R;Sp),fail.

vertex(1);player(ann);ffffffff;[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32];[[down, right], [down, right], [down, right], [down, right], [down, right]]
vertex(3);player(ann);ffffffff;[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32];[[down, right], [down, right], [down, right], [down, right], [down, right]]
vertex(5);player(ann);ffff0000;[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16];[[down, right], [down, right], [down, right], [down, right], [down]]
vertex(2);player(bob);ffffffff;[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32];[[down, right], [down, right], [down, right], [down, right], [down, right]]
vertex(4);player(bob);ffffffff;[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32];[[down, right], [down, right], [down, right], [down, right], [down, right]]

No
?- 

*************************************************/


/*************************************************

% simulation (2): 
% A trivial case of non empty common knowledge of rationality
% which was suggested in the proof of Theorem B in Aumann(1995).
% There exisits only a state which maps the backward induction choice.


?- generate_states([1],X,N).

X = [1, 0, 0, 0, 0, 0, 0, 0, 0|...]
N = 1 

Yes
?- state(W).

W = 1 ;

No
?- is_rational_at_hx_1(V,PL,SLR,R,[Hx,Sp]),
    nl,write(V;PL;Hx;R;Sp),fail.

vertex(1);player(ann);1;[1];[[down], [down], [down], [down], [down]]
vertex(3);player(ann);1;[1];[[down], [down], [down], [down], [down]]
vertex(5);player(ann);1;[1];[[down], [down], [down], [down], [down]]
vertex(2);player(bob);1;[1];[[down], [down], [down], [down], [down]]
vertex(4);player(bob);1;[1];[[down], [down], [down], [down], [down]]

No
?- is_rational(A,B,C).

A = [1]
B = 1
C = [[down], [down], [down], [down], [down]] ;

No
?- common_knowledge(CKE,on(E),A).

CKE = [1]
E = [1]
A = 1, [[down], [down], [down], [down], [down]] ;

CKE = []
E = []
A = 0, [[], [], [], [], []] ;

No
?-

*************************************************/


% (ex post) material rationality of players
%---------------------------------------------------%
% a weaker version of rationality in Aumann(1998).

% `call i ex post materially rational if he is ex post 
% rational each of his reached vertex.'
% (Aumann ,1998 p.99)

% Although generally it is not sufficient to yield inductive choices, 
% is the case for Game 3 in Aumann(1995), a centipade game of Rosenthal, 
% and so our case of modeling in this program.


is_M_rational_at(V,PL,[SLR1,Rv,UR],Rmv):-
   is_rational_at(V,PL,SLR1,Rv),
   event_not_reached(V,UR),
   union(Rv,UR,Rm1),
   sort(Rm1,Rmv).

is_M_rational(RM,Hx,D):-
   findall(Rv,is_M_rational_at(_V,_PL,_,Rv),RMv),
   intersection_of_lists(RMv,RM),
   hexa_event(RM,_,Hx),
   event_description(RM,_,D).

event_not_reached(V,Unreached):-
   event_reached(V,Reached),
   complement(Reached,_,Unreached).

event_reached(V,Reached):-
   V=vertex(_),
   V,
   findall(W,
    (
     is_reached_by(V,_Id,S,_,_),
     state_description(W,S)
    ),
   Reached).

is_reached_by(V,Id,S,H,F):-
   track_back_history(V,H),
   strategy_description(Id,S,D,_),
   append(H,F,D). 


/*************************************************

?- event_reached(V,Reached),hexa_event(Reached,_,H),nl,write(V;H;Reached),fail.

vertex(1);ffffffff;[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32]
vertex(2);55555555;[2, 4, 6, 8, 10, 12, 14, 16, 18, 20, 22, 24, 26, 28, 30, 32]
vertex(3);11111111;[4, 8, 12, 16, 20, 24, 28, 32]
vertex(4);01010101;[8, 16, 24, 32]
vertex(5);00010001;[16, 32]

No
?- event_not_reached(V,Reached),hexa_event(Reached,_,H),nl,write(V;H;Reached),fail.

vertex(1);00000000;[]
vertex(2);aaaaaaaa;[1, 3, 5, 7, 9, 11, 13, 15, 17, 19, 21, 23, 25, 27, 29, 31]
vertex(3);eeeeeeee;[1, 2, 3, 5, 6, 7, 9, 10, 11, 13, 14, 15, 17, 18, 19, 21, 22, 23, 25, 26, 27, 29, 30, 31]
vertex(4);fefefefe;[1, 2, 3, 4, 5, 6, 7, 9, 10, 11, 12, 13, 14, 15, 17, 18, 19, 20, 21, 22, 23, 25, 26, 27, 28, 29, 30, 31]
vertex(5);fffefffe;[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31]

No
?- is_M_rational_at(A,B,_,D),
    hexa_event(D,_,H),nl,write(A;B;H;D),fail.

vertex(1);player(ann);ffffffff;[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32]
vertex(3);player(ann);ffffffff;[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32]
vertex(5);player(ann);ffffffff;[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32]
vertex(2);player(bob);ffffffff;[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32]
vertex(4);player(bob);ffffffff;[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32]

No
?- is_M_rational(A,B,C).

A = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
B = ffffffff
C = [[down, right], [down, right], [down, right], [down, right], [down, right]] ;

No
?- common_knowledge(A,B,C).

A = []
B = on([1, 2, 3, 4, 5, 6, 7, 8|...])
C = 32, [[down, right], [down, right], [down, right], [down, right], [down, right]] 

Yes
?-

% Thus, CKR is included I=[1] is trivial. 

*************************************************/

% yet another stronger rationality (i.e., ignorance of 
% possible profitable deviances across the vertices).
%---------------------------------------------------%

is_rational_at_0(V,PL,NR,R):-
   PL =player(_J),
   PL,
   V=vertex(_),
   V,
   event_would_have_been_higher(NR,at(V),PL),
   does_not_know(R,NR,_,PL,_Part).


/*************************************************

% not correct but a weaker notion.

?- event_would_have_been_higher(LWS,AT,PL),hexa_event(LWS,_,Hx),
knowledge_operator(KE,LWS,Len,PL,Par),hexa_event(KE,_,Hxk),
complement(KE,_,R),hexa_event(R,_,Hxr).

LWS = [2, 3, 6, 7, 8, 10, 11, 12, 14|...]
AT = at(vertex(1))
PL = player(ann)
Hx = '67766777'
KE = [22, 24, 30, 32]
Len = len(21)
Par = [7]
Hxk = '00000505'
R = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
Hxr = fffffafa 

Yes
?- event_would_have_been_higher(LWS,AT,PL),hexa_event(LWS,_,Hx),
does_not_know(KE,LWS,Len,PL,Par),hexa_event(KE,_,Hxk).

LWS = [2, 3, 6, 7, 8, 10, 11, 12, 14|...]
AT = at(vertex(1))
PL = player(ann)
Hx = '67766777'
KE = [1, 2, 3, 4, 5, 6, 7, 8, 9|...]
Len = len(21)
Par = [7]
Hxk = fffffafa 

Yes
?- is_rational_at_0(V,PL,NR,RV),
 hexa_event(RV,_,Hx),nl,write(V:PL:Hx:RV),fail.

vertex(1):player(ann):fffffafa:[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 23, 25, 26, 27, 28, 29, 31]
vertex(3):player(ann):fffff0f0:[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 25, 26, 27, 28]
vertex(5):player(ann):ffff0000:[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16]
vertex(2):player(bob):ffffffff:[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32]
vertex(4):player(bob):ffffffff:[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32]

No
?- 

*************************************************/



% generating non trivial CKR (CKI) of backward induction.
%---------------------------------------------------%
% The following observations by using find_non_trivila_CKR/3 are
% assuming somewhat nomadic knowledge system such that 
% where strategies are measurable only for oneself, i.e., 
% the players know only his/her own strategy.
% 17 Feb 2005.


find_non_trivial_CKR(N,A,B):-
   generate_states(A,[1|_X],N),
   forall(player(I),make_strategies_measurable(I)),
   R = [1],
   common_knowledge(CKR,on(R),B),
   CKR \= [].


/*************************************************

?- find_non_trivial_CKR(2,A,B).

(...)
A = [1, 32]
B = 1, [[down], [down], [down], [down], [down]] ;

No
?- common_knowledge(CKE,on(E),A).

CKE = [1]
E = [1, 32]
A = 2, [[down, right], [down, right], [down, right], [down, right], [down, right]] ;

CKE = [1]
E = [1]
A = 1, [[down], [down], [down], [down], [down]] ;

CKE = []
E = [32]
A = 1, [[right], [right], [right], [right], [right]] ;

CKE = []
E = []
A = 0, [[], [], [], [], []] ;

No
?- findall(A,find_non_trivial_CKR(2,[1,A],B),L),nl,write(L).

[4, 7, 8, 10, 12, 13, 14, 15, 16, 19, 20, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32]

A = _G160
B = _G165
L = [4, 7, 8, 10, 12, 13, 14, 15, 16|...] 

Yes
?- findall(A,find_non_trivial_CKR(3,[1|A],B),L),flatten(L,F),sort(F,G),nl,write(G).

[4, 7, 8, 10, 12, 13, 14, 15, 16, 19, 20, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32]

A = _G161
B = _G165
L = [[4, 7], [4, 8], [4, 10], [4, 12], [4, 13], [4, 14], [4, 15], [4|...], [...|...]|...]
F = [4, 7, 4, 8, 4, 10, 4, 12, 4|...]
G = [4, 7, 8, 10, 12, 13, 14, 15, 16|...] 

Yes
?- partition(A,B,C),event_description(B,_,D),nl,write(A;B;C;D),fail.

player(ann);[1];0;[[down], [down], [down], [down], [down]]
player(ann);[31];1;[[down], [right], [right], [right], [right]]
player(ann);[32];2;[[right], [right], [right], [right], [right]]
player(bob);[1];0;[[down], [down], [down], [down], [down]]
player(bob);[31, 32];1;[[down, right], [right], [right], [right], [right]]

No
?- common_knowledge(A,B,C).

A = [1, 31, 32]
B = on([1, 31, 32])
C = 3, [[down, right], [down, right], [down, right], [down, right], [down, right]] ;

A = [1]
B = on([1, 31])
C = 2, [[down], [down, right], [down, right], [down, right], [down, right]] ;

A = [1]
B = on([1, 32])
C = 2, [[down, right], [down, right], [down, right], [down, right], [down, right]] ;

A = [31, 32]
B = on([31, 32])
C = 2, [[down, right], [right], [right], [right], [right]] ;

A = [1]
B = on([1])
C = 1, [[down], [down], [down], [down], [down]] ;

A = []
B = on([31])
C = 1, [[down], [right], [right], [right], [right]] ;

A = []
B = on([32])
C = 1, [[right], [right], [right], [right], [right]] ;

A = []
B = on([])
C = 0, [[], [], [], [], []] ;

No
?- setof(A,find_non_trivial_CKR(4,[1|A],B),L),
length(L,M),flatten(L,P),sort(P,Q),nl,write(Q).

[4, 7, 8, 10, 12, 13, 14, 15, 16, 19, 20, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32]

A = _G15
B = 1, [[down], [down], [down], [down], [down]]
L = [[4, 7, 8], [4, 7, 10], [4, 7, 12], [4, 7, 13], [4, 7, 14], [4, 7, 15], [4, 7|...], [4|...], [...|...]|...]
M = 1330
P = [4, 7, 8, 4, 7, 10, 4, 7, 12|...]
Q = [4, 7, 8, 10, 12, 13, 14, 15, 16|...] 

Yes
?- member(X,
[1, 4, 7, 8, 10, 12, 13, 14, 15, 16, 19, 20, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32]),
state_description(X,_,A),nl,write(X;A),fail.

1;[d, d, d, d, d]
4;[r, r, d, d, d]
7;[d, r, r, d, d]
8;[r, r, r, d, d]
10;[r, d, d, r, d]
12;[r, r, d, r, d]
13;[d, d, r, r, d]
14;[r, d, r, r, d]
15;[d, r, r, r, d]
16;[r, r, r, r, d]
19;[d, r, d, d, r]
20;[r, r, d, d, r]
23;[d, r, r, d, r]
24;[r, r, r, d, r]
25;[d, d, d, r, r]
26;[r, d, d, r, r]
27;[d, r, d, r, r]
28;[r, r, d, r, r]
29;[d, d, r, r, r]
30;[r, d, r, r, r]
31;[d, r, r, r, r]
32;[r, r, r, r, r]

No
?-

% Note:
% The complementary set of the above consists of states where
% there is a single deviator from inductive choice.

?- state_description(X,_,A),\+ member(X,
[1, 4, 7, 8, 10, 12, 13, 14, 15, 16, 19, 20, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32]),
nl,write(X;A),fail.

2;[r, d, d, d, d]
3;[d, r, d, d, d]
5;[d, d, r, d, d]
6;[r, d, r, d, d]
9;[d, d, d, r, d]
11;[d, r, d, r, d]
17;[d, d, d, d, r]
18;[r, d, d, d, r]
21;[d, d, r, d, r]
22;[r, d, r, d, r]

No
?-

?- A=[4, 7, 8, 10, 12, 13, 14, 15, 16, 19, 20, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32],
find_non_trivial_CKR(N,[1|A],B).

A = [4, 7, 8, 10, 12, 13, 14, 15, 16|...]
N = 22
B = 1, [[down], [down], [down], [down], [down]] ;

No
?-

% The inductive choice is necessary for CKI: [1] must be included.

?- A=[4, 7, 8, 10, 12, 13, 14, 15, 16, 19, 20, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32],
find_non_trivial_CKR(N,A,B).

No

% the above event is the maximal CKI.

?- A=[4, 7, 8, 10, 12, 13, 14, 15, 16, 19, 20, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32],
strategy_profile_0(W,_,_),\+ member(W,A),append(A,[W],A1),sort(A1,A2),
find_non_trivial_CKR(N,A2,B).

A = [4, 7, 8, 10, 12, 13, 14, 15, 16|...]
W = 1
A1 = [4, 7, 8, 10, 12, 13, 14, 15, 16|...]
A2 = [1, 4, 7, 8, 10, 12, 13, 14, 15|...]
N = 22
B = 1, [[down], [down], [down], [down], [down]] ;

No
?- 

% the CKR event.

?- is_rational(R,Hx,D),nl,write(R).

[1, 4, 7, 8, 10, 12, 13, 14, 15, 16]

R = [1, 4, 7, 8, 10, 12, 13, 14, 15|...]
Hx = '3ff000'
D = [[down, right], [down, right], [down, right], [down, right], [down]] ;

No
?- R=[1, 4, 7, 8, 10, 12, 13, 14, 15, 16],
    common_knowledge(CKR,on(R),S).

R = [1, 4, 7, 8, 10, 12, 13, 14, 15|...]
CKR = [1]
S = 10, [[down, right], [down, right], [down, right], [down, right], [down]] ;

No
?- 

% Thus, in the above event, w.r.t. a nomadic knowledge system,
% the players do inductive choice
% nevertheless they have no deductive ability of 
% backward induction. 
% So, I think that it make sense of a reason why Aumann said
% `substantively rational'.


*************************************************/




%---------------------------------------------------%
% common programs
%---------------------------------------------------%

% intersection of list
%---------------------------------------------------%
% 6 Feb 2005.

intersection_of_lists([],_).
intersection_of_lists([X|H],Z):-
   intersection_of_lists(H,Y),
   intersection(X,Y,Z).

% hexa and bits (intended for abbreviation of event)
%---------------------------------------------------%
% 5-6 Feb 2005.

hexa_list(X,N,[Tx|Hx]):-
   \+ var(X),
   length(X,N),
   R is N mod 4,
   hexa_list_residual(R,X,Y,Tx),
   hexa_list_0(Y,Hx).

hexa_list_0([],[]).
hexa_list_0([A,B,C,D|X],[Hx|Y]):-
   hexa_list_0(X,Y),
   hexa_1([A,B,C,D],Hx).

hexa_list_residual(0,[A,B,C,D|X],X,Hx):-
   hexa_1([A,B,C,D],Hx).
hexa_list_residual(3,[A,B,C|X],X,Hx):-
   hexa_1([0,A,B,C],Hx).
hexa_list_residual(2,[A,B|X],X,Hx):-
   hexa_1([0,0,A,B],Hx).
hexa_list_residual(1,[A|X],X,Hx):-
   hexa_1([0,0,0,A],Hx).


hexa_1(FourBits,Hx):-
   list_projection(FourBits,[a,b,c,d],_),
   bits(FourBits,Decimal,_B),
   hexa_pattern(Hx,Decimal).

hexa_pattern(Hx,Hx):-
   Hx <10,
   !.

hexa_pattern(Hx,D):-
   member((D,Hx),[
     (10,a),(11,b),(12,c),(13,d),(14,e),(15,f)
   ]).

hexa(L,Decimal,Hx):-
   concat_list(Hx,[0,x|L]),
   atom_chars(Hx,Atoms),
   number_chars(Decimal,Atoms).

bits(L,Decimal,B):-
   concat_list(B,[0,b|L]),
   atom_chars(B,Atoms),
   number_chars(Decimal,Atoms).

% concat list
%---------------------------------------------------%
% cited and modified from moji.pl(July 2003)

concat_list(A,[A]).
concat_list(Z,[L|R]):- 
   concat_list(Q,R),
   concat(L,Q,Z).


/*
% ISO definition: 0[box].
% binary, octal hexadecimal numbers.

?- A is 0x101.

A = 257 

Yes
?- 

% system predicates

?- atom_chars(123,A),number_chars(B,A).

A = ['1', '2', '3']
B = 123 

Yes
?- number_chars(B,['0','x','1','1']).

B = 17 

Yes
?-
*/

%---------------------------------------------------%
% 28 Jan 2005.

forall_write(A):- forall(member(X,A),(nl,write(X))).
forall_write_goals(A,B):- B,nl,write(A),fail.
forall_write_goals(_,_):- nl,write(complete).

inductive_numbers([]).
inductive_numbers([N|H]):-
   length(H,N),
   inductive_numbers(H).

make_pairs([],[],[]).
make_pairs([A-X|Z],[A|B],[X|Y]):-
   length(B,N),
   length(Y,N),
   length(Z,N),
   make_pairs(Z,B,Y).

% super set projection 
%---------------------------------------------------%
% 1 Feb 2005.

sup_projection([],[]).
sup_projection([W|Z],[X|Y]):-
   member((X,W),[(1,1),(0,0),(0,1)]),
   sup_projection(Z,Y).


% a naive program of distribution (index function). 
% this is not useful for generate a long list.
%---------------------------------------------------%

project_N_things_of(N,O,P,Q):-
   integer(N),
   length(O,U),
   N==N)
    ->!,true
    ; (
      inductive_numbers([U|M]),
      member(N,[U|M])
   )),
   length(P,U),
   choose_N_units_0(P,N,_L).


% validation of bit sequence

is_a_bounded_bit_sequence_of_length(P,L):- 
   length(P,L),
   forall(member(X,P),
    (
     \+ var(X),
     member(X,[0,1])
    )
   ).

/*************************************************

?- choose_N_units_among(5000,2,[1,1|X]).

X = [0, 0, 0, 0, 0, 0, 0, 0, 0|...] 

Yes

*************************************************/


% generation of bit sequence

choose_N_units_0([],0,0).
choose_N_units_0(Z,0,0):-
   length(Z,R),
   zeros(Z,R).
choose_N_units_0(Z,M,L):-
   length(Z,R),
   M>=R,
   ones(Z,R),
   L is M -R.
choose_N_units_0([X|Y],M,L1):-
   length([X|Y],R),
   M >0,
   M U=0;integer(U)),
   inductive_numbers([U|M]),
   !,
   reverse([U|M],[0|R]),
   list_projection(P,R,W).
   

/*************************************************

?- assign_values(A,[0,1,2],4,(sum(A,N),N = 5)).

A = [2, 2, 1, 0]
N = 5 ;

A = [2, 1, 2, 0]
N = 5 ;

A = [1, 2, 2, 0]
N = 5 ;

...

?- replace_sublist_with_values(A,[x],true,[a,b,c,d,e],[1,3,4]).

A = [x, b, x, x, e] ;

No
?- replace_sublist_with_values(A,[x,y],true,[a,b,c,d,e],[1,3,4]).

A = [x, b, x, x, e] ;

A = [y, b, x, x, e] ;

A = [x, b, y, x, e] ;

A = [y, b, y, x, e] ;

A = [x, b, x, y, e] ;

A = [y, b, x, y, e] ;

A = [x, b, y, y, e] ;

A = [y, b, y, y, e] ;

No
?- subsequence_of_inductive_numbers(2,P,R,W).

P = [0, 0]
R = [1, 2]
W = [] ;

P = [0, 1]
R = [1, 2]
W = [2] ;

P = [1, 0]
R = [1, 2]
W = [1] ;

P = [1, 1]
R = [1, 2]
W = [1, 2] ;

No
?- 

*************************************************/


% priority-considered version of bag0
%---------------------------------------------------%

variation_seek_sequence([],_A,0).
variation_seek_sequence([C|B],A,N):-
   length([C|B],N),
   member(C,A),
   subtract(A,[C],D),
   append(D,[C],E),
   variation_seek_sequence(B,E,_N1).

:- dynamic temp_vss/1.

update_temp_vss(C):-
   retract(temp_vss(H)),
   assert(temp_vss([C|H])).



% cited from set.pl  
%---------------------------------------------------%

bag0([],_A,0).
bag0([C|B],A,N):-
   length([C|B],N),
   bag0(B,A,_N1),
   member(C,A).
zeros(Zero,N):-bag0(Zero,[0],N).
ones(One,N):-bag0(One,[1],N).

subset_of(A,N,As):-
   length(As,L),
   length(D,L),
   list_projection(D,As,B),
   length(B,N),
   sort(B,A).

list_projection([],[],[]).
list_projection([X|Y],[_A|B],C):-
   X = 0,
   list_projection(Y,B,C).
list_projection([X|Y],[A|B],[A|C]):-
   X = 1,
   list_projection(Y,B,C).

c_list_projection([],[],[]).
c_list_projection([X|Y],[_A|B],C):-
   X = 1,
   c_list_projection(Y,B,C).
c_list_projection([X|Y],[A|B],[A|C]):-
   X = 0,
   c_list_projection(Y,B,C).

allocation(N,A,[X|Y]):-
    allocation(N,A,A,[X|Y]).
allocation(0,_,0,[]).
allocation(N,A,B,[X|Y]):-
    integer(A),
    length([X|Y],N),
    allocation(_N1,A,B1,Y),
    K is A - B1 + 1,
    length(L,K),
    nth0(X,L,X),
    B is B1 + X.


% cited from math1.pl
%---------------------------------------------------%

sum([],0).
sum([X|Members],Sum):-
   sum(Members,Sum1),
  %number(X),
   Sum is Sum1 + X.

product([],1).
product([X|Members],Z):-
   product(Members,Z1),
  %number(X),
   Z is Z1 * X.

product_sum([],[],[],0).
product_sum([P|Q],[A|B],[E|F],V):-
    length(Q,N),
    length(B,N),
    product_sum(Q,B,F,V1),
    E is P * A,
    V is V1 + E.




%   Utilities for file output and display
%---------------------------------------------------%
% cited from : menu.pl

tell_goal(File,G):-
   (current_stream(File,write,S0)->close(S0);true),
   open(File,write,S),
   tell(File),
   nl,
   tstamp('% file output start time ',_),
   nl,
   write('%----------  start from here ------------%'),
   nl,
   G,
   nl,
   write('%----------  end of data ------------%'),
   nl,
   tstamp('% file output end time ',_),
   tell(user),
   close(S),
   % The following is to cope with the duplicated stream problem.
   (current_stream(File,write,S1)->close(S1);true).

% save all successful goals to file.
%--------------------------------

tell_goal(File,forall,G):-
   G0 = (nl,write(G),write('.')),
   G1 = forall(G,G0),
   tell_goal(File,G1).

% the conditionalized version
% Aug 2003.

tell_goal(File,forall_such_that,G,Condition):-
   % G should be occurred in the Condition.
   WRITE = (nl,write(G),write('.')),
   G1 = forall(Condition,WRITE),
   tell_goal(File,G1).


% time stamp
%--------------------------------

tstamp(no,T):-
   get_time(U),
   convert_time(U,A,B,C,D,E,F,_G),
   T = [date(A/B/C), time(D:E:F)],
   nl.

tstamp(Word,T):-
   \+ var(Word),
   Word \= no,
   get_time(U),
   convert_time(U,A,B,C,D,E,F,_G),
   T = [date(A/B/C), time(D:E:F)],
%   format('~`.t~t~a~30|~`.t~t~70|~n',[Word]),
   write((Word,T)),
   nl.

% measuring time consumption 
%--------------------------------

stopwatch_0(Goal,TD):-
   get_time(TS),
   Goal,
   get_time(TF),
   TD is TF - TS.

stopwatch(Goal,TD):-
   stopwatch_0(Goal,TD),   
   nl,
   write('% time elapsed (sec): '),
   write(TD),
   nl.

%---------------------------------------------------%
%   Testing tools
%---------------------------------------------------%
% cited from: kalp01.pl (Jan 2004)

% Display
%--------------------------------

% display all successful goals (with the count).
display_goals(G):-
   (\+ var(G)->true;G=empty),
   forall(G,(nl,write(G))).
display_goals(_).
display_goals(G,C):-
   (\+ var(G)->true;G=empty),
   (\+ var(C)->true;C=true),
   forall((G,C),(nl,write(G))).
display_goals(_,_).
display_goals(G,C,N):-
   (\+ var(G)->true;G=empty),
   (\+ var(C)->true;C=true),
   findall(G,(G,C),L),
   length(L,N),
   display_goals(G,member(G,L)),
   nl,
   write('the number of goals='),
   write(N).


% Equivalence
%--------------------------------

verify_equality_of_goals(G1:V1,G2:V2,S,D):-
   findall(V1,G1,S1),
   findall(V2,G2,S2),
   subtract(S1,S2,D1),
   subtract(S2,S1,D2),
   S=[S1,S2],D=[D1,D2].


% a script for generating goals as facts
%---------------------------------------------------%
% a generalized version of factualize_strategies/0.
% 31 Jan 2005.

:- dynamic id_of_temp_goal/1.
:- dynamic temp_goal/3.

update_id_of_temp_goal(ID):-
   retract(id_of_temp_goal(ID_0)),
   ID is ID_0 +1,
   assert(id_of_temp_goal(ID)).

preliminary_to_factualize_goals:-
   abolish(id_of_temp_goal/1),
   abolish(temp_goal/3),
   assert(id_of_temp_goal(0)).

factualize_goals(G):-
   warn_if_not_a_list(G),
   preliminary_to_factualize_goals,
   factualize_goals(G,LID),
   finalize_factualization(LID).

factualize_goals([Goal|Constraint],ID):-
   Goal,
   Constraint,
   update_id_of_temp_goal(ID),
   assert(temp_goal(ID,Goal,Constraint)),
   fail.

factualize_goals(_,ID):-
   id_of_temp_goal(ID).

finalize_factualization(Last_ID):-
   write(complete),
   nl,
   write(total:Last_ID),
   write(' successful goals have asserted as temp_goal/3.').

warn_if_not_a_list(G):-
   length(G,_),
   forall(member(X,G),clause(X,_)),
   !.

warn_if_not_a_list(_):-
   write('**** warning : not a list of executable goals.'),
   nl,
   write('no data has generated.'),
   fail.


:- initialize_program.

% end of program
%---------------------------------------------------%

return to front page.