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