You selected kalp01.pl
headline([''
, '------------------------------------------------------'
, ' Epistemic modeling of decision maker : '
, ' Knowlege-and-Awareness Logic on Prolog (KALP01) '
, '------------------------------------------------------'
, ' for SWI-Prolog version 5.0.10'
]).
author([' author: Kenryo INDO (Kanto Gakuen University) '
, ' Ota-si, Gunma-ken, 373-8515 Japan.'
]).
model_predicates([' Models:'
, ' state/1, event/1, possibility/3: state space and belief operators.'
, ' primitive_act/3, act/3, preference/3,strict_preference/3: acts, preferences.'
, ' savage_null/3, belief_via_preference/3, possibility_via_preference/3: Savagian beliefs.'
, ' auto_primitive_acts/0 :(->escape_1/3) generating acts given preferences.'
, ' lemma_2/0: (->escape_3/3) properties of possibility relations and axioms of beliefs.'
, ' does_not_know/3, be_unaware_of/4, be_unaware_of_degree/5: unawareness operators.'
, ' generate_and_test_of_unawareness: (->escape_4/3).'
, ' create_belief_of_0/2, cautious_generation_of_belief_of_0/3: (->escape_2/3).'
]).
history(long,['% file: epilog01.pl'
, ' created: 20-22 Dec 2004. possibility and belief operators.(epilog0)'
, ' revised: 26-29 Dec 2004. preferences and acts. scripts which generate and verify Savagian beliefs.'
, ' revised: 30-31 Dec 2004. scripts which generate and verify possible relations and lemma 2.'
, ' revised: 1 Jan 2005. nontriviality, extended sympathy, strong monotonicity.'
, ' revised: 1 Jan 2005. decision problem, and coherency.(prolonged)'
, ' revised: 2-8 Jan 2005. unawareness operator.(file renamed: epilog0-->kalp01)'
, ' revised: 9-10 Jan 2005. generate and test for belief operators and theorem 1.'
, ' revised: 10 Jan 2005. a non-standard unawareness, DLR98 example 2.'
, ' revised: 11 Jan 2005. the modeling of acts revised.'
, ' revised: 12-14,17 Jan 2005. debug the models of unawareness and so on.'
, ' revised: 21 Jan 2005. debug the axiom of unawareness (npk).'
, ' snowfall: 29, 31 Dec at Ota.'
]).
history(short,[' file: epilog01.pl (20 Dec 2004-- 21 Jan 2005) ']).
references(short,[' References:'
, ' [1] Morris, S.(1996) The logic of belief change: a decision theoretic approach.'
, ' Journal of Economic Theory 69: 1-23.'
, ' [2] Dekel, E., B. L. Lipman, and A. Rustichini. Standard state-space models '
, ' preclude unawareness. Econometrica 66(1): 159-173(1998).'
]).
references(long,[' References:'
, ' [1] Morris, S.(1996) The logic of belief change: a decision theoretic approach.'
, ' Journal of Economic Theory 69: 1-23.'
, ' [2] Morris, S.(1997) Alternative definitions of knowledge. In M.O.L. Bacharach et al.(eds.), '
, ' Epistemic Logic and the Theory of Games and Decisions, pp.217-233. Kluwer A.P.'
, ' [3] Modica, S., and A. Rustichini(1994). Awareness and partitional information structures. '
, ' Theory and Decisions 37: 107-124.'
, ' [4] Dekel, E., B. L. Lipman, and A. Rustichini. Standard state-space models '
, ' preclude unawareness. Econometrica 66(1): 159-173(1998).'
, ' [5] Modica, S., and A. Rustichini(1999). unawareness and partitional information structures. '
, ' Games and Economic Behavior 27: 265-298.'
, ' [7] Halpern, J.(2001). Alternative semantics for unawareness. '
, ' Games and Economic Behavior 37: 321-339.'
]).
%--------------------------------
% Display of headers
%--------------------------------
display_all_lines(A):-
\+ var(A),
forall(member(B,A),(nl,write('%'),write(B))).
:- headline(H),
references(short,R),
history(short,D),
%model_predicates(P),
author(A),
forall(member(C,[H,D,A,R]),(display_all_lines(C))),
nl.
% forall/2.
% forall(A,B):- \+((A,\+B)).
:- display_all_lines( [
' ********** loading model predicates and scripts *********** ',
' state/1, event/1, possibility/3: state space and knowledge operators with the axioms.'
]).
/**********************************************************/
/* modeling beliefs of agent */
/**********************************************************/
% 20-22 Dec 2004.
% ------------------------------------------------- %
% state, agent, event, information (possibility),
% and possibility correspondences
% ------------------------------------------------- %
agent(J):- all_agents(Is),member(J,Is).
state(S):- all_states(Ss),member(S,Ss).
event(E):- all_states(O), subset_of(E,_N,O).
event_pair(E,F):- event(E), event(F), E @=< F.
complement(E,C):- all_states(S),event(E),subtract(S,E,C).
% example 1-5 in Morris(1994).
% ------------------------------------------------- %
all_agents([1,2,3,4,5]).
all_states([a,b,c]).
:- dynamic possibility/3.
possibility(1,a,[a,b]).
possibility(1,b,[b]).
possibility(1,c,[b,c]).
possibility(3,a,[a,b]).
possibility(3,b,[b]).
possibility(3,c,[b,c]).
possibility(J,a,[a,b]):-member(J,[2,5]).
possibility(J,b,[b]):-member(J,[2,5]).
possibility(J,c,[a,c]):-member(J,[2,5]).
%possibility(4,a,[a,b,c]).
%possibility(4,b,[a,b,c]).
%possibility(4,c,[a,b,c]).
% ------------------------------------------------- %
% belief operator B : 2^S -> 2^S
% given possiblility correspondence,
% i.e., (non-)partitional information structure
% ------------------------------------------------- %
% definition:
% Agent believes event E at state w iff w in B(E).
%
% Note: In the later part of this program, generation and test of
% belief operators with three states and their relation to the
% possibility correspondences (in accordance with Lemma 2 of
% Morris(1996)) are verified.
is_believed_at(State,Agent,Event):-
event(Event),
possibility(Agent,State,Partition),
subset(Partition,Event).
belief_of_1(Agent,Event,Belief):-
agent(Agent),
event(Event),
findall(
State,
is_believed_at(State,Agent,Event),
Bag
),
sort(Bag,Belief).
% utilize belief_of_0/3
% after execution of make_beliefs_table/0.
%---------------------------------------------------
% revised: 8 Jan 2005 clause/2 is added for the belief_of_0s.
belief_of(Agent,Event,Belief):-
agent(Agent),
\+ clause(belief_of_0(_Id,Agent,_,_),true),
\+ clause(belief_of_0(Agent,_,_),true),
belief_of_1(Agent,Event,Belief).
belief_of(Agent,Event,Belief):-
clause(belief_of_0(Agent,Event,Belief),_).
belief_of(Agent,Event,Belief):-
clause(belief_of_0(_,Agent,Event,Belief),_).
% ------------------------------------------------- %
% axioms for normal beliefs: B1 & B2
% ------------------------------------------------- %
% logically omniscient agent
% distribution, or conjunction, which implies monotonicity
axiom_B1(distribution,A,X):-
agent(A),
findall((E,F,MB,BM),
(
belief_of(A,E,BE),
belief_of(A,F,BF),
intersection(E,F,M),
belief_of(A,M,BM),
intersection(BE,BF,MB),
MB\=BM
),
Y),
(Y\=[]->X=violation(Y);X=hold).
% totology, or necessiation.
axiom_B2(totology,Agent,X):-
all_states(S),
belief_of(Agent,S,BS),
(BS \= S ->X=violation;X=hold).
% monotonicity
axiom_BM(monotonicity,J,X):-
agent(J),
findall((E,F,BE,BF),
(
event(E),event(F),subset(E,F),
belief_of(J,E,BE),belief_of(J,F,BF),
\+ subset(BE,BF)
),
Y),
(Y\=[]->X=violation(Y);X=hold).
% inconsistency.
axiom_BI(inconsistency,Agent,X):-
agent(Agent),
(belief_of(Agent,[],[])->X=hold;X=false).
/***************** demo ********************************
?- axiom_B1(A,J,B).
A = distribution
J = 1
B = hold ;
A = distribution
J = 2
B = hold ;
No
% alternatively, verifying these axioms directly.
% axiom B2 (distribution)
?- P= (event(E),event(F),intersection(E,F,M),is_believed_at(W,1,M)),
Q= (is_believed_at(W,1,E),is_believed_at(W,1,F)),
forall(P,Q),
forall(Q,P).
P = event(_G157), event(_G159), intersection(_G157, _G159, _G163), is_believed_at(_G165, 1, _G163)
E = _G157
F = _G159
M = _G163
W = _G165
Q = is_believed_at(_G165, 1, _G157), is_believed_at(_G165, 1, _G159)
Yes
?-
% monotonicity (axiom B2)
?- forall((event(E),event(F),subset(E,F)),
(
belief_of(J,E,BE),belief_of(J,F,BF),
subset(BE,BF)
)).
Yes
******************** end *****************************/
% display beliefs
% ------------------------------------------------- %
skim_distribution([A,E,F,MB,BM]):-
B=check_distribution(A,E,F,MB,BM),
display_goals(B).
skim_beliefs([A,E,C]):-
write('mode: belief_'),
(clause(belief_of_0(_,_,_,_),_)->write(0);write(1)),
nl,
B=belief_of(A,E,C),
display_goals(B).
/***************** demo ********************************
?- skim_beliefs([1,_,_]).
mode: belief_1
belief_of(1, [], [])
belief_of(1, [s5], [])
belief_of(1, [s4], [])
belief_of(1, [s4, s5], [s4, s5])
belief_of(1, [s3], [])
belief_of(1, [s3, s5], [])
belief_of(1, [s3, s4], [])
belief_of(1, [s3, s4, s5], [s4, s5])
belief_of(1, [s2], [])
belief_of(1, [s2, s5], [])
belief_of(1, [s2, s4], [])
belief_of(1, [s2, s4, s5], [s4, s5])
belief_of(1, [s2, s3], [s2, s3])
belief_of(1, [s2, s3, s5], [s2, s3])
belief_of(1, [s2, s3, s4], [s2, s3])
belief_of(1, [s2, s3, s4, s5], [s2, s3, s4, s5])
belief_of(1, [s1], [s1])
belief_of(1, [s1, s5], [s1])
belief_of(1, [s1, s4], [s1])
belief_of(1, [s1, s4, s5], [s1, s4, s5])
belief_of(1, [s1, s3], [s1])
belief_of(1, [s1, s3, s5], [s1])
belief_of(1, [s1, s3, s4], [s1])
belief_of(1, [s1, s3, s4, s5], [s1, s4, s5])
belief_of(1, [s1, s2], [s1])
belief_of(1, [s1, s2, s5], [s1])
belief_of(1, [s1, s2, s4], [s1])
belief_of(1, [s1, s2, s4, s5], [s1, s4, s5])
belief_of(1, [s1, s2, s3], [s1, s2, s3])
belief_of(1, [s1, s2, s3, s5], [s1, s2, s3])
belief_of(1, [s1, s2, s3, s4], [s1, s2, s3])
belief_of(1, [s1, s2, s3, s4, s5], [s1, s2, s3, s4, s5])
No
?-
******************** end *****************************/
% possiblity thinking operator.
% ------------------------------------------------- %
think_possible_at(State,Agent,Event):-
event(Event),
possibility(Agent,State,Partition),
intersection(Partition,Event,M),
M \= [].
think_possible_of(Agent,Event,Belief):-
setof(
State,
think_possible_at(State,Agent,Event),
Belief
).
% another equivalent modeling cited from trade.pl
% ------------------------------------------------- %
know_event_when(J,E,K):-
agent(J),
event(E),
setof(S,
H^(
possibility(J,S,H),
subset(H,E)
),
K).
think_possible_when(J,E,P):-
agent(J),
event(E),
setof(S,
H^(
possibility(J,S,H),
intersection(H,E,M),
M\=[]
),
P).
% ------------------------------------------------- %
% possiblility correspondence reproduced by beliefs
% ------------------------------------------------- %
% Theorem 1:
% B1 & B2 iff B represents P (i.e.,noramal belief)
% The if part is prooved when P(w)={c:w is not in B(S-[c])}.
a_possibility(at(W),agent(J),think(C),complement_B(BCC)):-
%agent(J),
state(W),
%state(C),
complement([C],CC),
belief_of(J,CC,BCC),
\+ member(W,BCC).
% revised: 7 Jan 2004. a forgotten exsistence quantifier.
% revised: 9 Jan 2004. recovery of empty cases.
possibility_1(at(W),agent(J),think(P)):-
agent(J),
state(W),
findall(C,
a_possibility(at(W),agent(J),think(C),_),
P0),
sort(P0,P).
/***************** demo ********************************
?- Q=(possibility_1(at(W),agent(J),think(C)),possibility(J,W,P)),
display_goals(Q).
possibility_1(at(a), agent(1), think([a, b])), possibility(1, a, [a, b])
possibility_1(at(b), agent(1), think([b])), possibility(1, b, [b])
possibility_1(at(c), agent(1), think([b, c])), possibility(1, c, [b, c])
possibility_1(at(a), agent(2), think([a, b])), possibility(2, a, [a, b])
possibility_1(at(b), agent(2), think([b])), possibility(2, b, [b])
possibility_1(at(c), agent(2), think([a, c])), possibility(2, c, [a, c])
possibility_1(at(a), agent(3), think([a, b])), possibility(3, a, [a, b])
possibility_1(at(b), agent(3), think([b])), possibility(3, b, [b])
possibility_1(at(c), agent(3), think([b, c])), possibility(3, c, [b, c])
possibility_1(at(a), agent(5), think([a, b])), possibility(5, a, [a, b])
possibility_1(at(b), agent(5), think([b])), possibility(5, b, [b])
possibility_1(at(c), agent(5), think([a, c])), possibility(5, c, [a, c])
Q = possibility_1(at(_G157), agent(_G159), think(_G161)), possibility(_G159, _G157, _G169)
W = _G157
J = _G159
C = _G161
P = _G169
Yes
?-
******************** end *****************************/
% ------------------------------------------------- %
% a factualization: generating beliefs as facts
% ------------------------------------------------- %
% make_beliefs_table/0
%%%%%%% %%%%%%%
%%%% script %%%%%
%%%%% %%%%%%
%%%%%%% %%%%%%%%
%%%%%%%% %%%%%%%%%
%%%%%%% %%%%%%%%
:- dynamic belief_of_0/4.
:- dynamic last_id/1.
init_beliefs_table:-
abolish(last_id/1),
abolish(belief_of_0/4).
update_id(1):-
\+ clause(last_id(_),_),
assert(last_id(1)).
update_id(Id):-
last_id(Id0),
Id is Id0+1,
retractall(last_id(Id0)),
assert(last_id(Id)).
make_beliefs_table:-
init_beliefs_table,
fail.
make_beliefs_table:-
belief_of_1(A,E,B), % to prevent doubling data
update_id(Id),
assert(belief_of_0(Id,A,E,B)),
fail.
make_beliefs_table.
:- display_all_lines( [
' primitive_act/3, act/3, act_1/3, preference/3,strict_preference/3: acts, preferences, axioms, etc.'
]).
/**********************************************************/
/* modeling acts and preferences of agent */
/**********************************************************/
% 26-28 Dec 2004.
% revised : 11 Jan 2005.
% ------------------------------------------------- %
% consequences and acts
% ------------------------------------------------- %
% basic part of the Savage framework
% states: a finite set. --- see belief section.
% consequences: a finite set of real numbers.
consequences([0,1,2]).
% acts: the set of functions act:states->consequences.
% act_1/1,2,3, generate_act_1/3:
% the complete set of acts generated as functions of states into consequences.
generate_act_1([E|B],[E->C|D],[C|H]):-
(var(B)->(all_states(S),[E|B]=S);true),
generate_act_1(B,D,H),
consequences(X),
member(C,X).
generate_act_1([],[],[]).
act_1(Map,Values):-
all_states(S),
generate_act_1(S,Map,Values).
act_1(X,S,V):-
act_1(Map,X),
member((S->V),Map).
act_1(X):- act_1(_,X).
% act/1,3:
% the synonyms of special acts and their compositions defined over event partition.
act(X):- all_primitive_acts(A),member(X,A).
act(X):- composite_act(X).
act(X):- act_1(X).
% act(Act, State, Number)
% an act defines prizes over states
act(X,S,V):-
act_1(X,S,V).
act(X,S,V):-
primitive_act(X,S,V).
act(HX,S,V):-
composite_act(K,HX,_Part),
K >0,
member((H->X),HX),
member(S,H),
primitive_act(X, S, V).
constant_act(F,S,V):-
setof(R,S^act(F,S,R),[V]),
act(F,S,R).
% eventwise binary choice.
%--------------------------------------------------------------
eventwise_binary_act(Act, Event->X; Y):-
act(Act),
complement(Event,Complement),
member((Event->X),Act),
member((Complement->Y),Act).
/***************** demo ********************************
?- eventwise_binary_act(Act1, [W]->X; Z).
Act1 = [ ([a]->y), ([b, c]->x)]
W = a
X = y
Z = x
Yes
******************** end *****************************/
% primitive acts
% ------------------------------------------------- %
all_primitive_acts([x,y,z]).
:- dynamic primitive_act/3.
% an example:
% alternative definition of three constant act symbols x, y, z.
primitive_act(x, a, 1).
primitive_act(x, b, 1).
primitive_act(x, c, 1).
primitive_act(y, a, 0).
primitive_act(y, b, 0).
primitive_act(y, c, 0).
primitive_act(z, a, 2).
primitive_act(z, b, 2).
primitive_act(z, c, 2).
% composite act
% ------------------------------------------------- %
% composite act state-by-state.
composite_act_1([],[],[]).
composite_act_1([X|Y],[S|H],[V|U]):-
composite_act_1(Y,H,U),
primitive_act(X,S,V).
composite_act_2(X,O,Z):-
all_states(O),
composite_act_1(X,O,Z).
% composite act defined over possibility.
composite_act_3(0,[],[]).
composite_act_3(K,[H->X|Acts],Part):-
(var(Part)->partitioning_of_states(Part,_O);true),
Part=[H|Part1],
composite_act_3(K1,Acts,Part1),
all_primitive_acts(A),
member(X,A),
\+ member((_->X),Acts),
K is K1 + 1.
composite_act(K,A,P):-
clause(composite_act_0(_,K,A,P),_).
composite_act(K,A,P):-
\+ clause(composite_act_0(_,_,_,_),_),
composite_act_3(K,A,P).
composite_act(X):- composite_act(K,X,_Part), K>0.
% makeing partitions
% ------------------------------------------------- %
partitioning_of_states([],[]).
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).
/***************** demo ********************************
?- partitioning_of_states(A,B), B\=[].
A = [[a], [b], [c]]
B = [a, b, c] ;
A = [[a], [b, c]]
B = [a, b, c] ;
A = [[a, c], [b]]
B = [a, b, c] ;
A = [[a, b], [c]]
B = [a, b, c] ;
A = [[a, b, c]]
B = [a, b, c] ;
No
?-
******************** end *****************************/
:- dynamic preference/4.
:- dynamic preference_0/4.
% preference(Agent,State,X,Y)
% an example of preference relations with incomparable pair.
% ------------------------------------------------- %
% It can be completed by using auto_completion/0 below.
preference(1,a,x,y).
preference(1,a,y,z).
preference(1,a,z,x).
preference(1,b,x,y).
preference(1,b,y,z).
preference(1,b,x,z).
preference(1,c,x,y).
preference(1,c,y,z).
preference(1,c,x,z).
% a state-dependent preferences (full information at the state).
% ------------------------------------------------- %
preference(full,S,X,Y):- % who know the true state.
state(S),
act(X, S, V1),
act(Y, S, V2),
V1 >= V2.
% example 3 (Morris, 1994)
% ------------------------------------------------- %
% a risk neutral preference which confirms
% possibility relations in example 1,
% P(a)=[a,b],P(b)=[b],P(c)=[b,c].
preference(3,a,X,Y):-
act(X,a,Xa),
act(Y,a,Ya),
act(X,b,Xb),
act(Y,b,Yb),
Vx is 0.5*Xa +0.5*Xb, % P(a)={a,b}, where a and b are equiprobable.
Vy is 0.5*Ya +0.5*Yb,
Vx >= Vy.
preference(3,b,X,Y):-
act(X,b,Xb),
act(Y,b,Yb),
Xb >=Yb.
preference(3,c,X,Y):-
act(X,c,Xc),
act(Y,c,Yc),
act(X,b,Xb),
act(Y,b,Yb),
Vx is 0.5*Xb +0.5*Xc,
Vy is 0.5*Yb +0.5*Yc,
Vx >=Vy.
% strict-preferences and indifference
strict_preference(J,W,X,Y):-
state(W),
act(X),
act(Y),
agent(J),
preference(J,W,X,Y),
\+ preference(J,W,Y,X).
indifference(J,W,X,Y):-
state(W),
act(X),
act(Y),
agent(J),
preference(J,W,X,Y),
preference(J,W,Y,X).
% ------------------------------------------------- %
% preference on events :
% ------------------------------------------------- %
% preference_on_event(Agent,Event,X,Y)
preference_on_event(J,E,X,Y):-
clause(preference_on_event_1(_,J,E,X,Y),_).
preference_on_event(J,E,X,Y):-
\+ clause(preference_on_event_1(_,_,_,_,_),_),
preference_on_event_1(J,E,X,Y).
preference_on_event_1(J,E,X,Y):-
agent(J),
event(E),
E \= [],
act(X),
act(Y),
\+ (
state(S),
\+ preference(J,S,X,Y)
).
strict_preference_on_event(J,E,X,Y):-
preference_on_event(J,E,X,Y),
state(S),
strict_preference(J,S,X,Y).
indifference_on_event(J,E,X,Y):-
preference_on_event(J,E,X,Y),
preference_on_event(J,E,Y,X).
% ------------------------------------------------- %
% the factualization of composite acts
% ------------------------------------------------- %
% make_acts_table/0
:- dynamic composite_act_0/4.
%:- dynamic last_id/1.
init_acts_table:-
abolish(last_id/1),
abolish(composite_act_0/4).
% update_id(Id) has defined above.
make_acts_table:-
init_acts_table,
fail.
make_acts_table:-
composite_act_3(K,A,P),
update_id(Id),
assert(composite_act_0(Id,K,A,P)),
fail.
make_acts_table.
% ------------------------------------------------- %
% the factualization of event base preferences
% ------------------------------------------------- %
% make_preferences_table/0
%%%%%%% %%%%%%%
%%%% script %%%%%
%%%%% %%%%%%
%%%%%%% %%%%%%%%
%%%%%%%% %%%%%%%%%
%%%%%%% %%%%%%%%
:- dynamic preference_on_event_0/5.
:- dynamic strict_preference_on_event_0/5.
:- dynamic indifference_on_event_0/5.
%:- dynamic last_id/1.
init_preference_table:-
abolish(last_id/1),
abolish(preference_on_event_0/5),
abolish(strict_preference_on_event_0/5),
abolish(indifference_on_event_0/5).
% update_id(Id) has defined above.
make_preference_table:-
init_preference_table,
fail.
make_preference_table:-
preference_on_event_1(J,E,X,Y),
update_id(Id),
assert(preference_on_event_0(Id,J,E,X,Y)),
fail.
make_preference_table:-
abolish(last_id/1),
strict_preference_on_event(J,E,X,Y),
update_id(Id),
assert(strict_preference_on_event_0(Id,J,E,X,Y)),
fail.
make_preference_table:-
abolish(last_id/1),
indifference_on_event(J,E,X,Y),
update_id(Id),
assert(indifference_on_event_0(Id,J,E,X,Y)),
fail.
make_preference_table.
% list factualized preferences
% ------------------------------------------------- %
list_preferences:-
list_preferences(all).
list_preferences(A):-
((member(w,A);A=all)->listing(preference_on_event_0/5);true),
((member(s,A);A=all)->listing(strict_preference_on_event_0/5);true),
((member(i,A);A=all)->listing(indifference_on_event_0/5);true).
/***************** demo ********************************
% a test run for factualization of preferences.
?- findall(L,(setof((X,Y,Z),
preference_on_event_0(_,J,X,Y,Z),D),length(D,L)),F),sort(F,P).
F = [1, 1, 1, 1, 1, 1, 1, 1, 1|...]
P = [1]
Yes
?-
******************** end *****************************/
% ------------------------------------------------- %
% axioms for preference relations: P1 & P2
% ------------------------------------------------- %
axiom_P1(completeness,(J,W),R):-
agent(J),
state(W),
findall([X,Y],
(
act_1(X),
act_1(Y),
\+ preference(J,W,X,Y),
\+ preference(J,W,Y,X)
),
Y),
(Y\=[]->R=violation(Y);R=true).
/*
axiom_P1(completeness,J):-
agent(J),
forall((state(W),act_pair(X,Y)),
preference(J,W,X,Y);
preference(J,W,Y,X)
).
*/
axiom_P2(transitivity,(J,W),R):-
var(R),
agent(J),
state(W),
findall([X,Y,Z],
(
act_1(X),
act_1(Y),
act_1(Z),
preference(J,W,X,Y),
preference(J,W,Y,Z),
\+ preference(J,W,X,Z)
),
V),
(V\=[]->R=violation(V);R=true).
/***************** demo ********************************
?- axiom_P2(A,(1,a),C).
A = transitivity
C = true
Yes
?- axiom_P2(A,(1,b),C).
A = transitivity
C = true
Yes
?- axiom_P2(A,(1,c),C).
A = transitivity
C = true
Yes
?- axiom_P1(A,(3,_),C).
A = completeness
C = true
Yes
?- axiom_P2(A,(3,_),C). % please wait about a minutes.
A = transitivity
C = true
Yes
******************** end *****************************/
% ------------------------------------------------- %
% completion of preferences
% ------------------------------------------------- %
%%%%%%% %%%%%%%
%%%% script %%%%%
%%%%% %%%%%%
%%%%%%% %%%%%%%%
%%%%%%%% %%%%%%%%%
%%%%%%% %%%%%%%%
auto_completion(J):-
axiom_P1(completeness,(J,W),R),
R=violation(V),
forall(
member([X,Y],V),
(
assert(preference(J,W,X,Y)),
nl,
write(preference(J,W,X,Y)),
write(' has asserted.')
)),
fail.
auto_completion(J):-
nl,
write('the agent '),
write(J),
write('`s preferences have been completed.').
/***************** demo ********************************
?- auto_completion(1).
(...)
preference(1, c, [ ([a, b, c]->x)], [ ([a, b, c]->z)]) has asserted.
preference(1, c, [ ([a, b, c]->y)], [ ([a, b, c]->y)]) has asserted.
preference(1, c, [ ([a, b, c]->y)], [ ([a, b, c]->z)]) has asserted.
preference(1, c, [ ([a, b, c]->z)], [ ([a, b, c]->z)]) has asserted.
the agent 1`s preferences have been completed.
Yes
?- axiom_P1(A,(1,_),C).
A = completeness
C = true
Yes
?- axiom_P2(A,(1,_),C).
A = transitivity
C = violation(a, x, y, z)
Yes
?-
******************** end *****************************/
:- display_all_lines( [
' savage_null/3, belief_via_preference/3, possibility_via_preference/3: Savagian beliefs.'
]).
% ------------------------------------------------- %
% belief which represents preference relations
% ------------------------------------------------- %
% agent believes an event E at w if the complement of E is null.
belief_via_preference(Agent,Event,Belief):-
agent(Agent),
complement(Event,Complement),
findall(W,
savage_null(Agent,W,Complement),
B),
sort(B,Belief).
savage_null(Agent,State,Event):-
agent(Agent),
state(State),
event(Event),
complement(Event,Complement),
Complement\=[], % avoid void presumption.
forall(
(
composite_act(_,Act1,_),
composite_act(_,Act2,_),
member((Complement->X),Act1),
member((Complement->X),Act2)
),
(
indifference(Agent,State,Act1,Act2)
%,nl,write([State,Act1,Act2])
)
).
% ------------------------------------------------- %
% possiblity relation via preference relations
% ------------------------------------------------- %
possibility_via_preference_1(Agent,State,Possible):-
agent(Agent),
state(State),
findall(W,
(
state(W),
complement([W],Complement),
belief_via_preference(Agent,Complement,CBel),
\+ member(State,CBel)
),
P),
sort(P,Possible).
possibility_via_preference(Agent,State,Possible,Mode):-
agent(Agent),
state(State),
findall(W,
(
eventwise_binary_act(Act1, [W]->_X; Z),
eventwise_binary_act(Act2, [W]->_Y; Z),
SP=strict_preference(Agent,State,Act1,Act2),
SP
,(Mode=[d,_]-> (nl,tab(1),write(SP)) ;true)
),
P),
sort(P,Poss),
Data=[Poss,Agent,State],
compare_two_possible_sets(Mode,Data,Possible).
compare_two_possible_sets([_,d],[Poss,Agent,State],Possible):-
possibility_via_preference_1(Agent,State,Poss1),
(Poss1=Poss->Possible=Poss;Possible=(Poss,Poss1)),
!.
compare_two_possible_sets(_,[Poss|_],Poss).
possibility_via_preference(Agent,State,Possible):-
possibility_via_preference(Agent,State,Possible,[n,n]).
/***************** demo ********************************
?- display_goals(belief_of(3,_,_)).
belief_of(3, [], [])
belief_of(3, [c], [])
belief_of(3, [b], [b])
belief_of(3, [b, c], [b, c])
belief_of(3, [a], [])
belief_of(3, [a, c], [])
belief_of(3, [a, b], [a, b])
belief_of(3, [a, b, c], [a, b, c])
Yes
?- display_goals(belief_via_preference(3,_,_)).
belief_via_preference(3, [], [])
belief_via_preference(3, [c], [])
belief_via_preference(3, [b], [b])
belief_via_preference(3, [b, c], [b, c])
belief_via_preference(3, [a], [])
belief_via_preference(3, [a, c], [])
belief_via_preference(3, [a, b], [a, b])
belief_via_preference(3, [a, b, c], [a, b, c])
Yes
?- display_goals(savage_null(3,_,_)).
savage_null(3, a, [])
savage_null(3, a, [c])
savage_null(3, b, [])
savage_null(3, b, [c])
savage_null(3, b, [a])
savage_null(3, b, [a, c])
savage_null(3, c, [])
savage_null(3, c, [a])
Yes
?- display_goals(possibility_via_preference(3,_,_)).
possibility_via_preference(3, a, [a, b])
possibility_via_preference(3, b, [b])
possibility_via_preference(3, c, [b, c])
Yes
?- display_goals(possibility_via_preference(3,_,_,[d,d])).
strict_preference(3, a, [ ([a]->z), ([b, c]->x)], [ ([a]->y), ([b, c]->x)])
strict_preference(3, a, [ ([a]->z), ([b, c]->y)], [ ([a]->x), ([b, c]->y)])
strict_preference(3, a, [ ([a]->x), ([b, c]->z)], [ ([a]->y), ([b, c]->z)])
strict_preference(3, a, [ ([a, c]->z), ([b]->x)], [ ([a, c]->z), ([b]->y)])
strict_preference(3, a, [ ([a, c]->x), ([b]->z)], [ ([a, c]->x), ([b]->y)])
strict_preference(3, a, [ ([a, c]->y), ([b]->z)], [ ([a, c]->y), ([b]->x)])
possibility_via_preference(3, a, [a, b], [d, d])
strict_preference(3, b, [ ([a, c]->z), ([b]->x)], [ ([a, c]->z), ([b]->y)])
strict_preference(3, b, [ ([a, c]->x), ([b]->z)], [ ([a, c]->x), ([b]->y)])
strict_preference(3, b, [ ([a, c]->y), ([b]->z)], [ ([a, c]->y), ([b]->x)])
possibility_via_preference(3, b, [b], [d, d])
strict_preference(3, c, [ ([a, c]->z), ([b]->x)], [ ([a, c]->z), ([b]->y)])
strict_preference(3, c, [ ([a, c]->x), ([b]->z)], [ ([a, c]->x), ([b]->y)])
strict_preference(3, c, [ ([a, c]->y), ([b]->z)], [ ([a, c]->y), ([b]->x)])
strict_preference(3, c, [ ([a, b]->z), ([c]->x)], [ ([a, b]->z), ([c]->y)])
strict_preference(3, c, [ ([a, b]->x), ([c]->z)], [ ([a, b]->x), ([c]->y)])
strict_preference(3, c, [ ([a, b]->y), ([c]->z)], [ ([a, b]->y), ([c]->x)])
possibility_via_preference(3, c, [b, c], [d, d])
Yes
?-
******************** end *****************************/
:- display_all_lines( [
' auto_primitive_acts/0, escape_1/3: generating acts given preferences.'
]).
% ------------------------------------------------- %
% experimentation script for generating acts
% to approximate example 3 in Morris(1994):
% a risk neutral preference which confirms
% P(a)=[a,b]; P(b)=[b]; P(c)=[b,c].
% ------------------------------------------------- %
% added: 27-28 Dec 2004
% revised: 7 Jan 2004.
%%%%%%% %%%%%%%
%%%% script %%%%%
%%%%% %%%%%%
%%%%%%% %%%%%%%%
%%%%%%%% %%%%%%%%%
%%%%%%% %%%%%%%%
assign_values(A,B,C):-
% A: An assginment
% B: A base set
% C: The length of assignment
bag0(A,B,C),
sum(A,N),
N =< 3.
auto_primitive_acts:-
escape_original_primitive_acts,
abolish(escape_1/3),
abolish(last_id/1),
nl,write('work memory initilized.'),nl,
auto_primitive_acts_1.
auto_primitive_acts_1:-
consequences(Constants), % restricted to the consequences.
findall([X,W],primitive_act(X,W,_V),Acts),
assert(escape_1(domain_of_acts,Constants,Acts)),
length(Acts,N),
forall(assign_values(Values, Constants, N),
(
update_id(Id),
assert(escape_1(profile_of_prizes,Id,Values))
)
),
last_id(LId),
abolish(last_id/1),
write(LId),
write(' patterns generated.'), nl,
auto_primitive_acts_2.
auto_primitive_acts_2:-
auto_primitive_acts(_Id),
fail.
auto_primitive_acts_2:-
save_escaped_data,
nl,
write(complete).
auto_primitive_acts(Id):-
/*Constraints=[G1a,G1b,G1c],*/
EX=3, % example 3
G1a= possibility_via_preference(EX,a,Pa,[n,d]),
G1b= possibility_via_preference(EX,b,Pb,[n,d]),
G1c= possibility_via_preference(EX,c,Pc,[n,d]),
%G0= member(_V,Domain),
escape_1(domain_of_acts,_Domain,Acts),
escape_1(profile_of_prizes,Id,Values),
update_primitive_acts_with(Id,Acts,Values),
%findall(C,(member(C,Constraints),C),O),
write_by_times(10,Id),
G1a,G1b,G1c,
escape_generated_possibility_relations(Id,[Pa,Pb,Pc]),
escape_generated_primitive_acts(Id).
write_by_times(T,Id):-
0 is Id mod T,
save_escaped_data,
write([Id]),
!.
write_by_times(_,_).
save_escaped_data:-tell_goal('act.txt',forall,escape_1(_,_,_)).
update_primitive_acts_with(Id,Acts,Values):-
(var(Values)->
escape_1(profile_of_prizes,Id,Values)
;true),
P0= primitive_act(X,W,_),
P1= primitive_act(X,W,V),
escape_1(domain_of_acts,_Domain,Acts),
forall(P0,
(
retract(P0),
nth1(K,Acts,[X,W]),
nth1(K,Values,V),
assert(P1)
)
).
:- dynamic escape_0/1.
:- dynamic escape_1/3.
recover_primitive_acts:-
abolish(primitive_act/3),
forall(escape_0(L),(P=..L,assert(P))).
escape_original_primitive_acts:-
abolish(escape_0/1),
forall(primitive_act(A,B,C),
assert(escape_0([primitive_act,A,B,C]))
).
escape_generated_possibility_relations(Id,X):-
(\+ var(Id)->true;last_id(Id)),
assert(escape_1(possibility,Id,X)).
escape_generated_primitive_acts(Id):-
(\+ var(Id)->true;last_id(Id)),
forall(primitive_act(A,B,C),
assert(escape_1(primitive_act,Id,[A,B,C]))
% assert(escape_1(Id,X,[primitive_act,A,B,C]))
).
/***************** demo ********************************
?- auto_primitive_acts.
work memory initilized.
211 patterns generated.
[10][20][30][40][50][60][70][80]...[200][210]
complete
?- findall(P,escape_1(possibility,I,P),H),sort(H,H1),display_all_lines(H1).
%[[], [], []]
%[[], [], [c]]
%[[a], [], []]
%[[a], [], [c]]
%[[a, b], [b], [b]]
%[[a, b], [b], [b, c]]
%[[b], [b], [b]]
%[[b], [b], [b, c]]
P = _
I = _
H = [[[], [], []], [[], [], []], [[], [], []], [[], [], []], [[], [], []], [[], [], []], [[], []|...], [[]|...], [...|...]|...]
H1 = [[[], [], []], [[], [], [c]], [[a], [], []], [[a], [], [c]], [[a, b], [b], [b]], [[a, b], [b], [...|...]], [[b], [...]|...], [[...]|...]]
Yes
?- escape_1(domain_of_acts,Values,Acts).
Values = [0, 1, 2]
Acts = [[x, a], [x, b], [x, c], [y, a], [y, b], [y, c], [z, a], [z, b], [z, c]]
?- escape_1(profile_of_prizes,Id,C),
escape_1(possibility,Id,P),
(P=[[a,b],[b],[b,c]]),
nl,write(Id:P:C),fail.
13:[[a, b], [b], [b, c]]:[1, 1, 1, 0, 0, 0, 0, 0, 0]
26:[[a, b], [b], [b, c]]:[0, 1, 1, 1, 0, 0, 0, 0, 0]
39:[[a, b], [b], [b, c]]:[1, 0, 1, 0, 1, 0, 0, 0, 0]
45:[[a, b], [b], [b, c]]:[0, 0, 1, 1, 1, 0, 0, 0, 0]
56:[[a, b], [b], [b, c]]:[1, 1, 0, 0, 0, 1, 0, 0, 0]
64:[[a, b], [b], [b, c]]:[0, 1, 0, 1, 0, 1, 0, 0, 0]
68:[[a, b], [b], [b, c]]:[1, 0, 0, 0, 1, 1, 0, 0, 0]
71:[[a, b], [b], [b, c]]:[0, 0, 0, 1, 1, 1, 0, 0, 0]
87:[[a, b], [b], [b, c]]:[0, 1, 1, 0, 0, 0, 1, 0, 0]
97:[[a, b], [b], [b, c]]:[0, 0, 1, 0, 1, 0, 1, 0, 0]
102:[[a, b], [b], [b, c]]:[0, 1, 0, 0, 0, 1, 1, 0, 0]
105:[[a, b], [b], [b, c]]:[0, 0, 0, 0, 1, 1, 1, 0, 0]
121:[[a, b], [b], [b, c]]:[1, 0, 1, 0, 0, 0, 0, 1, 0]
127:[[a, b], [b], [b, c]]:[0, 0, 1, 1, 0, 0, 0, 1, 0]
136:[[a, b], [b], [b, c]]:[1, 0, 0, 0, 0, 1, 0, 1, 0]
139:[[a, b], [b], [b, c]]:[0, 0, 0, 1, 0, 1, 0, 1, 0]
145:[[a, b], [b], [b, c]]:[0, 0, 1, 0, 0, 0, 1, 1, 0]
148:[[a, b], [b], [b, c]]:[0, 0, 0, 0, 0, 1, 1, 1, 0]
162:[[a, b], [b], [b, c]]:[1, 1, 0, 0, 0, 0, 0, 0, 1]
170:[[a, b], [b], [b, c]]:[0, 1, 0, 1, 0, 0, 0, 0, 1]
174:[[a, b], [b], [b, c]]:[1, 0, 0, 0, 1, 0, 0, 0, 1]
177:[[a, b], [b], [b, c]]:[0, 0, 0, 1, 1, 0, 0, 0, 1]
188:[[a, b], [b], [b, c]]:[0, 1, 0, 0, 0, 0, 1, 0, 1]
191:[[a, b], [b], [b, c]]:[0, 0, 0, 0, 1, 0, 1, 0, 1]
195:[[a, b], [b], [b, c]]:[1, 0, 0, 0, 0, 0, 0, 1, 1]
198:[[a, b], [b], [b, c]]:[0, 0, 0, 1, 0, 0, 0, 1, 1]
201:[[a, b], [b], [b, c]]:[0, 0, 0, 0, 0, 0, 1, 1, 1]
No
?- escape_1(profile_of_prizes,Id,C),
escape_1(possibility,Id,P),
(P=[[],[],[c]];P=[[a],[],[]]),
nl,write(Id:P:C),fail.
2:[[a], [], []]:[1, 0, 0, 0, 0, 0, 0, 0, 0]
3:[[a], [], []]:[2, 0, 0, 0, 0, 0, 0, 0, 0]
9:[[], [], [c]]:[0, 0, 1, 0, 0, 0, 0, 0, 0]
15:[[], [], [c]]:[0, 0, 2, 0, 0, 0, 0, 0, 0]
18:[[a], [], []]:[0, 0, 0, 1, 0, 0, 0, 0, 0]
19:[[a], [], []]:[1, 0, 0, 1, 0, 0, 0, 0, 0]
20:[[a], [], []]:[2, 0, 0, 1, 0, 0, 0, 0, 0]
28:[[a], [], []]:[0, 0, 0, 2, 0, 0, 0, 0, 0]
29:[[a], [], []]:[1, 0, 0, 2, 0, 0, 0, 0, 0]
52:[[], [], [c]]:[0, 0, 0, 0, 0, 1, 0, 0, 0]
58:[[], [], [c]]:[0, 0, 1, 0, 0, 1, 0, 0, 0]
61:[[], [], [c]]:[0, 0, 2, 0, 0, 1, 0, 0, 0]
73:[[], [], [c]]:[0, 0, 0, 0, 0, 2, 0, 0, 0]
76:[[], [], [c]]:[0, 0, 1, 0, 0, 2, 0, 0, 0]
79:[[a], [], []]:[0, 0, 0, 0, 0, 0, 1, 0, 0]
80:[[a], [], []]:[1, 0, 0, 0, 0, 0, 1, 0, 0]
80:[[a], [], []]:[1, 0, 0, 0, 0, 0, 1, 0, 0]
81:[[a], [], []]:[2, 0, 0, 0, 0, 0, 1, 0, 0]
89:[[a], [], []]:[0, 0, 0, 1, 0, 0, 1, 0, 0]
93:[[a], [], []]:[0, 0, 0, 2, 0, 0, 1, 0, 0]
107:[[a], [], []]:[0, 0, 0, 0, 0, 0, 2, 0, 0]
108:[[a], [], []]:[1, 0, 0, 0, 0, 0, 2, 0, 0]
111:[[a], [], []]:[0, 0, 0, 1, 0, 0, 2, 0, 0]
158:[[], [], [c]]:[0, 0, 0, 0, 0, 0, 0, 0, 1]
164:[[], [], [c]]:[0, 0, 1, 0, 0, 0, 0, 0, 1]
167:[[], [], [c]]:[0, 0, 2, 0, 0, 0, 0, 0, 1]
179:[[], [], [c]]:[0, 0, 0, 0, 0, 1, 0, 0, 1]
185:[[], [], [c]]:[0, 0, 0, 0, 0, 2, 0, 0, 1]
203:[[], [], [c]]:[0, 0, 0, 0, 0, 0, 0, 0, 2]
206:[[], [], [c]]:[0, 0, 1, 0, 0, 0, 0, 0, 2]
209:[[], [], [c]]:[0, 0, 0, 0, 0, 1, 0, 0, 2]
No
?- update_primitive_acts_with(28,Acts,Values).
Acts = [[x, a], [x, b], [x, c], [y, a], [y, b], [y, c], [z, a], [z|...], [...|...]]
Values = [0, 0, 0, 2, 0, 0, 0, 0, 0]
Yes
?- display_goals(possibility_via_preference(3,_,_,[d,d])).
strict_preference(3, a, [ ([a]->y), ([b, c]->x)], [ ([a]->z), ([b, c]->x)])
strict_preference(3, a, [ ([a]->y), ([b, c]->z)], [ ([a]->x), ([b, c]->z)])
possibility_via_preference(3, a, [a], [d, d])
possibility_via_preference(3, b, [], [d, d])
possibility_via_preference(3, c, [], [d, d])
Yes
?-
******************** end *****************************/
:- display_all_lines( [
' dominance/2, axiom_PR/3, axiom_PNT/3,axiom_P3/3,axiom_P4: further axioms, etc.'
]).
% ------------------------------------------------- %
% dominance and some additional preference relations
% ------------------------------------------------- %
% added: 29 Dec 2004
% dominance relations: '>/', '>', '>>'
dominance(X,Y):-
act(X),
act(Y),
\+ (state(W),
act(X,W,V1),
act(Y,W,V2),
V2 >V1
).
strict_dominance(X,Y):-
dominance(X,Y),
\+ (\+ (state(W),
act(X, W, V1),
act(Y, W, V2),
V1 > V2
)).
strong_dominance(X,Y):-
dominance(X,Y),
forall(state(W),
(
act(X, W, V1),
act(Y, W, V2),
V1 > V2
)).
/***************** demo ********************************
?- update_primitive_acts_with(201,Acts,Values).
Acts = [[x, a], [x, b], [x, c], [y, a], [y, b], [y, c], [z, a], [z|...], [...|...]]
Values = [0, 0, 0, 0, 0, 0, 1, 1, 1]
Yes
?- display_goals(primitive_act(_,_,_)).
primitive_act(x, a, 0)
primitive_act(x, b, 0)
primitive_act(x, c, 0)
primitive_act(y, a, 0)
primitive_act(y, b, 0)
primitive_act(y, c, 0)
primitive_act(z, a, 1)
primitive_act(z, b, 1)
primitive_act(z, c, 1)
Yes
?- dominance(X,y).
X = x ;
X = y ;
X = z ;
X = [ ([a]->z), ([b]->y), ([c]->x)]
Yes
?- strict_dominance(X,y).
X = z ;
X = [ ([a]->z), ([b]->y), ([c]->x)]
Yes
******************** end *****************************/
% ------------------------------------------------- %
% Further axioms of Preferences:
% ------------------------------------------------- %
% Reflectivity and non-triviality
% ------------------------------------------------- %
axiom_PR(reflectivity,(J,W),R):-
agent(J),
state(W),
findall(X,
(
act_1(X),
\+ preference(J,W,X,X)
),
Y),
(Y\=[]->R=violation(Y);R=true).
axiom_PNT(non_triviality,(J,W),R):-
agent(J),
state(W),
(\+ (
act_1(X),
act_1(Y),
strict_preference(J,W,X,Y)
)
-> R=violation; R=true).
% Continuity and Monotonocity
% ------------------------------------------------- %
% added: 29 Dec 2004. P3 & P4.
axiom_P3(continuity_0,(J,W),R):- % not correct.
agent(J),
state(W),
findall([X,Y,Z],
(
act_1(X),act_1(Y),act_1(Z),
preference(J,W,X,Y),
indifference(J,W,X,Z),
strict_preference(J,W,Y,Z)
),
V),
(V\=[]->R=violation(V);R=true).
axiom_P4((monotonicity,i),(J,W),R):-
agent(J),
state(W),
findall([X,Y],
(
act_1(X),act_1(Y),
dominance(X,Y),
\+ preference(J,W,X,Y)
),
V),
(V\=[]->R=violation(V);R=true).
axiom_P4((monotonicity,ii),(J,S),R):-
agent(J),
state(S),
findall([W,[X,Y,Z],[X1,Y1,Z1]],
(
preference(J,S,Act1,Act2),
eventwise_binary_act(Act1, [W]->X; Z),
eventwise_binary_act(Act2, [W]->Y; Z),
eventwise_binary_act(Act3, [W]->X1; Z1),
eventwise_binary_act(Act4, [W]->Y1; Z1),
act(X1,W,U),
act(Y1,W,V),
U > V,
\+ strict_preference(J,S,Act3,Act4)
),
V),
(V\=[]->R=violation(V);R=true).
axiom_P4((monotonicity,iii),(J,W),R):-
agent(J),
state(W),
findall([X,Y],
(
act_1(X),act_1(Y),
strong_dominance(X,Y),
preference(J,W,Y,X)
),
V),
(V\=[]->R=violation(V);R=true).
% Lemma 1. P1--P4 -->P(w)=[S:forall(X>>Y,(Y>>Z,strict_prefer(J,S,[[W]->X|_],Y)].
% (A version of) Theorem 2 of Moris(1997, 1996).
% ------------------------------------------------- %
% Suppose a belief operator representing (completely ordered )
% preference relations.
% Then
% B1(distribution, but subset(MB,BM)) <--> P2 (transitivity)
% B2(necessitation) <--> PR (reflectivity)
% BM (monotonicity) always true
% BI (inconsistency) <--> PNT (non-triviality)
% verification of preference axioms in a lump
% ------------------------------------------------- %
% added: 11 Jan 2005.
verify_axioms_of_preferences(A:Name,Id:Values,Y):-
update_primitive_acts_with(Id,_Acts,Values),
member(A,[
axiom_P1,
axiom_P2,
axiom_PR,
axiom_PNT,
axiom_P3,
axiom_P4
]),
Agent=3,
Axiom=..[A,Name,(Agent,State),X],
setof((State,X), Axiom, Y0),
findall(State,member((State,violation),Y0),Y).
/***************** demo ********************************
?- verify_axioms_of_preferences(A,13:Values,Violated),nl,write(A:Violated),fail.
(axiom_P1:completeness):[]
(axiom_P2:transitivity):[]
(axiom_PR:reflectivity):[]
(axiom_PNT:non_triviality):[]
(axiom_P3:continuity_0):[]
(axiom_P4: (monotonicity, i)):[]
(axiom_P4: (monotonicity, ii)):[]
(axiom_P4: (monotonicity, iii)):[]
No
?-
******************** end *****************************/
:- display_all_lines( [
' axiom_B3-5, lemma_2/0, escape_3/3: equivalence of transitive/reflective/euclidean and B3/B4/B5.'
]).
% ------------------------------------------------- %
% further axioms of belief (knowledge) operators %
% ------------------------------------------------- %
% added: 30 Dec 2004.
% Lemma 2. (to be verified)
% P(w) is transitivie<->B3;is reflectivie<->B4;is euclidean<->B5.
axiom_B3(positive_introspection,J,X):-
var(X),
agent(J),
findall([E,BE,BBE],
(
belief_of(J,E,BE),
belief_of(J,BE,BBE),
\+ subset(BE,BBE)
),
Y),
(Y\=[]->X=violation(Y);X=hold).
axiom_B4(knowledge,J,X):- % axiom of knowledge, truth, or non-delusion.
var(X),
agent(J),
findall([E,BE],
(
belief_of(J,E,BE),
\+ subset(BE,E)
),
Y),
(Y\=[]->X=violation(Y);X=hold).
axiom_B5(negative_introspection,J,X):-
var(X),
agent(J),
findall([E,BE,NotBE,BNotBE],
(
belief_of(J,E,BE),
complement(BE,NotBE),
belief_of(J,NotBE,BNotBE),
\+ subset(NotBE,BNotBE)
),
Y),
(Y\=[]->X=violation(Y);X=hold).
/***************** demo ********************************
?- axiom_B3(Axiom,J,X), member(J, [1,2,3]), X\=hold.
Axiom = positive_introspection
J = 2
X = violation([[[a, c], [c], []]])
Yes
?- axiom_B4(Axiom,J,X),X\=hold.
No
?- axiom_B5(Axiom,1,X),X\=hold.
Axiom = negative_introspection
X = violation([[[b], [b], [a, c], []], [[b, c], [b, c], [a], []], [[a, b], [a, b], [c], []]])
Yes
?- axiom_B5(Axiom,2,X),X\=hold.
Axiom = negative_introspection
X = violation([[[b], [b], [a, c], [c]], [[b, c], [b], [a, c], [c]], [[a, b], [a, b], [c], []]])
Yes
?-
******************** end *****************************/
:- display_all_lines( [
' (prolonged) decsision problem and coherence.'
]).
% ------------------------------------------------- %
% Static Decision Problems and Coherency
% ------------------------------------------------- %
% added: 1 Jan 2004. P5 & P6 & P7.
% Nontriviality and Extended Sympathy: Axioms P5 and P6
% ------------------------------------------------- %
axiom_P5((nontriviality),J,R):-
var(R),
agent(J),
findall(W,
(
state(W),
\+ savage_null(J,W,[W])
),
Y),
(Y=[]->R=violation(J);R=true).
axiom_P6((extended_sympathy),J,R):-
var(R),
agent(J),
findall([S,X,Y],
(
possibility(J,S,H),
strict_preference_on_event(J,H,X,Y),
\+ strict_preference(J,S,X,Y)
),
Z),
(Y\=[]->R=violation(J,Z);R=true).
% Lemma 3. nontriviality(P5) -->knowledge axiom(B4)
% Lemma 4. extended_sympathy(P6) -->positive introspection(B3)
% Coherence: Axiom P7 on preferences.
% ------------------------------------------------- %
% under construction
/*
axiom_P7((coherence),(J,S),R):-
var(R),
possibility(J,S,H),
strict_preference_on_event(J,H,X,Y),
\+ strict_preference(J,W,X,Y),
R=violation([S,H,X,Y,W]);R=true.
*/
% Strong monotonocity:
% 'meta-ordering' (Definition 6 in Morris)
% satisfies the condition other than P1, P2, and P3.
% ------------------------------------------------- %
make_a_preference(Preference):-
Preference=[Id,Acts,Values],
update_primitive_acts_with(Id,Acts,Values),
write_by_times_prefer(10,Id).
write_by_times_prefer(T,Id):-
0 is Id mod T,
write([Id]),
!.
write_by_times_prefer(_,_).
meta_ordering([R1,R2,R3],W,Preference,S,D):-
make_a_preference(Preference),
strong_monotonicity(S,D),
(R1==n->true;axiom_P1(_,(1,W),R1)),
(R2==n->true;axiom_P2(_,(1,W),R2)),
(R3==n->true;axiom_P3(_,(1,W),R3)).
strong_monotonicity(S,D):-
P=(
primitive_act(X,W,V),
primitive_act(Y,W,U),
U >=V
),
Q=(
eventwise_binary_act(A, [W]->X; Z),
eventwise_binary_act(B, [W]->Y; Z),
\+ strict_preference(full,W,B,A)
),
verify_equality_of_goals(P:[W,X,Y],Q:[W,X,Y],S,D).
/***************** demo ********************************
?- findall(Id,(meta_ordering([n,n,n],[Id|_],S,D),D=[[],[]]),L).
[10][20][30][40][50][60][70][80][90][100][110][120][130][140][150][160][170][180][190][200][210]
L = [1, 90, 90, 131, 182]
Yes
?- member(Id,[1,90,131, 182]),escape_1(primitive_act,Id,[x,a,_]),
escape_1(possibility,Id,X).
Id = 1
X = [[], [], []] ;
Id = 90
X = [[], [], []] ;
Id = 90
X = [[], [], []] ;
Id = 131
X = [[], [], []] ;
Id = 182
X = [[], [], []] ;
No
?-
******************** end *****************************/
% ------------------------------------------------- %
% Lemma 2 : generate and test for belief operators
% ------------------------------------------------- %
% A classical result in epistemic logic restated wrt possibility
% correspondences in Morris(1996).
% B3 (positive introspection) iff P(w) is transitive.
% B4 (knowledge axiom) iff P(w) is reflective.
% B5 (negative introspection) iff P(w) is euclidean.
% experimentation design:
% (1) For agent 1, generate a possibility relations P( ) over three states [a,b,c].
% (2) Verify the above six propoerties.
% (3) Repeat until there is no P() any more.
% generating and test of possibility correspondence
% (non-)partitional information structure
% (i.e., accessibility relations of Kripke structure)
% ------------------------------------------------- %
assgin_event_for_each_state_in([],[]).
assgin_event_for_each_state_in([S|E],[S->H|F]):-
% H: An information set (not always an element of partition).
% S: A state
state(S),
event(H),
H \= [], % accessible set is not empty
assgin_event_for_each_state_in(E,F).
a_possbility_correspondence(F):-
all_states(S),
assgin_event_for_each_state_in(S,F).
% ex ante verification of possibility correspondences
% ------------------------------------------------- %
violation_of_possibility_correspondence(transitive,Possible,Violation):-
(var(Possible)->a_possbility_correspondence(Possible);true),
Violation=[S->H,W->H1],
member(S->H,Possible),
member(W,H),
member(W->H1,Possible),
\+ subset(H1,H).
check_possibility_correspondence(transitive,Possible,Violations):-
(var(Possible)->a_possbility_correspondence(Possible);true),
findall([S->H,W->H1],
(
member(S->H,Possible),
member(W,H),
member(W->H1,Possible),
\+ subset(H1,H)
),
Violations).
check_possibility_correspondence(reflective,Possible,Violations):-
(var(Possible)->a_possbility_correspondence(Possible);true),
findall([S->H],
(
member(S->H,Possible),
\+ member(S,H)
),
Violations).
check_possibility_correspondence(eucliadean,Possible,Violations):-
(var(Possible)->a_possbility_correspondence(Possible);true),
findall([S->H,W->H1],
(
member(S->H,Possible),
member(W,H),
member(W->H1,Possible),
\+ subset(H,H1)
),
Violations).
% pooling test (which would be used in lemma_2)
% ------------------------------------------------- %
% revised: 14 Jan 2005
filter_possibility_correspondence(Possible,([T,R,E],Constraint),Violations):-
(var(Possible)->a_possbility_correspondence(Possible);true),
(var(Constraint)->Constraint=([T,R,E]\=[yes,yes,yes]);true),
findall([[T,R,E],S->H,W->H1],
% The term is the 3rd argument of escape_3(verified,_,V).
(
filtered_data(Possible,Constraint,S->H,W->H1,[T,R,E])
),
Violations).
filtered_data(Possible,Constraint,S->H,W->H1,[T,R,E]):-
member(S->H,Possible),
possibility_reachable_from(Possible,[S,H],[W,H1],Z),
filter_possibility_rule([S,H],reflective,R),
filter_possibility_rule([Z,H,H1],transitive,T),
filter_possibility_rule([Z,H,H1],euclidean,E),
Constraint.
possibility_reachable_from(_,[_,[]],[[],[]],no).
possibility_reachable_from(Possible,[_S,H],[W,H1],yes):-
H\=[],
member(W,H),
member(W->H1,Possible).
filter_possibility_rule([_,[]],reflective,no).
filter_possibility_rule([S,H],reflective,R):-
H\=[],
(\+ member(S,H)->R=no;R=yes).
filter_possibility_rule([no,_,_],transitive,yes).
filter_possibility_rule([yes,H,H1],transitive,T):-
(\+ subset(H1,H)->T=no;T=yes).
filter_possibility_rule([no,_,_],euclidean,yes).
filter_possibility_rule([yes,H,H1],euclidean,E):-
(\+ subset(H,H1)->E=no;E=yes).
/***************** demo ********************************
?- filter_possibility_correspondence(Poss,_,Checked).
Poss = [ (a->[c]), (b->[c]), (c->[c])]
Checked = [[[yes, no, yes], (a->[c]), (c->[c])], [[yes, no, yes], (b->[c]), (c->[c])]] ;
Poss = [ (a->[c]), (b->[c]), (c->[b])]
Checked = [[[no, no, no], (a->[c]), (c->[b])], [[no, no, no], (b->[c]), (c->[b])], [[no, no, no], (c->[b]), (b->[c])]] ;
Poss = [ (a->[c]), (b->[c]), (c->[b, c])]
Checked = [[[no, no, yes], (a->[c]), (c->[b, c])], [[no, no, yes], (b->[c]), (c->[b, c])], [[yes, yes, no], (c->[b, c]), (b->[c])]] ;
Yes
?-
******************** end *****************************/
% ------------------------------------------------- %
% experimentation script of lemma 2
% ------------------------------------------------- %
% added: 31 Dec 2004.
% revised: 1-2 Jan 2005.
% Note: We will prolonged full generation of belief operators
% for three states model until the last part of this program.
%%%%%%% %%%%%%%
%%%% script %%%%%
%%%%% %%%%%%
%%%%%%% %%%%%%%%
%%%%%%%% %%%%%%%%%
%%%%%%% %%%%%%%%
:- dynamic escape_3/3.
lemma_2:-
lemma_2_preliminary,
lemma_2_step_1,
lemma_2_step_2.
lemma_2_preliminary:-
escape_original_possibility,
abolish(escape_3/3),
abolish(last_id/1),
nl,write('work memory initilized.'),
nl.
lemma_2_step_1:-
forall(
filter_possibility_correspondence(Poss,_,Checked),
(
update_id(Id),
assert(escape_3(possibility(Id),Poss,Checked))
)
),
last_id(LId),
abolish(last_id/1),
write(LId),
write(' patterns generated.'),
nl.
lemma_2_step_2:-
lemma_2_verification(_Id),
fail.
lemma_2_step_2:-
lemma_2_final_verification,
save_escaped_possibility,
nl,
write(complete).
lemma_2_verification(Id):-
J =1,
B3= axiom_B3(_tran,J,X3),
B4= axiom_B4(_refl,J,X4),
B5= axiom_B5(_eucl,J,X5),
escape_3(possibility(Id),Poss,_),
update_possibility_with(Id,Poss),
write_by_times(possibility,10,Id),
B3,B4,B5,
record_experimentation(verified,Id,[X3,X4,X5]).
record_experimentation(verified,Id,X):-
(\+ var(Id)->true;last_id(Id)),
forall(escape_3(possibility(Id),_,_),
assert(escape_3(verified,Id,X))
).
update_possibility_with(Id,Poss):-
(var(Poss)-> escape_3(possibility(Id),Poss,_);true),
P0=possibility(1,S,_),
P1=possibility(1,S,H),
forall(P0,
(
retract(P0),
member(S->H,Poss),
assert(P1)
)
).
recover_possibility:-
abolish(possibility/3),
forall(escape_3(0,original,P),assert(P)).
escape_original_possibility:-
X=escape_3(0,original,_),
forall(X,retract(X)),
forall(possibility(A,B,C),
assert(escape_3(0,original,possibility(A,B,C)))
).
write_by_times(possibility,T,Id):-
0 is Id mod T,
save_escaped_possibility,
write([Id]),
!.
write_by_times(possibility,_,_).
save_escaped_possibility:-tell_goal('poss.txt',forall,escape_3(_,_,_)).
% a naive code
lemma_2_final_verification_0([[ST,S3],[D3,DT]],[[SR,S4],[D4,DR]],[[SE,S5],[D5,DE]]):-
Data=[Id,Checked,B3,B4,B5],
findall(Data,
(
escape_3(possibility(Id),_Poss,Checked),
escape_3(verified,Id,[B3,B4,B5])
),
Table),
GT= (member(Data,Table),\+ member([[no,_,_]|_],Checked)),
GR= (member(Data,Table),\+ member([[_,no,_]|_],Checked)),
GE= (member(Data,Table),\+ member([[_,_,no]|_],Checked)),
G3=(member(Data,Table),B3=hold),
G4=(member(Data,Table),B4=hold),
G5=(member(Data,Table),B5=hold),
verify_equality_of_goals(GT:Id,G3:Id,[ST,S3],[D3,DT]),
verify_equality_of_goals(GR:Id,G4:Id,[SR,S4],[D4,DR]),
verify_equality_of_goals(GE:Id,G5:Id,[SE,S5],[D5,DE]).
/*
?- lemma_2_final_verification_0(A,B,C).
A = [[[1, 8, 15, 29, 43, 57, 58|...], [1, 8, 15, 29, 43, 57|...]], [[], []]]
B = [[[155, 157, 159, 161, 162, 164, 166|...], [155, 157, 159, 161, 162, 164|...]], [[], []]]
C = [[[1, 8, 17, 57, 58, 66, 115|...], [1, 8, 17, 57, 58, 66|...]], [[], []]] ;
No
?-
*/
% a refinement
lemma_2_final_verification:-
lemma_2_final_verification(collect,suc:S,dif:D),
lemma_2_final_verification(assert,suc:S,dif:D).
lemma_2_final_verification(collect,suc:[ST3,SR4,SE5],dif:[DT3,DR4,DE5]):-
Data=[Id,Checked,B3,B4,B5],
findall(Data,
(
escape_3(possibility(Id),_Poss,Checked),
escape_3(verified,Id,[B3,B4,B5])
),
Table),
verification_rule(tran=b3,[Data,Table],suc:ST3,dif:DT3),
verification_rule(refl=b4,[Data,Table],suc:SR4,dif:DR4),
verification_rule(eucl=b5,[Data,Table],suc:SE5,dif:DE5).
lemma_2_final_verification(assert,suc:[ST3,SR4,SE5],dif:[DT3,DR4,DE5]):-
assert(escape_3(verified,final(tran=b3),(suc:ST3,dif:DT3))),
assert(escape_3(verified,final(refl=b4),(suc:SR4,dif:DR4))),
assert(escape_3(verified,final(eucl=b5),(suc:SE5,dif:DE5))).
verification_rule(Name,[Data,Table],suc:[SP,SB],dif:[DP,DB]):-
Data=[Id,Checked,B3,B4,B5],
member( [Name,NoGood,Axiom],
[
[tran=b3,[no,_,_],B3],
[refl=b4,[_,no,_],B4],
[eucl=b5,[_,_,no],B5]
]
),
GP= (member(Data,Table),\+ member([NoGood,_,_],Checked)),
GB= (member(Data,Table), Axiom=hold),
verify_equality_of_goals(GP:Id,GB:Id,[SP,SB],[DB,DP]).
/***************** demo ********************************
% generation and testing of possibilitys
%---------------------------------------------------------
?- lemma_2.
work memory initilized.
343 patterns generated.
[10][20][30][40][50][60][70][80][90][100][110][120][130][140][150][160][170][180][190][200][210][220][230][240][250][260][270][280][290][300][310][320][330][340]
complete
Yes
% cf., 512 patterns if mapping empty set is permitted.
% the possibility relation of example 1 (and example 3).
% This example is not euclidean, therefore the belief system
% does not satisfy B5.
%---------------------------------------------------------
?- escape_3(possibility(I),[a->[a,b],b->[b],c->[b,c]],C),
escape_3(verified,I,[B3,B4,B5]).
I = 255
C = [[[yes, yes, no], (a->[a, b]), (b->[b])], [[yes, yes, no], (c->[b, c]), (b->[b])]]
B3 = hold
B3 = hold
B4 = hold
B5 = violation([[[b], [b], [a, c], []], [[b, c], [b, c], [a], []], [[a, b], [a, b], [c], []]])
Yes
?-
% the possibility relation of example 2.
% This example is either transitive or euclidean, therefore
% the belief system does not satisfy both B3 and B5.
%---------------------------------------------------------
?- escape_3(possibility(I),[a->[a,b],b->[b],c->[a,c]],C),
escape_3(verified,I,[B3,B4,B5]).
I = 257
C = [[[yes, yes, no], (a->[a, b]), (b->[b])], [[no, yes, no], (c->[a, c]), (a->[a, b])]]
B3 = violation([[[a, c], [c], []]])
B4 = hold
B5 = violation([[[b], [b], [a, c], [c]], [[b, c], [b], [a, c], [c]], [[a, b], [a, b], [c], []]])
Yes
?-
% possibility relations which are transitive, relfletive,
% and euclieadian simultaneously are partitional. And these
% are equivalent to the belief operator with axioms B3, B4, and B5.
%---------------------------------------------------------
?- escape_3(possibility(I), P, []).
I = 155
P = [ (a->[a]), (b->[b]), (c->[c])] ;
I = 164
P = [ (a->[a]), (b->[b, c]), (c->[b, c])] ;
I = 208
P = [ (a->[a, c]), (b->[b]), (c->[a, c])] ;
I = 281
P = [ (a->[a, b]), (b->[a, b]), (c->[c])] ;
I = 343
P = [ (a->[a, b, c]), (b->[a, b, c]), (c->[a, b, c])] ;
No
?- escape_3(verified,I,[hold,hold,hold]).
I = 155 ;
I = 164 ;
I = 208 ;
I = 281 ;
I = 343 ;
No
?- escape_3(verified,final(U),M).
U = tran=b3
M = suc:[[1, 8, 15, 29, 43, 57|...], [1, 8, 15, 29, 43|...]], dif:[[], []] ;
U = refl=b4
M = suc:[[155, 157, 159, 161, 162, 164|...], [155, 157, 159, 161, 162|...]], dif:[[], []] ;
U = eucl=b5
M = suc:[[1, 8, 17, 57, 58, 66|...], [1, 8, 17, 57, 58|...]], dif:[[], []] ;
No
?- abolish(escape_3/3).
Yes
% The case of empty map permitted.
?- ['poss_512.txt'].
% poss_512.txt compiled 0.34 sec, 848,788 bytes
Yes
?- escape_3(verified,final(U),M).
U = tran=b3
M = suc:[[1, 2, 3, 4, 5, 6|...], [1, 2, 3, 4, 5|...]], dif:[[], []] ;
U = refl=b4
M = suc:[[274, 276, 278, 280, 282, 284|...], [274, 276, 278, 280, 282|...]], dif:[[], []] ;
U = eucl=b5
M = suc:[[1, 2, 10, 17, 18, 19|...], [1, 2, 10, 17, 18|...]], dif:[[], []] ;
No
?-
******************** end *****************************/
% ex post verification of the nature of possibility correspondence
%---------------------------------------------------------
% added: 13 Jan 2005
verify_axioms_of_belief(Id,Belief,H):-
escape_3(verified,(Id),Verif),
findall((E->B),belief_of(1,E,B),Belief),
(Verif=[]->H=[b3:yes,b4:yes,b5:yes];true),
([hold,_,_]=Verif->H=[b3:yes,b4:_,b5:_];H=[b3:no,b4:_,b5:_]),
([_,hold,_]=Verif->H=[b3:_,b4:yes,b5:_];H=[b3:_,b4:no,b5:_]),
([_,_,hold]=Verif->H=[b3:_,b4:_,b5:yes];H=[b3:_,b4:_,b5:no]).
verify_axioms_of_possibility_correspondence(Id,Poss,H):-
escape_3(possibility(Id),Poss,Violated),
(Violated=[]->H=[yes,yes,yes];true),
(member([[no,_,_]|_],Violated)->H=[no,_,_];H=[yes,_,_]),
(member([[_,no,_]|_],Violated)->H=[_,no,_];H=[_,yes,_]),
(member([[_,_,no]|_],Violated)->H=[_,_,no];H=[_,_,yes]).
/***************** demo ********************************
?- verify_axioms_of_belief(Id,Belief,H).
Id = 1
Belief = [ ([]->[]), ([c]->[]), ([b]->[b]), ([b, c]->[b, c]), ([a]->[]), ([a, c]->[]), ([a|...]->[a|...]), ([...|...]->[...|...])]
H = [b3:yes, b4:no, b5:yes] ;
Id = 2
Belief = [ ([]->[]), ([c]->[]), ([b]->[b]), ([b, c]->[b, c]), ([a]->[]), ([a, c]->[]), ([a|...]->[a|...]), ([...|...]->[...|...])]
H = [b3:yes, b4:no, b5:yes] ;
Id = 3
Belief = [ ([]->[]), ([c]->[]), ([b]->[b]), ([b, c]->[b, c]), ([a]->[]), ([a, c]->[]), ([a|...]->[a|...]), ([...|...]->[...|...])]
H = [b3:yes, b4:no, b5:no]
Yes
?- verify_axioms_of_possibility_correspondence(Id,Poss,H).
Id = 1
Poss = [ (a->[]), (b->[]), (c->[])]
H = [yes, no, yes] ;
Id = 2
Poss = [ (a->[]), (b->[]), (c->[c])]
H = [yes, no, yes] ;
Id = 3
Poss = [ (a->[]), (b->[]), (c->[b])]
H = [yes, no, no]
Yes
?-
******************** end *****************************/
:- display_all_lines( [
' does_not_konw/3, be_unaware_of/4, axiom_UA/3: unawareness operators.'
]).
/**********************************************************/
/* modeling ignorance and unawareness */
/**********************************************************/
% added: 2 Jan 2005.
% revised: 3-7,10-13 Jan 2005.
% higher order ignorance
% ------------------------------------------------- %
does_not_know(J,E,NBE):-
belief_of(J,E,BE),
complement(BE,NBE).
ignorance_of_degree(1,[J,E,NBE],Series,Meet):-
does_not_know(J,E,NBE),
Series=[],
Meet=NBE.
ignorance_of_degree(K,[J,E,UKE],[UE|H],Meet):-
length([_|H],K1),
(K1>=5->!,fail %write('*** loop! *** please type n. to stop>'),read(y)
;true),
ignorance_of_degree(K1,[J,E,UE],H,M1),
K is K1 + 1,
does_not_know(J,UE,UKE),
intersection(M1,UKE,Meet).
% A cut and fail step below is a "look before you leap".
% However, it would be better to substitute a list of
% finite length in the last argument.
/***************** demo ********************************
% The cases where ignorance would be resolved in higer order beliefs,
% eventually, a total ignorance is succeeded by a full belief then oscillate forever.
% It may be conjectured that more states, more likely to oscillate.
% See the experimentation of strongly plausible unawareness below.
?- clause(belief_of_0(_,_,_),_)->abolish(belief_of_0/3).
Yes
?- update_possibility_with(255,Poss).
Poss = [ (a->[a, b]), (b->[b]), (c->[b, c])]
Yes
?- display_goals(belief_of(1,_,_)).
belief_of(1, [], [])
belief_of(1, [c], [])
belief_of(1, [b], [b])
belief_of(1, [b, c], [b, c])
belief_of(1, [a], [])
belief_of(1, [a, c], [])
belief_of(1, [a, b], [a, b])
belief_of(1, [a, b, c], [a, b, c])
Yes
?- display_goals(ignorance_of_degree(_,[1,[c],_],_,_)).
ignorance_of_degree(1, [1, [c], [a, b, c]], [], [a, b, c])
ignorance_of_degree(2, [1, [c], []], [[a, b, c]], [])
ignorance_of_degree(3, [1, [c], [a, b, c]], [[], [a, b, c]], [])
ignorance_of_degree(4, [1, [c], []], [[a, b, c], [], [a, b, c]], [])
ignorance_of_degree(5, [1, [c], [a, b, c]], [[], [a, b, c], [], [a, b, c]], [])
Yes
?- display_goals((ignorance_of_degree(_,[1,_,_],_,Meet),Meet\=[])).
ignorance_of_degree(1, [1, [], [a, b, c]], [], [a, b, c]), [a, b, c]\=[]
ignorance_of_degree(1, [1, [c], [a, b, c]], [], [a, b, c]), [a, b, c]\=[]
ignorance_of_degree(1, [1, [b], [a, c]], [], [a, c]), [a, c]\=[]
ignorance_of_degree(1, [1, [b, c], [a]], [], [a]), [a]\=[]
ignorance_of_degree(1, [1, [a], [a, b, c]], [], [a, b, c]), [a, b, c]\=[]
ignorance_of_degree(1, [1, [a, c], [a, b, c]], [], [a, b, c]), [a, b, c]\=[]
ignorance_of_degree(1, [1, [a, b], [c]], [], [c]), [c]\=[]
ignorance_of_degree(2, [1, [b], [a, b, c]], [[a, c]], [a, c]), [a, c]\=[]
ignorance_of_degree(2, [1, [b, c], [a, b, c]], [[a]], [a]), [a]\=[]
ignorance_of_degree(2, [1, [a, b], [a, b, c]], [[c]], [c]), [c]\=[]
Meet = _G172
Yes
?- update_possibility_with(342,P).
P = [ (a->[a, b, c]), (b->[a, b, c]), (c->[a, b])]
Yes
?- display_goals((ignorance_of_degree(_,[1,_,_],_,Meet),Meet\=[])).
ignorance_of_degree(1, [1, [], [a, b, c]], [], [a, b, c]), [a, b, c]\=[]
ignorance_of_degree(1, [1, [c], [a, b, c]], [], [a, b, c]), [a, b, c]\=[]
ignorance_of_degree(1, [1, [b], [a, b, c]], [], [a, b, c]), [a, b, c]\=[]
ignorance_of_degree(1, [1, [b, c], [a, b, c]], [], [a, b, c]), [a, b, c]\=[]
ignorance_of_degree(1, [1, [a], [a, b, c]], [], [a, b, c]), [a, b, c]\=[]
ignorance_of_degree(1, [1, [a, c], [a, b, c]], [], [a, b, c]), [a, b, c]\=[]
ignorance_of_degree(1, [1, [a, b], [a, b]], [], [a, b]), [a, b]\=[]
ignorance_of_degree(2, [1, [a, b], [a, b]], [[a, b]], [a, b]), [a, b]\=[]
ignorance_of_degree(3, [1, [a, b], [a, b]], [[a, b], [a, b]], [a, b]), [a, b]\=[]
ignorance_of_degree(4, [1, [a, b], [a, b]], [[a, b], [a, b], [a, b]], [a, b]), [a, b]\=[]
ignorance_of_degree(5, [1, [a, b], [a, b]], [[a, b], [a, b], [a, b], [a, b]], [a, b]), [a, b]\=[]
Meet = _G172
Yes
?-
******************** end *****************************/
% ------------------------------------------------- %
% operators of awareness and unawareness
% ------------------------------------------------- %
% (Modica and Rustichini,1994; Dekel et al.,1998)
% Ap iff Bp v (-Bp, B-Bp)
be_aware_of(J,E,[B,NB,BNB],A):-
belief_of(J,E,B),
does_not_know(J,E,NB),
belief_of(J,NB,BNB),
intersection(NB,BNB,A1),
union(B,A1,A).
% -Ap iff -Bp, (Bp v -B-Bp)
be_unaware_of(mr,J,E,UA,X):-
does_not_know(J,E,NB),
does_not_know(J,NB,NBNB),
intersection(NB,NBNB,UA),
X=[is_intersection_of,dk:NB,dk^2:NBNB].
be_unaware_of(npk(K),J,E,M,[U|H]):-
ignorance_of_degree(K,[J,E,U],H,M).
be_unaware_of(npk,J,E,M,[U|H]):-
K=5,
be_unaware_of(npk(K),J,E,M,[U|H]).
be_unaware_of(A,J,E,UE):-
be_unaware_of(A,J,E,UE,_).
% Example 2 of Dekel, Lipman, and Rustichini(1998).
% ------------------------------------------------- %
% In the latter part, we will verify this strongly plausible
% unawareness operator.
be_unaware_of(dlr98_ex_2,1,[],[]).
be_unaware_of(dlr98_ex_2,1,[c],[c]).
be_unaware_of(dlr98_ex_2,1,[b],[]).
be_unaware_of(dlr98_ex_2,1,[b,c],[]).
be_unaware_of(dlr98_ex_2,1,[a],[]).
be_unaware_of(dlr98_ex_2,1,[a,c],[]).
be_unaware_of(dlr98_ex_2,1,[a,b],[c]).
be_unaware_of(dlr98_ex_2,1,[a,b,c],[]).
% Note: It was prooved that standard state-space models
% i.e., (non-)partitional possibility corespondences
% can not satisfy npk.
% ------------------------------------------------- %
% axioms of unawareness
% ------------------------------------------------- %
% Symmetry axiom (Modica and Rustichini, 1994).
% ------------------------------------------------- %
axiom_UA(symmetry,[OP,J,E,UE],[X,UCE]):-
(var(UE)->
be_unaware_of(OP,J,E,UE)
;true),
complement(E,CE),
be_unaware_of(OP,J,CE,UCE),
(UE=UCE->X=hold;X=violate).
/***************** demo ********************************
% verifying the unawareness which satisfies
% Modica-Rustichini's symmetry axiom.
% ------------------------------------------------- %
% an example of unawareness operator which does not satify symmetry.
% example 1 of Dekel, Lipman, and Rustichini(1998)
?- clause(belief_of_0(_,_,_),_)->abolish(belief_of_0/3).
Yes
?- update_possibility_with(161,Poss).
I = 161
Poss = [ (a->[a]), (b->[b]), (c->[a, b, c])]
Yes
?- display_goals(be_unaware_of(mr,1,_,_)).
be_unaware_of(mr, 1, [], [])
be_unaware_of(mr, 1, [c], [])
be_unaware_of(mr, 1, [b], [c])
be_unaware_of(mr, 1, [b, c], [c])
be_unaware_of(mr, 1, [a], [c])
be_unaware_of(mr, 1, [a, c], [c])
be_unaware_of(mr, 1, [a, b], [c])
be_unaware_of(mr, 1, [a, b, c], [])
Yes
?- display_goals(axiom_UA(symmetry,[mr,1,_,_],_)).
axiom_UA(symmetry, [mr, 1, [], []], [hold, []])
axiom_UA(symmetry, [mr, 1, [c], []], [violate, [c]])
axiom_UA(symmetry, [mr, 1, [b], [c]], [hold, [c]])
axiom_UA(symmetry, [mr, 1, [b, c], [c]], [hold, [c]])
axiom_UA(symmetry, [mr, 1, [a], [c]], [hold, [c]])
axiom_UA(symmetry, [mr, 1, [a, c], [c]], [hold, [c]])
axiom_UA(symmetry, [mr, 1, [a, b], [c]], [violate, []])
axiom_UA(symmetry, [mr, 1, [a, b, c], []], [hold, []])
Yes
?-
******************** end *****************************/
% ------------------------------------------------- %
% dlr axioms (Dekel, Lipman and Rustichini, 1998).
% ------------------------------------------------- %
% The tree axioms: plausibility, AU- and KU-introspection
% revised: 11-13 Jan 2005.
% adding a variable of U-operator.
axiom_UA(plausibility,[OP,J,E,UE],[X,SUE]):-
be_unaware_of(mr,J,E,SUE),
be_unaware_of(OP,J,E,UE),
(subset(UE,SUE)->X=hold;X=violate).
axiom_UA(ku_introspection,[OP,J,E,UE],[X,KUE]):-
be_unaware_of(OP,J,E,UE),
belief_of(J,UE,KUE),
(KUE=[]->X=hold;X=violate).
% The synonyms
% ------------------------------------------------- %
axiom_UA(au_introspection,[OP,J,E,UE],[X,UUE]):-
be_unaware_of(OP,J,E,UE),
be_unaware_of(OP,J,UE,UUE),
(subset(UE,UUE)->X=hold;X=violate).
axiom_UA(dlr_axioms([T1,T2,T3]),[OP,J,E,UE],[X,SU,KU,UU]):-
event(E),
axiom_UA(plausibility,[OP,J,E,UE],[T1,SU]),
axiom_UA(ku_introspection,[OP,J,E,UE],[T2,KU]),
axiom_UA(au_introspection,[OP,J,E,UE],[T3,UU]),
(member(violate,[T1,T2,T3])->X=violate;X=hold).
axiom_UA(dlr_axioms,[OP,J,E,UE],X):-
axiom_UA(dlr_axioms(_),[OP,J,E,UE],X).
% ------------------------------------------------- %
% strong plausibility: no positive knowledge (NPK)
% ------------------------------------------------- %
% an approximated npk with truncation by 5-th degree.
% revised: 13-14 Jan 2005.
% revised: 21 Jan 2005.
axiom_UA(npk,[OP,J,E,M],[X,K]):-
K=5,
axiom_UA(npk_of_degree(K),[OP,J,E,_],[X,M]).
axiom_UA(strong_plausibility,[OP,J,E,M],[X,K]):-
axiom_UA(npk,[OP,J,E,M],[X,K]).
% a truncated version of axiom of no positive knowledge.
% ------------------------------------------------- %
% plausibility axiom is the case of K= 2.
axiom_UA(npk_of_degree(K),[OP,J,E,U],[X,M]):-
(var(OP)->OP=npk;true),
member(K,[1,2,3,4,5]),
be_unaware_of(npk(K),J,E,M),
be_unaware_of(OP,J,E,U),
(subset(U,M)->X=hold;X=violate).
/*
% the equivalence of unwareness operators mr and npk(2).
?- findall(ID,(update_possibility_with(ID,Po),
axiom_UA_pooled(symmetry,npk(2),1,hold)),L),assert(hold_sym(L)).
ID = _G157
Po = _G158
L = [1, 2, 10, 17, 18, 19, 28, 66, 74|...]
Yes
?- findall(ID,(update_possibility_with(ID,Po),
axiom_UA_pooled(symmetry,mr,1,hold)),L),assert(hold_sym_1(L)).
ID = _G157
Po = _G158
L = [1, 2, 10, 17, 18, 19, 28, 66, 74|...]
Yes
?- hold_sym(L),hold_sym_1(L1),subtract(L,L1,D),subtract(L1,L,D1).
L = [1, 2, 10, 17, 18, 19, 28, 66, 74|...]
L1 = [1, 2, 10, 17, 18, 19, 28, 66, 74|...]
D = []
D1 = []
Yes
?-
*/
%------------------------------------
% total test for unawareness axioms
%------------------------------------
% revised: 10,13, 21 Jan 2005.
axiom_UA_pooled(Axiom,OP,J,X):-
member(Axiom,[
symmetry,
plausibility,
ku_introspection,
au_introspection,
dlr_axioms,
strong_plausibility,
npk_of_degree(_),
npk
]),
agent(J),
member(OP,[mr,npk,npk(_),dlr98_ex_2]),
(\+ axiom_UA(Axiom,[OP,J,_,_],_)-> write(not_exsist),fail;true),
findall(E,
(
axiom_UA(Axiom,[OP,J,E,_],[violate|_])
),
Y),
(Y=[]->X=hold;X=violation(Y)).
axiom_UA_pooled(dlr_axioms([T1,T2,T3]),OP,J,X):-
agent(J),
member(OP,[mr,npk,npk(_),dlr98_ex_2]),
(\+ axiom_UA(dlr_axioms(_),[OP,J,_,_],_)-> write(not_exsist),fail;true),
findall([E,PL,KUI,AUI],
(
axiom_UA(dlr_axioms([PL,KUI,AUI]),[OP,J,E,_],[violate|_])
),
Y1),
findall(E,member([E,_,_,_],Y1),Y0),sort(Y0,Y),
findall(D,member([_|D],Y1),Y3),sort(Y3,Yd),
(Y1=[]->X=hold;X=violation(Yd,Y)),
is_no_violation_in_each_DLR_axioms(Yd,plausibility,T1),
is_no_violation_in_each_DLR_axioms(Yd,ku_introspection,T2),
is_no_violation_in_each_DLR_axioms(Yd,au_introspection,T3).
is_no_violation_in_each_DLR_axioms(Y,plausibility,n):-
member([T,_,_],Y),T \= hold,!.
is_no_violation_in_each_DLR_axioms(Y,ku_introspection,n):-
member([_,T,_],Y),T \= hold,!.
is_no_violation_in_each_DLR_axioms(Y,au_introspection,n):-
member([_,_,T],Y),T \= hold,!.
is_no_violation_in_each_DLR_axioms(_,_,y).
/***************** demo ********************************
% verification for partitional information structures
% ------------------------------------------------- %
?- ['poss.txt'].
% poss.txt compiled 0.29 sec, 584,352 bytes
Yes
?- %member(I,[155, 164, 208, 281, 343] ),
escape_3(possibility(I),Poss,[]),
update_possibility_with(I,Poss),OP=mr,
axiom_UA_pooled(dlr_axioms,OP,1,X),
axiom_UA_pooled(symmetry,OP,1,Y),
axiom_UA_pooled(npk,OP,1,Z).
I = 155
Poss = [ (a->[a]), (b->[b]), (c->[c])]
OP = mr
X = hold
Y = hold
Z = hold ;
I = 164
Poss = [ (a->[a]), (b->[b, c]), (c->[b, c])]
OP = mr
X = hold
Y = hold
Z = hold ;
I = 208
Poss = [ (a->[a, c]), (b->[b]), (c->[a, c])]
OP = mr
X = hold
Y = hold
Z = hold ;
I = 281
Poss = [ (a->[a, b]), (b->[a, b]), (c->[c])]
OP = mr
X = hold
Y = hold
Z = hold ;
I = 343
Poss = [ (a->[a, b, c]), (b->[a, b, c]), (c->[a, b, c])]
OP = mr
X = hold
Y = hold
Z = hold ;
No
?-
******************** end *****************************/
/***************** demo ********************************
% generating a symmetric possibility correspondence.
% and their nontrivial unawareness
% ------------------------------------------------- %
?- update_possibility_with(I,Poss),
axiom_UA_pooled(symmetry,mr,1,hold).
I = 1
Poss = [ (a->[c]), (b->[c]), (c->[c])] ;
I = 8
Poss = [ (a->[c]), (b->[b]), (c->[c])] ;
I = 17
Poss = [ (a->[c]), (b->[b, c]), (c->[b, c])] ;
I = 57
Poss = [ (a->[b]), (b->[b]), (c->[c])] ;
I = 58
Poss = [ (a->[b]), (b->[b]), (c->[b])]
(...)
Yes
?- nl, OP=mr,
write('ntua (nontrivial unawarenesses) for symmetric u operators'),
update_possibility_with(I,Poss),
axiom_UA_pooled(symmetry,OP,1,hold),
findall(E,(be_unaware_of(OP,1,E,U),U\=[]),Y),
nl,write([I]:Poss:ntua:Y),fail.
ntua (nontrivial unawarenesses) for symmetric u operators
[1]:[ (a->[c]), (b->[c]), (c->[c])]:ntua:[]
[8]:[ (a->[c]), (b->[b]), (c->[c])]:ntua:[]
[17]:[ (a->[c]), (b->[b, c]), (c->[b, c])]:ntua:[]
[57]:[ (a->[b]), (b->[b]), (c->[c])]:ntua:[]
[58]:[ (a->[b]), (b->[b]), (c->[b])]:ntua:[]
[66]:[ (a->[b]), (b->[b, c]), (c->[b, c])]:ntua:[]
[106]:[ (a->[b, c]), (b->[b]), (c->[c])]:ntua:[[c], [b], [a, c], [a, b]]
[115]:[ (a->[b, c]), (b->[b, c]), (c->[b, c])]:ntua:[]
[148]:[ (a->[a]), (b->[c]), (c->[c])]:ntua:[]
[155]:[ (a->[a]), (b->[b]), (c->[c])]:ntua:[]
[156]:[ (a->[a]), (b->[b]), (c->[b])]:ntua:[]
[158]:[ (a->[a]), (b->[b]), (c->[a])]:ntua:[]
[160]:[ (a->[a]), (b->[b]), (c->[a, b])]:ntua:[[b], [b, c], [a], [a, c]]
[164]:[ (a->[a]), (b->[b, c]), (c->[b, c])]:ntua:[]
[169]:[ (a->[a]), (b->[a]), (c->[c])]:ntua:[]
[172]:[ (a->[a]), (b->[a]), (c->[a])]:ntua:[]
[176]:[ (a->[a]), (b->[a, c]), (c->[c])]:ntua:[[c], [b, c], [a], [a, b]]
[201]:[ (a->[a, c]), (b->[c]), (c->[a, c])]:ntua:[]
[208]:[ (a->[a, c]), (b->[b]), (c->[a, c])]:ntua:[]
[222]:[ (a->[a, c]), (b->[a]), (c->[a, c])]:ntua:[]
[229]:[ (a->[a, c]), (b->[a, c]), (c->[a, c])]:ntua:[]
[281]:[ (a->[a, b]), (b->[a, b]), (c->[c])]:ntua:[]
[282]:[ (a->[a, b]), (b->[a, b]), (c->[b])]:ntua:[]
[284]:[ (a->[a, b]), (b->[a, b]), (c->[a])]:ntua:[]
[286]:[ (a->[a, b]), (b->[a, b]), (c->[a, b])]:ntua:[]
[343]:[ (a->[a, b, c]), (b->[a, b, c]), (c->[a, b, c])]:ntua:[]
No
% nontrivial unawarenesses would vanish when they satisfy dlr axioms.
?- nl, OP=mr,
write('nontrivial unawarenesses for dlr axioms-confirming u operators'),
update_possibility_with(I,Poss),
axiom_UA_pooled(dlr_axioms,OP,1,hold),
findall(E,(be_unaware_of(OP,1,E,U),U\=[]),Y),
nl,write([I]:Poss:ntua:Y),fail.
nontrivial unawarenesses for dlr axioms-confirming u operators
[1]:[ (a->[c]), (b->[c]), (c->[c])]:ntua:[]
[8]:[ (a->[c]), (b->[b]), (c->[c])]:ntua:[]
[17]:[ (a->[c]), (b->[b, c]), (c->[b, c])]:ntua:[]
[57]:[ (a->[b]), (b->[b]), (c->[c])]:ntua:[]
[58]:[ (a->[b]), (b->[b]), (c->[b])]:ntua:[]
[66]:[ (a->[b]), (b->[b, c]), (c->[b, c])]:ntua:[]
[115]:[ (a->[b, c]), (b->[b, c]), (c->[b, c])]:ntua:[]
[148]:[ (a->[a]), (b->[c]), (c->[c])]:ntua:[]
[155]:[ (a->[a]), (b->[b]), (c->[c])]:ntua:[]
[156]:[ (a->[a]), (b->[b]), (c->[b])]:ntua:[]
[158]:[ (a->[a]), (b->[b]), (c->[a])]:ntua:[]
[164]:[ (a->[a]), (b->[b, c]), (c->[b, c])]:ntua:[]
[169]:[ (a->[a]), (b->[a]), (c->[c])]:ntua:[]
[172]:[ (a->[a]), (b->[a]), (c->[a])]:ntua:[]
[201]:[ (a->[a, c]), (b->[c]), (c->[a, c])]:ntua:[]
[208]:[ (a->[a, c]), (b->[b]), (c->[a, c])]:ntua:[]
[222]:[ (a->[a, c]), (b->[a]), (c->[a, c])]:ntua:[]
[229]:[ (a->[a, c]), (b->[a, c]), (c->[a, c])]:ntua:[]
[281]:[ (a->[a, b]), (b->[a, b]), (c->[c])]:ntua:[]
[282]:[ (a->[a, b]), (b->[a, b]), (c->[b])]:ntua:[]
[284]:[ (a->[a, b]), (b->[a, b]), (c->[a])]:ntua:[]
[286]:[ (a->[a, b]), (b->[a, b]), (c->[a, b])]:ntua:[]
[343]:[ (a->[a, b, c]), (b->[a, b, c]), (c->[a, b, c])]:ntua:[]
No
?-
******************** end *****************************/
/***************** demo ********************************
% a strongly plausible possibility correspondence
% ------------------------------------------------- %
% example 1 of Dekel, Lipman, and Rustichini(1998)
?- update_possibility_with(161,Poss),
OP=mr,
axiom_UA_pooled(dlr_axioms(DLR),OP,1,X),
axiom_UA_pooled(symmetry,OP,1,Y),
axiom_UA_pooled(npk,OP,1,Z).
Poss = [ (a->[a]), (b->[b]), (c->[a, b, c])]
OP = mr
DLR = [y, y, n] % au-introspection has violated.
X = violation([[hold, hold, violate]], [[a], [a, b], [a, c], [b], [b, c]])
Y = violation([[c], [a, b]])
Z = hold
Yes
?- display_goals((event(E),be_unaware_of(mr,1,E,U))).
event([]), be_unaware_of(mr, 1, [], [])
event([c]), be_unaware_of(mr, 1, [c], [])
event([b]), be_unaware_of(mr, 1, [b], [c])
event([b, c]), be_unaware_of(mr, 1, [b, c], [c])
event([a]), be_unaware_of(mr, 1, [a], [c])
event([a, c]), be_unaware_of(mr, 1, [a, c], [c])
event([a, b]), be_unaware_of(mr, 1, [a, b], [c])
event([a, b, c]), be_unaware_of(mr, 1, [a, b, c], [])
E = _G160
U = _G165
Yes
?- display_goals((event(E),be_unaware_of(npk(2),1,E,U))).
event([]), be_unaware_of(npk(2), 1, [], [])
event([c]), be_unaware_of(npk(2), 1, [c], [])
event([b]), be_unaware_of(npk(2), 1, [b], [c])
event([b, c]), be_unaware_of(npk(2), 1, [b, c], [c])
event([a]), be_unaware_of(npk(2), 1, [a], [c])
event([a, c]), be_unaware_of(npk(2), 1, [a, c], [c])
event([a, b]), be_unaware_of(npk(2), 1, [a, b], [c])
event([a, b, c]), be_unaware_of(npk(2), 1, [a, b, c], [])
E = _G160
U = _G167
Yes
?- display_goals((event(E),be_unaware_of(npk,1,E,U))).
event([]), be_unaware_of(npk, 1, [], [])
event([c]), be_unaware_of(npk, 1, [c], [])
event([b]), be_unaware_of(npk, 1, [b], [c])
event([b, c]), be_unaware_of(npk, 1, [b, c], [c])
event([a]), be_unaware_of(npk, 1, [a], [c])
event([a, c]), be_unaware_of(npk, 1, [a, c], [c])
event([a, b]), be_unaware_of(npk, 1, [a, b], [])
event([a, b, c]), be_unaware_of(npk, 1, [a, b, c], [])
E = _G160
U = _G165
Yes
?- display_goals(axiom_UA(dlr_axioms(_),[mr,1,_,_],_)).
axiom_UA(dlr_axioms([hold, hold, hold]), [mr, 1, [], []], [hold, [], [], []])
axiom_UA(dlr_axioms([hold, hold, hold]), [mr, 1, [c], []], [hold, [], [], []])
axiom_UA(dlr_axioms([hold, hold, violate]), [mr, 1, [b], [c]], [violate, [c], [], []])
axiom_UA(dlr_axioms([hold, hold, violate]), [mr, 1, [b, c], [c]], [violate, [c], [], []])
axiom_UA(dlr_axioms([hold, hold, violate]), [mr, 1, [a], [c]], [violate, [c], [], []])
axiom_UA(dlr_axioms([hold, hold, violate]), [mr, 1, [a, c], [c]], [violate, [c], [], []])
axiom_UA(dlr_axioms([hold, hold, violate]), [mr, 1, [a, b], [c]], [violate, [c], [], []])
axiom_UA(dlr_axioms([hold, hold, hold]), [mr, 1, [a, b, c], []], [hold, [], [], []])
Yes
?- display_goals(axiom_UA(npk_of_degree(3),[mr,1,_,_],_)).
axiom_UA(npk_of_degree(3), [mr, 1, [], []], [hold, []])
axiom_UA(npk_of_degree(3), [mr, 1, [c], []], [hold, []])
axiom_UA(npk_of_degree(3), [mr, 1, [b], [c]], [hold, [c]])
axiom_UA(npk_of_degree(3), [mr, 1, [b, c], [c]], [hold, [c]])
axiom_UA(npk_of_degree(3), [mr, 1, [a], [c]], [hold, [c]])
axiom_UA(npk_of_degree(3), [mr, 1, [a, c], [c]], [hold, [c]])
axiom_UA(npk_of_degree(3), [mr, 1, [a, b], [c]], [violate, []])
axiom_UA(npk_of_degree(3), [mr, 1, [a, b, c], []], [hold, []])
Yes
******************** end *****************************/
% An integrated test for unawareness axioms
% ------------------------------------------------- %
% revised: 10,13 Jan 2005.
:- dynamic escape_4/3.
generate_and_test_of_unawareness(OP,[H1,H2,DLR,H3],[T1,T2,T3],Constraint,Values):-
abolish(escape_4/3),
(nl,write(id:p345:possibility:[symmetry,dlr_axioms,npk])),
forall(
(
verify_axioms_of_possibility_correspondence(Id,Poss,P345),
update_possibility_with(Id,Poss),
axiom_UA_pooled(symmetry,OP,1,H1),(H1=hold->T1=y;T1=n),
axiom_UA_pooled(dlr_axioms(DLR),OP,1,H2),(H2=hold->T2=y;T2=n),
axiom_UA_pooled(npk,OP,1,H3),(H3=hold->T3=y;T3=n),
Constraint,
assert(
escape_4(poss(Id:P345:Poss),[sym:T1,npk:T3,dlr:[T2:DLR]],[cond:Constraint,value:Values])
)
),
(nl,write(Id:P345:Poss:[T1,T2,T3]:Values))
).
/***************** demo ********************************
?- generate_and_test_of_unawareness(npk,_,_, true,(op:npk,ful)).
id:p345:possibility:[symmetry, dlr_axioms, npk]
1:[yes, no, yes]:[ (a->[c]), (b->[c]), (c->[c])]:[y, y, y]: (op:npk, ful)
2:[no, no, no]:[ (a->[c]), (b->[c]), (c->[b])]:[n, n, y]: (op:npk, ful)
3:[no, no, no]:[ (a->[c]), (b->[c]), (c->[b, c])]:[n, n, y]: (op:npk, ful)
4:[no, no, no]:[ (a->[c]), (b->[c]), (c->[a])]:[n, n, y]: (op:npk, ful)
5:[no, no, no]:[ (a->[c]), (b->[c]), (c->[a, c])]:[n, n, y]: (op:npk, ful)
6:[no, no, no]:[ (a->[c]), (b->[c]), (c->[a, b])]:[n, n, y]: (op:npk, ful)
7:[no, no, no]:[ (a->[c]), (b->[c]), (c->[a, b, c])]:[n, n, y]: (op:npk, ful)
8:[yes, no, yes]:[ (a->[c]), (b->[b]), (c->[c])]:[y, y, y]: (op:npk, ful)
9:[no, no, no]:[ (a->[c]), (b->[b]), (c->[b])]:[y, y, y]: (op:npk, ful)
(...)
340:[no, no, no]:[ (a->[a, b, c]), (b->[a, b, c]), (c->[a])]:[n, n, y]: (op:npk, ful)
341:[no, yes, no]:[ (a->[a, b, c]), (b->[a, b, c]), (c->[a, c])]:[y, y, y]: (op:npk, ful)
342:[no, no, no]:[ (a->[a, b, c]), (b->[a, b, c]), (c->[a, b])]:[n, n, y]: (op:npk, ful)
343:[yes, yes, yes]:[ (a->[a, b, c]), (b->[a, b, c]), (c->[a, b, c])]:[y, y, y]: (op:npk, ful)
Yes
?- escape_4(A,[S,N,D],V).
A = poss(1:[yes, no, yes]:[ (a->[c]), (b->[c]), (c->[c])])
S = sym:y
N = npk:y
D = dlr:[y:[y, y, y]]
V = [cond:true, value: (op:npk, ful)]
Yes
?- Constraints=(
findall(E,(be_unaware_of(npk,1,E,U),U\=[]),Y),
findall(E,(belief_of(1,E,B),B\=[]),Z)
),
Values=[nontrivial_u_of_npk:Y,positive_knowledges:Z],
generate_and_test_of_unawareness(npk,_,_, Constraints,Values).
(...)
Yes
?- escape_4(A,[sym:S,npk:N,dlr:[y:_]],[_,value:[NTU,PK]]).
A = poss(1:[yes, no, yes]:[ (a->[c]), (b->[c]), (c->[c])])
S = y
N = y
NTU = nontrivial_u_of_npk:[]
PK = positive_knowledges:[[c], [b, c], [a, c], [a, b, c]] ;
A = poss(8:[yes, no, yes]:[ (a->[c]), (b->[b]), (c->[c])])
S = y
N = y
NTU = nontrivial_u_of_npk:[]
PK = positive_knowledges:[[c], [b], [b, c], [a, c], [a, b], [a, b|...]] ;
A = poss(9:[no, no, no]:[ (a->[c]), (b->[b]), (c->[b])])
S = y
N = y
NTU = nontrivial_u_of_npk:[]
PK = positive_knowledges:[[c], [b], [b, c], [a, c], [a, b], [a, b|...]]
Yes
No
?- tell_goal('ua_dlr.txt',forall,escape_4(_,_,_)).
Yes
?-
******************** end *****************************/
/***************** demo ********************************
% testing the possibility correspondences where
% empty sets allowed for all events as well as for [].
% ------------------------------------------------- %
% by a minor modification at assgin_event_for_each_state_in/2.
% The 512 ptterns generated have saved as 'poss_512.txt';
% cautions: Please abolish escape_3/3 before redefine them.
% The id numbers of possibility correspondences have changed.
?- Constraints=(
findall(E,(be_unaware_of(npk,1,E,U),U\=[]),Y),
findall(E,(belief_of(1,E,B),B\=[]),Z)
),
Values=[nontrivial_u_of_npk:Y,positive_knowledges:Z],
generate_and_test_of_unawareness(npk,_,_, Constraints,Values).
(...)
Yes
?- tell_goal('ua_dlr_512.txt',forall,escape_4(_,_,_)).
Yes
?- escape_4(A,[sym:S,npk:N,dlr:[y:D]],[_,value:[_:NTU,PK]]),NTU\=[].
No
?- escape_4(A,[sym:y,npk:N,dlr:D],[_,value:[_:NTU,PK]]),NTU\=[].
A = poss(210:[yes, no, no]:[ (a->[b, c]), (b->[b]), (c->[c])])
N = y
D = [n:[y, y, n]]
NTU = [[c], [b], [a, c], [a, b]]
PK = positive_knowledges:[[c], [b], [b, c], [a, c], [a, b], [a, b|...]] ;
A = poss(279:[yes, no, no]:[ (a->[a]), (b->[b]), (c->[a, b])])
N = y
D = [n:[y, y, n]]
NTU = [[b], [b, c], [a], [a, c]]
PK = positive_knowledges:[[b], [b, c], [a], [a, c], [a, b], [a, b|...]] ;
A = poss(280:[yes, yes, no]:[ (a->[a]), (b->[b]), (c->[a, b|...])])
N = y
D = [n:[y, y, n]]
NTU = [[b], [b, c], [a], [a, c]]
PK = positive_knowledges:[[b], [b, c], [a], [a, c], [a, b], [a, b|...]] ;
A = poss(298:[yes, no, no]:[ (a->[a]), (b->[a, c]), (c->[c])])
N = y
D = [n:[y, y, n]]
NTU = [[c], [b, c], [a], [a, b]]
PK = positive_knowledges:[[c], [b, c], [a], [a, c], [a, b], [a, b|...]] ;
A = poss(314:[yes, yes, no]:[ (a->[a]), (b->[a, b, c]), (c->[c])])
N = y
D = [n:[y, y, n]]
NTU = [[c], [b, c], [a], [a, b]]
PK = positive_knowledges:[[c], [b, c], [a], [a, c], [a, b], [a, b|...]] ;
A = poss(466:[yes, yes, no]:[ (a->[a, b, c]), (b->[b]), (c->[c])])
N = y
D = [n:[y, y, n]]
NTU = [[c], [b], [a, c], [a, b]]
PK = positive_knowledges:[[c], [b], [b, c], [a, c], [a, b], [a, b|...]] ;
No
******************** end *****************************/
%-------------------------------------------------------------------
% verifying the known results of unawarenesses and some findings
% under truncated npk operators with three states
%-------------------------------------------------------------------
% revised: 14 Jan 2005.
% Given the above experimental data escape_4/3 (saved in ua_dlr_512.txt),
% (1)All three dlr axioms confirming unawareness operators are also satisfy symmetric axioms.
% Further, they eliminate nontrivial unawarenesses.
% (This confirms the first half of Dekel et al.'s theorem 1 since the beliefs are normal.)
% (2)If au- and ku- introspection are both satisified, the operator is symmetric.
% (3)If symmetric, nontrivial unawareness are only those without negative introspection.
% And these six cases therefore obey first two axioms, but violate au-introspection.
% (4)No full ignorant cases.
/***************** demo ********************************
% (1) the three dlr axioms -> symmetry
?- escape_4(A,[sym:n,npk:N,dlr:D],[_,value:[_:NTU,PK]]),D=[y:D1].
No
?- escape_4(A,[sym:S,npk:N,dlr:[y:_]],[_,value:[_:NTU,PK]]),NTU\=[].
No
?-
% (2) au- and ku- introspection -> symmetry
?- escape_4(A,[sym:n,npk:N,dlr:D],[_,value:[_:NTU,PK]]),D=[_:[_,y,y]].
No
?-
% (3) symmetry -> (negative introspection --> trivial unawareness)
?- escape_4(A,[sym:y,npk:N,dlr:D],[_,value:[_:NTU,PK]]),NTU\=[].
A = poss(210:[yes, no, no]:[ (a->[b, c]), (b->[b]), (c->[c])])
N = y
D = [n:[y, y, n]]
NTU = [[c], [b], [a, c], [a, b]]
PK = positive_knowledges:[[c], [b], [b, c], [a, c], [a, b], [a, b|...]] ;
A = poss(279:[yes, no, no]:[ (a->[a]), (b->[b]), (c->[a, b])])
N = y
D = [n:[y, y, n]]
NTU = [[b], [b, c], [a], [a, c]]
PK = positive_knowledges:[[b], [b, c], [a], [a, c], [a, b], [a, b|...]] ;
A = poss(280:[yes, yes, no]:[ (a->[a]), (b->[b]), (c->[a, b|...])])
N = y
D = [n:[y, y, n]]
NTU = [[b], [b, c], [a], [a, c]]
PK = positive_knowledges:[[b], [b, c], [a], [a, c], [a, b], [a, b|...]] ;
A = poss(298:[yes, no, no]:[ (a->[a]), (b->[a, c]), (c->[c])])
N = y
D = [n:[y, y, n]]
NTU = [[c], [b, c], [a], [a, b]]
PK = positive_knowledges:[[c], [b, c], [a], [a, c], [a, b], [a, b|...]] ;
A = poss(314:[yes, yes, no]:[ (a->[a]), (b->[a, b, c]), (c->[c])])
N = y
D = [n:[y, y, n]]
NTU = [[c], [b, c], [a], [a, b]]
PK = positive_knowledges:[[c], [b, c], [a], [a, c], [a, b], [a, b|...]] ;
A = poss(466:[yes, yes, no]:[ (a->[a, b, c]), (b->[b]), (c->[c])])
N = y
D = [n:[y, y, n]]
NTU = [[c], [b], [a, c], [a, b]]
PK = positive_knowledges:[[c], [b], [b, c], [a, c], [a, b], [a, b|...]] ;
No
?-
% (4) no no positive knowlege.
?- escape_4(A,[sym:S,npk:N,dlr:D],[_,value:[_:NTU,_:PK]]),PK=[].
No
?-
******************** end *****************************/
% Known theorems of unawareness operators:
%-------------------------------------------------------------------
% (1) The symmetry axiom of unawareness with standard logical deduction rules
% means (reflective) partition (S5).
% therefore there is no unawareness ( Modica and Rustichini, 1994).
% (2) Alternative axioms (No positive knowledge condition) cannot be satisfied
% by standard possibility correspondeces(Dekel, Lipman, and Rustichini, 1998).
% (2-i) the necessitation of belief,
% so the reflectiveness (p4), implies no unawareness, and
% (2-ii) the monotonicity of belief, which is implied by transitivity (p3),
% but implies that a total ignorance implied by a nonempty unawareness event.
:- display_all_lines( [
' careate_belief_of_0_for_each_event/1: full generation of belief operator.'
]).
% ------------------------------------------------- %
% script of generating and test for unawareness
% ------------------------------------------------- %
% added: 8-9 Jan 2005.
%%%%%%% %%%%%%%
%%%% script %%%%%
%%%%% %%%%%%
%%%%%%% %%%%%%%%
%%%%%%%% %%%%%%%%%
%%%%%%% %%%%%%%%
% the script of experimentation
% ----------------------------------------------------------- %
:- dynamic escape_2/3, belief_of_0/3, be_unaware_of_0/3.
create_powerset_if_no_data(P):-
clause(escape_2(power_set,_S,P),_),
!.
create_powerset_if_no_data(P):-
findall(E,event(E),P),
all_states(S),
assert(escape_2(power_set,S,P)).
% generate beliefs without to commit detabase.
assign_belief_of_0_for_each_event([],[]).
assign_belief_of_0_for_each_event([E|B],[E->C|D]):-
assign_belief_of_0_for_each_event(B,D),
all_states(S),
event(C),
%(E=S->C=S;true), % enforcing to obey the axiom B2
(E=S->C\=S;true), % leading to betray the axiom B2
(E=[]->C=[];true).
% generation of belief_of_0/3.
create_belief_of_0_for_each_event(B):-
create_powerset_if_no_data(P),
assign_belief_of_0_for_each_event(P,B),
update_belief_of_0(B).
update_belief_of_0([E->C|B]):-
O=belief_of_0(1,E,_),
forall(clause(O,_),retract(O)),
assert(belief_of_0(1,E,C)),
update_belief_of_0(B).
update_belief_of_0([]).
write_by_times_for_belief_of_0(T,Id):-
0 is Id mod T,
save_escape_2,
write([Id]),
!.
write_by_times_for_belief_of_0(_,_).
save_escape_2:-tell_goal('ua.txt',forall,escape_2(_,_,_)).
/***************** demo ********************************
% a strongly plausible unawareness.
% ----------------------------------------------------------- %
% Example 2 of Dekel, Lipman, and Rustichini(1998).
% caution: belief_of_0/3 will be generated.
% It procedes possibility relations (cf., belief_of_1/3).
?- create_belief_of_0_for_each_event([
[]->[],
[c]->[],
[b]->[b],
[b, c]->[b],
[a]->[a],
[a, c]->[a,c],
[a, b]->[a,b],
[a, b, c]->[a, b]
]).
Yes
?- axiom_UA_pooled(symmetry,dlr98_ex_2,1,H1),(H1=hold->T1=yes;T1=no),
axiom_UA_pooled(dlr_axioms(DLR),dlr98_ex_2,1,H2),(H2=hold->T2=yes;T2=no).
H1 = hold
T1 = yes
DLR = [y, y, y]
H2 = hold
T2 = yes
Yes
?-
******************** end *****************************/
:- display_all_lines( [
' create_belief_of_0/0: full genaration of beleif operators.'
,' verify_theorem_1/2: test of equivalence of nomal beliefs and possibility relations.'
]).
/**********************************************************/
/* full beliefs : normality <--> possibility relations */
/**********************************************************/
% added: 9-10 Jan 2005.
% ----------------------------------------------------------- %
% full genaration of beleif operators
% ----------------------------------------------------------- %
create_belief_of_0(Cond,stop_id(T)):-
%Cond=[[XB1,XB2],[Id,Pos,Dif]],
initialize_create_belief_of_0,
create_iteratively_belief_of_0(Cond,stop_id(T)),
finilize_create_belief_of_0.
initialize_create_belief_of_0:-
abolish(escape_2/3),
abolish(last_id/1),
(\+ clause(escape_3(_,_,_),_)
->['poss.txt'];true).
create_iteratively_belief_of_0(Cond,stop_id(T)):-
create_iteratively_belief_of_0(Cond,stop_id(T),_Id),
fail.
create_iteratively_belief_of_0(_,_).
finilize_create_belief_of_0:-
save_escape_2,
nl,
write('complete').
% unconditional generation of belief operators with stopping time
create_iteratively_belief_of_0(M,stop_id(T),Id):-
(M==full_beliefs->true;fail),
create_belief_of_0_for_each_event(B),
update_id(Id),
assert(escape_2(belief_0,Id,B)),
write_by_times_for_belief_of_0(1000,Id),
((var(T);Idtrue;!).
% conditional generation of belief operators with stopping time
create_iteratively_belief_of_0(Cond,stop_id(T),Id):-
Cond=[[XB1,XB2],[Id,Pos,Dif]],
XB=[XB1,XB2],XP=[_Pid,Pos,Dif],
cautious_generation_of_belief_of_0(B,XB,XP),
update_id(Id),
assert(escape_2(belief_0,Id,B)),
assert(escape_2(verified,Id,[ax:XB,pc:XP])),
write_by_times_for_belief_of_0(1000,Id),
((var(T);Idtrue;!).
cautious_generation_of_belief_of_0(B,[XB1,XB2],X):-
(var(B)->create_belief_of_0_for_each_event(B);true),
is_consistent_with_possibility(X),
beliefs_are_satisfying_axiom(distribution,XB1),
beliefs_are_satisfying_axiom(totology,XB2).
% inspections for the generated beliefs.
beliefs_are_satisfying_axiom(Axiom,X):-
J=1,
member([Axiom,Goal],[
[distribution,axiom_B1(Axiom,J,T)],
[totology,axiom_B2(Axiom,J,T)]
]),
Goal,
(T=hold->X=T;X=violate).
is_consistent_with_possibility(X):-
beliefs_represent_possibility(Pid,Poss),
!,
update_possibility_with(Pid,Poss),
verify_equality_of_goals(
belief_of_0(1,E,B):[E,B],
belief_of_1(1,E,B1):[E,B1],
_S,D),
X=[Pid,Poss,D].
is_consistent_with_possibility(not_exsist).
beliefs_represent_possibility(Pid,Poss):-
possibility_1(at(a),agent(1),think(Pa)),
possibility_1(at(b),agent(1),think(Pb)),
possibility_1(at(c),agent(1),think(Pc)),
Poss=[(a->Pa),(b->Pb),(c->Pc)],
escape_3(possibility(Pid),Poss,_).
/***************** demo ********************************
% a test of generating belief operators.
% ----------------------------------------------------------- %
% Hereafter,
% we restrict experimentations to be enforced B2, B[a,b,c]=[a,b,c].
% Arguments D1 and D2 below are
% the assymetric diffrence of two types of belief operators;
% belief_of_0/3 as operaors on events generated directly (which does not satisfy B2 in this use),
% belief_of_1/3 as reproduced by the generated possibility correspondence.
% Three different beliefs below have a same, constant possibility correspondence
% (with pid 343 in escape_3/3) which maps the whole states [a,b,c] for each state.
?- cautious_generation_of_belief_of_0(B,[violate,XB2],[Pid,P,[D1,D2]]).
B = [ ([]->[]), ([c]->[c]), ([b]->[]), ([b, c]->[]), ([a]->[]), ([a, c]->[]), ([a|...]->[]), ([...|...]->[...|...])]
XB2 = hold
Pid = 343
P = [ (a->[a, b, c]), (b->[a, b, c]), (c->[a, b, c])]
D1 = [[[c], [c]]]
D2 = [[[c], []]] ;
B = [ ([]->[]), ([c]->[b]), ([b]->[]), ([b, c]->[]), ([a]->[]), ([a, c]->[]), ([a|...]->[]), ([...|...]->[...|...])]
XB2 = hold
Pid = 343
P = [ (a->[a, b, c]), (b->[a, b, c]), (c->[a, b, c])]
D1 = [[[c], [b]]]
D2 = [[[c], []]] ;
B = [ ([]->[]), ([c]->[b, c]), ([b]->[]), ([b, c]->[]), ([a]->[]), ([a, c]->[]), ([a|...]->[]), ([...|...]->[...|...])]
XB2 = hold
Pid = 343
P = [ (a->[a, b, c]), (b->[a, b, c]), (c->[a, b, c])]
D1 = [[[c], [b, c]]]
D2 = [[[c], []]]
Yes
?-
% an unrestricted experimentation where B2 may be violated.
% However, B[]=[] is enforced throughout the course of experiment.
?- cautious_generation_of_belief_of_0(B,[XB1,XB2],[Pid,P,D]).
B = [ ([]->[]), ([c]->[]), ([b]->[]), ([b, c]->[]), ([a]->[]), ([a, c]->[]), ([a|...]->[]), ([...|...]->[])]
XB1 = hold
XB2 = violate
Pid = 343
P = [ (a->[a, b, c]), (b->[a, b, c]), (c->[a, b, c])]
D = [[[[a, b, c], []]], [[[a, b, c], [a, b, c]]]]
Yes
% We may generate B1- or B2-violated beliefs and verify
% whether they represent some possibility correspondence or not.
% They would be detected as not_exsist cases as follows.
?- cautious_generation_of_belief_of_0(B,[XB1,XB2],not_exsist).
B = [ ([]->[]), ([c]->[]), ([b]->[]), ([b, c]->[c]), ([a]->[]), ([a, c]->[c]), ([a|...]->[c]), ([...|...]->[])]
XB1 = violate
XB2 = violate
Yes
?- display_goals(belief_of(1,_,_)).
belief_of(1, [], [])
belief_of(1, [c], [])
belief_of(1, [b], [])
belief_of(1, [b, c], [c])
belief_of(1, [a], [])
belief_of(1, [a, c], [c])
belief_of(1, [a, b], [c])
belief_of(1, [a, b, c], [])
Yes
?- display_goals(belief_of_1(1,_,_)).
belief_of_1(1, [], [])
belief_of_1(1, [c], [])
belief_of_1(1, [b], [])
belief_of_1(1, [b, c], [])
belief_of_1(1, [a], [c])
belief_of_1(1, [a, c], [c])
belief_of_1(1, [a, b], [c])
belief_of_1(1, [a, b, c], [a, b, c])
Yes
?-
% In these cases a generated belief operator is inconsistent
% in that the possibility correspondence it represents do not
% reproduce the original beliefs.
******************** end *****************************/
% ----------------------------------------------------------- %
% Verification of Therem 1 (Morris, 1994)
% belief represents possibility correspondence <--> B1 & B2
% ----------------------------------------------------------- %
verify_theorem_1(S,D):-
G1=(escape_2(verified,_Id,[_XB,XP]),XP=pc:[Pid,_Pos,_Dif]),
G2=(escape_3(verified,Pid,_X)),
verify_equality_of_goals(G1:Pid,G2:Pid,S,D).
/***************** demo ********************************
% a naive test for theorem 1 for three states
% ----------------------------------------------------------- %
% Generating beliefs in accordance both with axiom B1 and axiom B2.
% Further, B[]=[] and B[a,b,c]=[a,b,c] are enforced during the
% generation of beliefs.
% Note that
% the task is computationally easy in contrast with one for the
% if part where much more beliefs must be verified.
?- create_belief_of_0([[hold,hold],_],stop_id(_)).
complete
Yes
?-
% Generated examples of belief operator:
?- escape_2(verified,Id,[XB,XP]),XP=pc:[Pid,Pos,Dif].
Id = 1
XB = ax:[hold, hold]
XP = pc:[343, [ (a->[a, b, c]), (b->[a, b, c]), (c->[a, b|...])], [[], []]]
Pid = 343
Pos = [ (a->[a, b, c]), (b->[a, b, c]), (c->[a, b, c])]
Dif = [[], []] ;
Id = 2
XB = ax:[hold, hold]
XP = pc:[343, [ (a->[a, b, c]), (b->[a, b, c]), (c->[a, b|...])], [[], []]]
Pid = 343
Pos = [ (a->[a, b, c]), (b->[a, b, c]), (c->[a, b, c])]
Dif = [[], []]
Yes
?- escape_2(verified,_,[_,pc:[_,_,D]]),D\=[[],[]].
No
?-
% The result shows that all the generated beliefs which satisfies
% both axioms B1 and B2, XB=ax:[hold,hold]), represent
% some possibility correspondence has, for example,
% a possibility correspondence identified with Pid =343
% which is a constant map with the all states.
% Thus, each of these beliefs we generated is represent some
% possibility correspondence. This estabilishes the only-if
% part. Furthermore, the mapping is also onto.
?- verify_theorem_1(S,D).
S = [[343, 343, 339, 315, 311, 147, 143, 119|...], [1, 2, 3, 4, 5, 6, 7|...]]
D = [[], [final(tran=b3), final(refl=b4), final(eucl=b5)]]
Yes
?-
% Therefore, for any generated belief with B1 & B2, there is a
% possibility correpondence (in 'poss.txt') which is represented
% by the belief, i.e., it is a normal belief, and vice versa.
% The equivalence of normal beliefs and possibility correspondences
% has established. It is impossible that any other belief operator
% other than above verified, which must violate either B1 or B2,
% consistently represent a possibility correspondence. In other words,
% any violator ought to be absorbed into one of the normal beliefs.
% Caveat: This is partial verification of Theorem 1 because
% the possibility correspondence which map empty set at any state
% is not permitted to generate.
% Beliefs who represent such a map are detected as not-exsist cases
% in the latter part. In the above B1 and B2 obeying generation,
% there is no such anomal belief.
?- escape_2(verified,_Id,not_exsist).
No
% Of course, the original (syntactical) proof is easy to see.
******************** end *****************************/
/***************** demo ********************************
% Yet another test of Theorem 1 for three states:
% ----------------------------------------------------------- %
% Alternatively, if we want to establish that there is no belief
% which violates B1 or B2 can represent any possibility
% correpondence,
% it would be rather a computationally awkward to verify it.
% Because of the number of every possible belief operators.
% It amounts (2^#states)^(2^#states)= 8^8= 16,777,216.
% The if part test by generating beliefs which do satisy B2,
% by changing a term in assign_belief_of_0_for_each_event/2,
% about 370 lines above.
% (Sorry, this position may not be appropriate.)
% (E=S->C=S;true), % enforcing to obey the axiom B2
% %(E=S->C\=S;true). % leading to betray the axiom B2
% caution:the execution may consume your cpu time (it take a few hours).
?- cautious_generation_of_belief_of_0(B,[violate,XB2],[P,I,[[],[]]]).
No
?-
% Another if part test by generating beliefs which do not satisy B2.
% by changing a term in assign_belief_of_0_for_each_event/2
% %(E=S->C=S;true), % enforcing to obey the axiom B2
% (E=S->C\=S;true). % leading to betray the axiom B2
% caution:the execution may cunsume your cpu time (it take some hours).
?- cautious_generation_of_belief_of_0(B,[hold,XB2],[P,I,[[],[]]]).
No
?-
******************** end *****************************/
:- nl,tab(30),write(u^u),nl.
% ----------------------------------------------------------- %
% omake: a modeling of the syntactical proof for B1 of Theorem 1.
% ----------------------------------------------------------- %
% added: 10 Jan 2005
model_of_belief((
is_believed_at(S,J,E):-
event(E),possibility(J,S,P),subset(P,E)
)).
theorem_1((
(
C= (event(E),event(F),intersection(E,F,M)),
P= (is_believed_at(W,1,E),is_believed_at(W,1,F)),
Q= (is_believed_at(W,1,M))
),
forall(C,( (P->Q;write(violate(E,F,M))),( Q->P;write(violate(E,F,M)))))
)).
set_theory((
(
O=(event(X),event(Y),intersection(X,Y,Z)),
A=(subset(L,X),subset(X,Y)),
B=(subset(L,Z))
),
forall(O,(A->B, B->A))
)).
set_theory(special(1),
(
assert((a_condition(X,_P,_):- _)),
assert((subsetp(X,Y,Z):- a_condition(X,Y,Z), subset(X,Y)))
),
((
O=(event(X),event(Y),intersection(X,Y,Z)),
A=(subsetp(L,X),subsetp(X,Y)),
B=(subsetp(L,Z))
),
forall(O,(A->B, B->A))
)
).
theorem_1_proof(step(1),
(
assert((a_condition(X,P,[J,S]):-event(X),possibility(J,S,P))),
assert((subsetp(X,Y,Z):- a_condition(X,Y,Z), subset(X,Y)))
),
((
C= (event(E),event(F),intersection(E,F,M)),
P= (subsetp(P,E),subsetp(P,F)),
Q= (subsetp(P,M))
),
forall(C,( P->Q, Q->P))
)
).
/***************** demo ********************************
% alternative: directly verifying these axioms.
% axiom B2 (distribution)
?- P= (event(E),event(F),intersection(E,F,M),is_believed_at(W,1,M)),
Q= (is_believed_at(W,1,E),is_believed_at(W,1,F)),
forall(P,Q),
forall(Q,P).
******************** end *****************************/
:- display_all_lines( [
' loading other utilities.'
]).
%
% ----------------------------------------------------------- %
% Arithmetic and so on including probabilistic operators
% ----------------------------------------------------------- %
%
% sum
% ----------------------------------------------------------- %
sum([],0).
sum([X|Members],Sum):-
sum(Members,Sum1),
%number(X),
Sum is Sum1 + X.
%
% product
% ----------------------------------------------------------- %
product([],1).
product([X|Members],Z):-
product(Members,Z1),
%number(X),
Z is Z1 * X.
%
% weighted sum
% ----------------------------------------------------------- %
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.
% make combinatorial sequences
% ----------------------------------------------------------- %
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/3 : subset-enumeration
% ----------------------------------------------------------- %
subset_of(A,N,As):-
length(As,L),
length(D,L),
list_projection(D,As,B),
length(B,N),
sort(B,A).
% a sequence of binary choice for a list:
%--------------------------------------------------
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).
%
% ----------------------------------------------------------- %
% Utilities for file output and display
% ----------------------------------------------------------- %
%
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 tool
% ----------------------------------------------------------- %
%
% 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].
% example:
% replacing terms of findall/3 in possibility_via_preference/4.
test_1([Act1,Act2,W,X,Y,Z]):-
eventwise_binary_act(Act1, [W]->X; Z),
eventwise_binary_act(Act2, [W]->Y; Z).
test_2([Act1,Act2,W,X,Y,Z]):-
state(W),
complement([W],Complement),
composite_act(_,Act1,_),
composite_act(_,Act2,_),
member(([W]->X),Act1),
member(([W]->Y),Act2),
member((Complement->Z),Act1),
member((Complement->Z),Act2).
/***************** demo ********************************
?- verify_equality_of_goals(test_1(X):X,test_2(Y):Y,S,D).
X = _
Y = _
S = [[[[ ([a]->y), ([b, c]->x)], [ ([a]->y), ([b|...]->x)], a, y, y, x], [[ ([a]->y), ([b|...]->x)], [ ([a]->z), ([...|...]->x)], a, y, z|...], [[ ([a]->z), ([...|...]->x)], [ ([...]->y), (... ->...)], a, z|...], [[ ([...]->z), (... ->...)], [ (... ->...)|...], a|...], [[ (... ->...)|...], [...|...]|...], [[...|...]|...], [...|...]|...], [[[ ([a]->y), ([b|...]->x)], [ ([a]->y), ([...|...]->x)], a, y, y|...], [[ ([a]->y), ([...|...]->x)], [ ([...]->z), (... ->...)], a, y|...], [[ ([...]->z), (... ->...)], [ (... ->...)|...], a|...], [[ (... ->...)|...], [...|...]|...], [[...|...]|...], [...|...]|...]]
D = [[], []]
Yes
?-
******************** end *****************************/
:- display_all_lines( [
' ********** complete *********** '
]).
%end
return to front page.