You selected trivia01.pl
ttl(['Belief Revision and Minimal Change by Prolog:
','-------------------------------------------------------
','% file: trivia01.pl
','% date: 21-29 Mar 2005 (trivial.pl)
','% revised: 30-31, 1 Apr Mar 2005
','% language: SWI-Prolog (Version 5.0.9)
','% by: Kenryo INDO (Kanto Gakuen University)
']).
% the inconsisteny theorem ([1])
%---------------------------------------------------%
% The Ramsey test and the preservation criterion are
% inconsistent with each other unless the belief revision
% model is trivial.
% The theorem will be restated in 12.1.
% contents:
% Section 12 is the main section of this file.
contents([' contents:
','-------------------------------------------------------
',' 1. setup the model
',' 2. truth assignment for atomic propositions
',' 3. propositions of language
',' 3.1. Transforming propositions into the facts.
',' 4. truth function for propositions
',' 5. satisfiablity and models
',' 6. properties of proposition
',' 7. beliefs and belief sets
',' 8. generating beliefs
',' (without rationality consideration)
',' 9. model based logical consequence
',' 9.1 logical consequences: an alternative
',' 10. inquiring generated beliefs
',' 11. truncated closed beliefs
',' 12. belief revision model with conditionals
',' Appendix 1. State space
',' Appendix 2. common programs
','-------------------------------------------------------
',' jump: by search a word %~ (followed by 5. etc)
']).
ref([' references:
','-------------------------------------------------------
','% [1] P. G\"adenfors (1986).
','% Belief revisions and the Ramsey test for conditionals.
','% The Philosophical Review, XLV, No.1, pp.1-93.
','% [2] C.-L. Chang and R. C.-T. Lee (1973).
','% Symbolic Logic and Mechanical Theorem Proving.
','% Academic Press.
','% [3] C.E. Alchourr\'on, P. G\"ardenfors and D. Makinson (1985).
','% On the logic of theory change: partial meet contraction and revision fuctions.
','% The Journal of Symbolic Logic 50(2): 510-530.
']).
top_level_rules(['top level rules (cui)
','-------------------------------------------------------
','% set_model/0,2: => proposition_0/2,belief_0/4.
','% inquire_belief/2: => belief_set_0/2.
','% test_gen_rbs/0: => tmp_belief/2 (belief_0/4)
','% update_belief_set/2: tmp_belief/2=> belief_set_0/2
','% test_gen_mc/0: => tmp_revision/1
','% verify_mc(preservation): => tmp_preserving_mc/2
','% belief_revision/4:
','% minimal_change/4:
',' ex.,
',' belief_revision((K,L,E,H),a,(Ka,L1,F,G),[(D,A,K),Ldak]).
',' minimal_change((K,L,E,H),a,(Ka,L1,F,G),[DAK,Ldak]).
','% K: old belief set, Ka: revised set, A: proposition.
','% D: deleted, A: added, K: kept.
']).
/*************************************************
%~ 1. setup the system and the model
*************************************************/
% added: 23 Mar 2005
% revised: 29-31 Mar 2005 (using factualize_goals/1)
initialize_system:-
ttl(TTL),forall_write(TTL),
top_level_rules(TLR),forall_write(TLR),
conform_to_rebuild.
conform_to_rebuild:-
nl,write('initialize temporary data and do model setup ? >'),
read(Y),(member(Y,[y,'Y'])->!;fail),
abolish(tmp_belief/2),
abolish(tmp_revision/1),
abolish(tmp_preserving_mc/2),
default_model(ULS,APS),
set_model(ULS,APS,conform).
conform_to_rebuild.
:- dynamic atomic_propositions/1.
% the default
atomic_propositions(
% [a]
% [a,b]
[a,b,c]
% [a,b,c,d]
).
atomic_proposition(X):-
atomic_propositions(Y),
member(X,Y).
:- dynamic upper_limit_of_steps/1.
% the default
upper_limit_of_steps(1).
default_model(1,[a,b,c]).
set_model:-
nl,write('input(upper_limit_of_steps):'),
read(ULS),
nl,write('input(atomic_propositions):'),
read(APS),
set_model(ULS,APS),
display_model.
% setup script for belief models (revised: 31 Mar 2005)
set_model(ULS,APS):-
set_model(_,ULS,APS,no).
set_model(ULS,APS,Conform):-
set_model_1(_,ULS,APS),
set_model_2(_),
set_model_3(_,Conform),
display_model.
set_model_1(preliminary,ULS,APS):-
default_model(ULSd,APSd),
(var(ULS)->ULS=ULSd;true),
(var(APSd)->APS=APSd;true),
abolish(upper_limit_of_steps/1),
abolish(atomic_propositions/1),
abolish(tmp_belief/2), % (revised: 29 Mar 2005)
assert(upper_limit_of_steps(ULS)),
assert(atomic_propositions(APS)).
set_model_2(compile_propositions):-
nl,
write([factualize_propositions/0]:'compiling..'),
factualize_propositions.
%factualize_truth_evaluations.
set_model_3(compile_beliefs,no):-
test_gen_rbs,
write('complete').
set_model_3(compile_beliefs,conform):-
G=test_gen_rbs,
Mes='(without compiling) ',
nl,
write([G/0]:'start compiling beliefs ...'),
nl,
(
(write('sure ? (y.)>'),read(y))
-> (G,write('complete'))
; (write(Mes))
).
/*************************************************
%~ 2. truth assignment for atomic propositions
*************************************************/
% 21-23 Mar 2005
% a tuple of truth assignment for atomic propositions
% will be called an `interpretation' to a given propositional fomula
% (or a possible state of world). (See [2], p.9)
truth_assignment_0([],[],[]).
truth_assignment_0([X|A],[P|B],[(X,P)|C]):-
atomic_proposition(X),
member(P,[+,-]),
truth_assignment_0(A,B,C).
truth_assignment(A,B,C):-
atomic_propositions(A),
truth_assignment_0(A,B,C).
/*
%%% demo %%%
% atomic_propositions([a,b,c]).
?- truth_assignment(A,B,C).
A = [a, b, c]
B = [+, +, +]
C = [ (a, +), (b, +), (c, +)]
Yes
?- truth_assignment(A,B,C),nl,write(C),fail.
[ (a, +), (b, +), (c, +)]
[ (a, +), (b, +), (c, -)]
[ (a, +), (b, -), (c, +)]
[ (a, +), (b, -), (c, -)]
[ (a, -), (b, +), (c, +)]
[ (a, -), (b, +), (c, -)]
[ (a, -), (b, -), (c, +)]
[ (a, -), (b, -), (c, -)]
No
?-
*/
/*************************************************
%~ 3. propositions of language
*************************************************/
% 21-23 Mar 2005
% 30 Mar 2005 (proposition/2 to be the default hierarchy)
% the default hierarchy of proposition/2.
% proposition_0/2 can be utilized after an execution of set_mode/2, 0.
proposition(P,L):-
clause(proposition_0(P,L),true).
proposition(P,L):-
\+ clause(proposition_0(_,_),true),
proposition_1(P,L).
% the language:
% is a language in order to express the relevant
% propositions, (or propositional formula in , )
% including truth-functional connectives.
% The connectives (or `operators' interchangeably)
% are - (not), & (and), v (or),
% -> (material implication) and a propositional
% constant _|_ (the absurd proposition), as well as
% a conditional connective >.
% Instead, we will use an empty list [] to represent
% the absurd proposition, because Prolog syntax does
% not allow _|_ as a constant symbol,
% which must be a variable.
% proposition_1/2 (was: proposition/2)
proposition_1(o,[]). %absurd proposition
proposition_1(X,[]):- atomic_proposition(X).
proposition_1((-,X),[-|R]):-
allowable_composition(([-|R],[],R),(_,0,_)),
proposition_1(X,R).
proposition_1((X,Op,Y),[Op|L]):-
member(Op,[&,v,->]),
% (->) is a material implication
allowable_composition(([Op|L],Lx,Ly),_),
proposition_1(X,Lx),
proposition_1(Y,Ly).
proposition_1((X,>,Y),[>|L]):-
allowable_composition(([>|L],Lx,Ly),_),
proposition_1(X,Lx),
proposition_1(Y,Ly).
%%% The above (>) means a conditional connective.
% However, this is only an appearance.
% The legitimate meaning of conditional connective
% will be modeled by the Ramsey test and other postulates.
allowable_composition((L,Lx,Ly),(N,Nx,Ny)):-
allowable_number_of_steps(N,_,_K),
N1 is N -1,
allowable_number_of_steps(Nx,N1,Ny),
length(L,N),
length(Lx,Nx),
length(Ly,Ny),
append([_Op|Lx],Ly,L).
allowable_number_of_steps(J,N,Remains):-
(var(N)->upper_limit_of_steps(N);integer(N)),
inductive_numbers([N|R]),
member(K,[N|R]),
J is N -K,
Remains is K.
% default:
% upper_limit_of_steps(1).
% atomic_propositions([a,b,c]).
all_propositions(L):-
findall(P,proposition(P,_),L).
/*
%%% demo %%%
% upper_limit_of_steps(1).
% atomic_propositions([a]).
?- proposition(X,A),nl,write(A;X),fail.
[];o
[];a
[-];-, o
[-];-, a
[&];o, &, o
[&];o, &, a
[&];a, &, o
[&];a, &, a
[v];o, v, o
[v];o, v, a
[v];a, v, o
[v];a, v, a
[ (->)];o, (->), o
[ (->)];o, (->), a
[ (->)];a, (->), o
[ (->)];a, (->), a
[>];o, >, o
[>];o, >, a
[>];a, >, o
[>];a, >, a
No
?-
*/
%---------------------------------------------------
%~ 3.1. Transforming propositions into the facts.
%---------------------------------------------------
:- dynamic proposition_0/2.
factualize_propositions:-
abolish(proposition_0/2),
factualize_goals([proposition_1(_,_)]),
forall(
retract(temp_goal(_,proposition_1(P,L),_)),
assert(proposition_0(P,L))
),
nl, write('All the generated data have replaced by proposition_0/2.').
:- dynamic truth_evaluation_0/4.
factualize_truth_evaluations:-
abolish(truth_evaluation_0/4),
factualize_goals([truth_evaluation_1(_,_,_,_)]),
forall(
retract(temp_goal(_,truth_evaluation_1(P,L,C,T),_)),
assert(truth_evaluation_0(P,L,C,T))
),
nl, write('All generated data have replaced by truth_evaluation_0/4.').
display_model:-
upper_limit_of_steps(ULS),
atomic_propositions(APS),
nl,write(upper_limit_of_steps:ULS),
nl,write(atomic_propositions:APS).
/*************************************************
%~ 4. truth function for propositions
*************************************************/
% 21-23 Mar 2005
% 30 Mar 2005 (truth_evaluation/2 to be the default hierarchy)
% the default hierarchy
% can be utilized after an execution of set_mode/2, 0.
truth_evaluation(P,L,C,T):-
clause(truth_evaluation_0(P,L,C,T),true).
truth_evaluation(P,L,C,T):-
\+ clause(truth_evaluation_0(_,_,_,_),true),
truth_evaluation_1(P,L,C,T).
% truth_evaluation_1/4 (was: truth_evaluation/4)
truth_evaluation_1(X,[],C,T):-
proposition(X,[]),
truth_assignment(_,_,C),
member((X,T),[(o,-)|C]).
truth_evaluation_1((-,X),L,C,NT):-
proposition((-,X),L),
%(X\=(-,-,_)->true;!),
truth_evaluation_1(X,_R,C,T),
member((NT,T),[(+,-),(-,+)]).
truth_evaluation_1((X,Op,Y),L,C,T):-
proposition((X,Op,Y),L),
truth_evaluation_1(X,_,C,Tx),
%(X\=(X,Op,Y)->true;!),
truth_evaluation_1(Y,_,C,Ty),
%(Y\=(X,Op,Y)->true;!),
truth_pattern_for_binary(Op,Tx,Ty,T).
truth_pattern_for_binary(&,Tx,Ty,T):-
member(-,[Tx,Ty]),!,T='-'.
truth_pattern_for_binary(v,Tx,Ty,T):-
(Tx,Ty)=(-,-),!,T='-'.
truth_pattern_for_binary((->),Tx,Ty,T):-
(Tx,Ty)=(+,-),!,T='-'.
% a meaning of conditional, for convenience.
truth_pattern_for_binary(>,Tx,Ty,T):-
member((Tx,Ty),[(+,-),(-,-)]),!,T='-'.
truth_pattern_for_binary(_,_,_,+).
/*
%%% demo %%%
?- set_model(1,[a]).
complete
total:20 successful goals have asserted as temp_goal/3.
All generated data have replaced by proposition_0/2.
Yes
?- display_model.
upper_limit_of_steps:1
atomic_propositions:[a]
Yes
?- proposition(X,A),nl,write(A;X),fail.
[];o
[];a
[-];-, o
[-];-, a
[&];o, &, o
[&];o, &, a
[&];a, &, o
[&];a, &, a
[v];o, v, o
[v];o, v, a
[v];a, v, o
[v];a, v, a
[ (->)];o, (->), o
[ (->)];o, (->), a
[ (->)];a, (->), o
[ (->)];a, (->), a
[>];o, >, o
[>];o, >, a
[>];a, >, o
[>];a, >, a
No
?-
*/
/*************************************************
%~ 5. satisfiablity and models
*************************************************/
% 22-23 Mar 2005
% We will assume (|=, C, X) as a relation that
% a proposition X is satisifiable under an interpretation C,
% or C satisfies X in short.
% An interpretation C is also called a `model' of the proposition X
% when C satisfies X. (In modal logic, a possible state of world.
% In words, a set of such state gives the propositions it supports.)
% We regard |= at every state the counterpart of |-
% which satisfies the deduction theorem as assumed
% in the literature ([1], p.83).
is_a_model((A,B,C),(T,P,L)):-
truth_evaluation(P,L,C,T),
truth_assignment(A,B,C).
/*
%%% demo %%%
?- set_model(1,[a]),display_model.
complete
total:20 successful goals have asserted as temp_goal/3.
All generated data have replaced by proposition_0/2.
upper_limit_of_steps:1
atomic_propositions:[a]
Yes
?- is_a_model((_,_,M),(T,P,Q)),M=[(a,+)],
nl,write(M|=([T]:P)),fail.
[ (a, +)]|=([-]:o)
[ (a, +)]|=([+]:a)
[ (a, +)]|=([+]: (-, o))
[ (a, +)]|=([-]: (-, a))
[ (a, +)]|=([-]: (o, &, o))
[ (a, +)]|=([-]: (o, &, a))
[ (a, +)]|=([-]: (a, &, o))
[ (a, +)]|=([+]: (a, &, a))
[ (a, +)]|=([-]: (o, v, o))
[ (a, +)]|=([+]: (o, v, a))
[ (a, +)]|=([+]: (a, v, o))
[ (a, +)]|=([+]: (a, v, a))
[ (a, +)]|=([+]: (o, (->), o))
[ (a, +)]|=([+]: (o, (->), a))
[ (a, +)]|=([-]: (a, (->), o))
[ (a, +)]|=([+]: (a, (->), a))
[ (a, +)]|=([-]: (o, >, o))
[ (a, +)]|=([+]: (o, >, a))
[ (a, +)]|=([-]: (a, >, o))
[ (a, +)]|=([+]: (a, >, a))
No
?-
*/
% to display (satisfiable) propositions in a model
% classified by operators.
% added: 25 Mar 2005.
display_models((A,B,C),(T,P,L)):-
init_tmp_display_models,
is_a_model((A,B,C),(T,P,L)),
display_by_connectives(P,L),
fail.
:- dynamic tmp_display_model/1.
update_tmp_display_models(L):-
abolish(tmp_display_models/1),
assert(tmp_display_models(L)),
!.
init_tmp_display_models:-
update_tmp_display_models(0).
display_by_connectives(P,L):-
(tmp_display_models(L)->true
;(
nl,write(patterns(L)),nl,
update_tmp_display_models(L)
)
),
write([P]).
/*
%%% demo %%%
?- set_model(1,[a,b,c]),display_model.
complete
total:72 successful goals have asserted as temp_goal/3.
All generated data have replaced by proposition_0/2.
upper_limit_of_steps:1
atomic_propositions:[a, b, c]
Yes
?- display_models((_,[+,+,+],_),(+,P,L)).
patterns([])
[a][b][c]
patterns([-])
[ (-, o)]
patterns([&])
[ (a, &, a)][ (a, &, b)][ (a, &, c)][ (b, &, a)][ (b, &, b)][ (b, &, c)][ (c, &, a)][ (c, &, b)][ (c, &, c)]
patterns([v])
[ (o, v, a)][ (o, v, b)][ (o, v, c)][ (a, v, o)][ (a, v, a)][ (a, v, b)][ (a, v, c)][ (b, v, o)][ (b, v, a)][ (b, v, b)][ (b, v, c)][ (c, v, o)][ (c, v, a)][ (c, v, b)][ (c, v, c)]
patterns([ (->)])
[ (o, (->), o)][ (o, (->), a)][ (o, (->), b)][ (o, (->), c)][ (a, (->), a)][ (a, (->), b)][ (a, (->), c)][ (b, (->), a)][ (b, (->), b)][ (b, (->), c)][ (c, (->), a)][ (c, (->), b)][ (c, (->), c)]
patterns([>])
[ (o, >, a)][ (o, >, b)][ (o, >, c)][ (a, >, a)][ (a, >, b)][ (a, >, c)][ (b, >, a)][ (b, >, b)][ (b, >, c)][ (c, >, a)][ (c, >, b)][ (c, >, c)]
No
?- set_model(2,[a,b,c]),display_model.
complete
total:2316 successful goals have asserted as temp_goal/3.
All generated data have replaced by proposition_0/2.
upper_limit_of_steps:2
atomic_propositions:[a, b, c]
Yes
?- display_models((_,[+,+,+],_),(+,P,[v,-])).
patterns([v, -])
[ (o, v, -, o)]
[ (a, v, -, o)][ (a, v, -, a)][ (a, v, -, b)][ (a, v, -, c)]
[ (b, v, -, o)][ (b, v, -, a)][ (b, v, -, b)][ (b, v, -, c)]
[ (c, v, -, o)][ (c, v, -, a)][ (c, v, -, b)][ (c, v, -, c)]
[ ((-, o), v, o)][ ((-, o), v, a)][ ((-, o), v, b)][ ((-, o), v, c)]
[ ((-, a), v, a)][ ((-, a), v, b)][ ((-, a), v, c)]
[ ((-, b), v, a)][ ((-, b), v, b)][ ((-, b), v, c)]
[ ((-, c), v, a)][ ((-, c), v, b)][ ((-, c), v, c)]
No
?-
*/
/*************************************************
%~ 6. properties of proposition
*************************************************/
% 22-23 Mar 2005
% revised: 25 Mar 2005 (connectives in the 2nd argument)
is_valid(A):-
is_valid(A,_).
is_valid(A,L):-
proposition(A,L),
\+ (
is_a_model((_,_,_),(-,A,_));
is_a_model((_,_,_),(+,(-,A),_))
).
is_invalid(A):-
is_invalid(A,_).
is_invalid(A,L):-
proposition(A,L),
\+ is_valid(A).
is_inconsistent(A):-
is_inconsistent(A,_).
is_inconsistent(A,L):-
proposition(A,L),
\+ is_a_model((_,_,_),(+,A,_)).
% the synonym
is_unsatisfiable(A):-
is_inconsistent(A).
is_unsatisfiable(A):-
is_inconsistent(A,_).
is_consistent(A):-
is_consistent(A,_).
is_consistent(A,L):-
proposition(A,L),
\+ is_inconsistent(A).
% the synonym
is_satisfiable(A):-
is_consistent(A).
is_satisfiable(A):-
is_consistent(A,_).
is_disjoint(A,B):-
proposition((A, &, B),_),
is_inconsistent((A, &, B)).
/*
%%% demo %%%
% upper_limit_of_steps(1).
% atomic_propositions([a,b,c]).
?- is_valid(A),nl,write(A),fail.
-, o
o, (->), o
o, (->), a
o, (->), b
o, (->), c
a, (->), a
b, (->), b
c, (->), c
No
?- is_inconsistent(A),nl,write(A),fail.
o
o, &, o
o, &, a
o, &, b
o, &, c
a, &, o
b, &, o
c, &, o
o, v, o
o, >, o
a, >, o
b, >, o
c, >, o
No
?-
% upper_limit_of_steps(2).
% atomic_propositions([a,b,c]).
?- is_inconsistent(P,L),L=[-,->],
display_by_connectives(P,L),fail.
patterns([-, (->)])
[ (-, o, (->), o)][ (-, o, (->), a)][ (-, o, (->), b)]
[ (-, o, (->), c)][ (-, a, (->), a)][ (-, b, (->), b)]
[ (-, c, (->), c)]
No
?-
?- is_disjoint(A,B).
A = o
B = o ;
A = o
B = a ;
A = o
B = b ;
A = a
B = o ;
A = b
B = o ;
A = o
B = -, o ;
...
?-
*/
/*************************************************
%~ 7. beliefs and belief sets
*************************************************/
% 21-23 Mar 2005
% revised: 24 Mar 2005 (dealed with belief_0/4)
% revised: 29 Mar 2005 (priority of belief_set_0/2)
% state of belief, and belief set:
%---------------------------------------------------
% The only epistemic sttitude that will be concern is
% whether a proposition is accepted or not accepted.
% And Gardenfors [1] called `belief set' (denoted by K)
% as a set (of belifs which consists)
% of propositions that are accepted in the state.
% (See [1], p.83)
% belief/2 represents that a state of belief, i.e.,
% the accepted (+) or rejected (-) propositions
% in that state.
belief(T,X):-
clause(belief_0(T,X,_,_),true).
belief(T,X):-
\+ clause(belief_0(_,_,_,_),true),
belief_set(T,K),
member(X,K).
belief_set(T,K):-
\+ clause(belief_0(_,_,_,_),true),
belief_set_0(T,K).
belief_set(T,K):-
clause(belief_0(_,_,_,_),true),
!,
findall((T,P),belief_0(T,P,_,_),K1),
setof(P,member((T,P),K1),K).
:- dynamic belief_set_0/2.
% default belief set.
belief_set_0(+,[
a,
(a, &, a),
(a, v, a),
(a, (->), a)
]).
belief_set_0(-,[
[]
]).
%%% Note %%%
% belief_set_0/2 is removed/asserted/updated by
% initialize_system,
% generate_belief_set/3,
% and update_belief_set/2.
% While beliefs_0/4 is removed/asserted/updated by
% generate_rational_belief_set/3,
% and test_gen_rbs/0,3.
/*
%%% demo %%%
?- belief_set(+,K).
K = [a, (a, &, a), (a, v, a), (a, (->), a)]
Yes
*/
/*************************************************
%~ 8. generating beliefs
% (without rationality consideration)
*************************************************/
% 23 Mar 2005
% revised: 25 Mar 2005 (reexamination)
% revised: 31 Mar 2005 (priority of belief_set_0/2 against belief_0/4)
% without commitment
generate_belief_set(A,X,N,O):-
var(A),
all_propositions(O),
length(O,L),
choose_N_units_among(L,N,X),
list_projection(X,O,A).
generate_belief_set(A,X,N,O):-
\+ var(A),
all_propositions(O),
list_projection(X,O,A),
length(A,N).
% commitment
generate_belief_set(A,X,N,O,commit):-
generate_belief_set(A,X,N,O),
abolish(belief_0/4), % (revised: 31 Mar 2005)
abolish(belief_set_0/2),
assert(belief_set_0(+,A)).
/*
%%% demo %%%
?- set_model(2,[a,b]),display_model.
complete
total:1017 successful goals have asserted as temp_goal/3.
All generated data have replaced by proposition_0/2.
upper_limit_of_steps:2
atomic_propositions:[a, b]
Yes
?- generate_belief_set(A,X,N,O).
A = [o, a, b, c, (-, o), (-, a), (-, b), (-, c), (..., ...)|...]
X = [1, 1, 1, 1, 1, 1, 1, 1, 1|...]
N = 1017
O = [o, a, b, c, (-, o), (-, a), (-, b), (-, c), (..., ...)|...]
Yes
?- generate_belief_set(A,X,3,O).
A = [o, a, b]
X = [1, 1, 1, 0, 0, 0, 0, 0, 0|...]
O = [o, a, b, (-, o), (-, a), (-, b), (-, -, o), (-, ..., ...), (..., ...)|...]
Yes
?- belief_set(P,A).
P = +
A = [a, b, c, (-, o), (-, -, a), (-, -, b), (-, -, c), (-, ..., ...), (..., ...)|...]
No
?-
*/
/*************************************************
%~ 9. model based logical consequence
*************************************************/
% 24-25,27 Mar 2005
% revised: 30 Mar 2005 (a generalization by adding truth_functional_models/4)
truth_functional_models(T,A,M,X):-
member((X,Y),[
(1,(C,_,_)),(2,(_,C,_)),(3,(_,_,C))
]),
proposition(A,_),
findall(C,
is_a_model(Y,(T,A,_)),
M).
truth_functional_models(T,A,M):-
truth_functional_models(T,A,M,3).
truth_functional_totology(A,B,M):-
truth_functional_models(_,A,M),
truth_functional_models(_,B,M).
% the inverse of truth_functional_models/3.
propositions_satisfiable_by_model(T,Q,M):-
truth_assignment(A,B,C),
M=(A,B,C),
findall((Prop,Ops),
is_a_model(M,(T,Prop,Ops)),
Q).
/*
%%% demo %%%
?- set_model(1,[a,b,c]),display_model.
complete
total:72 successful goals have asserted as temp_goal/3.
All generated data have replaced by proposition_0/2.
upper_limit_of_steps:1
atomic_propositions:[a, b, c]
Yes
?- generate_belief_set(A,X,N,O,commit),\+ member(o,A).
A = [a, b, c, (-, o), (-, a), (-, b), (-, c), (o, ..., ...), (..., ...)|...]
X = [0, 1, 1, 1, 1, 1, 1, 1, 1|...]
N = 71
O = [o, a, b, c, (-, o), (-, a), (-, b), (-, c), (..., ...)|...]
Yes
?- forall(belief(+,B),write([B])).
[a][b][c][ (-, o)][ (-, a)][ (-, b)][ (-, c)]
[ (o, &, o)][ (o, &, a)][ (o, &, b)][ (o, &, c)]
[ (a, &, o)][ (a, &, a)][ (a, &, b)][ (a, &, c)]
[ (b, &, o)][ (b, &, a)][ (b, &, b)][ (b, &, c)]
[ (c, &, o)][ (c, &, a)][ (c, &, b)][ (c, &, c)]
[ (o, v, o)][ (o, v, a)][ (o, v, b)][ (o, v, c)]
[ (a, v, o)][ (a, v, a)][ (a, v, b)][ (a, v, c)]
[ (b, v, o)][ (b, v, a)][ (b, v, b)][ (b, v, c)]
[ (c, v, o)][ (c, v, a)][ (c, v, b)][ (c, v, c)]
[ (o, (->), o)][ (o, (->), a)][ (o, (->), b)][ (o, (->), c)]
[ (a, (->), o)][ (a, (->), a)][ (a, (->), b)][ (a, (->), c)]
[ (b, (->), o)][ (b, (->), a)][ (b, (->), b)][ (b, (->), c)]
[ (c, (->), o)][ (c, (->), a)][ (c, (->), b)][ (c, (->), c)]
[ (o, >, o)][ (o, >, a)][ (o, >, b)][ (o, >, c)]
[ (a, >, o)][ (a, >, a)][ (a, >, b)][ (a, >, c)]
[ (b, >, o)][ (b, >, a)][ (b, >, b)][ (b, >, c)]
[ (c, >, o)][ (c, >, a)][ (c, >, b)][ (c, >, c)]
B = _G158
?- propositions_satisfiable_by_model(+,Q,(_,[+,+,+],_)),
forall(member((X,_),Q),(write([X]))).
[a][b][c][ (-, o)]
[ (a, &, a)][ (a, &, b)][ (a, &, c)]
[ (b, &, a)][ (b, &, b)][ (b, &, c)]
[ (c, &, a)][ (c, &, b)][ (c, &, c)]
[ (o, v, a)][ (o, v, b)][ (o, v, c)]
[ (a, v, o)][ (a, v, a)][ (a, v, b)]
[ (a, v, c)][ (b, v, o)][ (b, v, a)]
[ (b, v, b)][ (b, v, c)][ (c, v, o)]
[ (c, v, a)][ (c, v, b)][ (c, v, c)]
[ (o, (->), o)][ (o, (->), a)][ (o, (->), b)][ (o, (->), c)]
[ (a, (->), a)][ (a, (->), b)][ (a, (->), c)]
[ (b, (->), a)][ (b, (->), b)][ (b, (->), c)]
[ (c, (->), a)][ (c, (->), b)][ (c, (->), c)]
[ (o, >, a)][ (o, >, b)][ (o, >, c)]
[ (a, >, a)][ (a, >, b)][ (a, >, c)]
[ (b, >, a)][ (b, >, b)][ (b, >, c)]
[ (c, >, a)][ (c, >, b)][ (c, >, c)]
Q = [ (a, []), (b, []), (c, []), ((-, o), [-]), ((a, &, a), [&]), ((a, &, b), [&]), ((a, ..., ...), [&]), ((..., ...), [...]), (..., ...)|...]
X = _G173
Yes
?- propositions_satisfiable_by_model(+,Q,(_,[+,+,+],_)),
length(Q,L),nl,write(L),
belief(+,P),\+ member((P,_),Q),nl,write(P),fail.
53
-, a
-, b
-, c
o, &, o
o, &, a
o, &, b
o, &, c
a, &, o
b, &, o
c, &, o
o, v, o
a, (->), o
b, (->), o
c, (->), o
o, >, o
a, >, o
b, >, o
c, >, o
No
?-
*/
% logical consequences and totologies
% by comparing model sets using the truth-function based code below.
%---------------------------------------------------
% Definition.
% A is a logical consequence of a proposition B iff
% the models of A (i.e., states of world
% where proposition A holds)
% subsumes that of B.
% Note: Generally,
% A is a logical consequence of a set of proposition B_1, B_2, ..., B_n iff
% -A & B_1 & ... & B_n is unsatisfiable. (See [2], p.17, Theorem 2.2)
is_a_logical_consequence(A->B):-
is_a_logical_consequence(A->B,[open,_,_]).
is_a_logical_consequence(A->B,[Closed,M,M1]):-
truth_functional_models(+,A,M),
truth_functional_models(+,B,M1),
subset(M,M1),
(Closed=open->true;proposition((A,->,B),_)).
% a set construction of logically_imply/3 (added: 30 Mar 2005.)
logically_imply([],O,P):-
is_valid(P),
all_states(O).
logically_imply([P|K],M,Q):-
logically_imply(K,MK,(-,o)),
truth_functional_models(+,P,MP,2),
truth_functional_models(+,Q,MQ,2),
intersection(MK,MP,M),
subset(M,MQ).
/*
%%% demo %%%
?- set_model(1,[a,b,c]).
complete
total:72 successful goals have asserted as temp_goal/3.
All generated data have replaced by proposition_0/2.
Yes
?- is_a_logical_consequence(a->A).
A = a ;
A = -, o ;
A = a, &, a ;
A = o, v, a ;
A = a, v, o ;
A = a, v, a ;
A = a, v, b
Yes
?- logically_imply([a,b],B,C),
\+ logically_imply([a],_,C).
B = [[+, +, +], [+, +, -]]
C = b ;
B = [[+, +, +], [+, +, -]]
C = a, &, b ;
B = [[+, +, +], [+, +, -]]
C = b, &, a
Yes
?- logically_imply([a],B,C),
\+ logically_imply([],_,C).
B = [[+, +, +], [+, +, -], [+, -, +], [+, -, -]]
C = a ;
B = [[+, +, +], [+, +, -], [+, -, +], [+, -, -]]
C = a, &, a ;
B = [[+, +, +], [+, +, -], [+, -, +], [+, -, -]]
C = o, v, a
Yes
?- logically_imply([a,b,c],B,C),
\+ logically_imply([a,b],_,C).
B = [[+, +, +]]
C = c ;
B = [[+, +, +]]
C = a, &, c ;
B = [[+, +, +]]
C = b, &, c
Yes
?-
*/
%---------------------------------------------------
%~ 9.1 logical consequences: an alternative
%---------------------------------------------------
% 21-23,27 Mar 2005
is_a_logical_consequence_1(A->B):-
is_valid((A,->,B)).
is_a_totology_1(A,B):-
is_a_logical_consequence_1(A->B),
is_a_logical_consequence_1(B->A).
% The above codes is an alternative to
% is_a_logical_consequence/1,2 which
% uses truth_functional_models/3.
% But we wil not use this to verify the
% closedness of generated (rational)
% belief set because of the limit of connectives.
% The equivalence of the two alternative codes
% is held only if `closed'
% is specified as the top of list in the second
% argument of is_a_logical_consequence/2.
/*
%%% demo %%%
?- set_model(1,[a,b,c]).
complete
total:72 successful goals have asserted as temp_goal/3.
All generated data have replaced by proposition_0/2.
Yes
?- is_a_totology_1(A,B),write([A=B]),fail.
[o=o][a=a][b=b][c=c]
No
?- is_a_logical_consequence_1(A),write([A]),fail.
[ (o->o)][ (o->a)][ (o->b)][ (o->c)][ (a->a)][ (b->b)][ (c->c)]
No
?- G1=is_a_logical_consequence_1(A),
G2=is_a_logical_consequence(B,[closed,_,_]),
verify_equality_of_goals(G1:A,G2:B,S,[D,D1]).
G1 = is_a_logical_consequence_1(_G157)
A = _G157
G2 = is_a_logical_consequence(_G171, [closed, _G165, _G168])
B = _G171
S = [[ (o->o), (o->a), (o->b), (o->c), (a->a), (b->b), (c->c)], [ (o->o), (o->a), (o->b), (o->c), (a->a), (b->b), (... ->...)]]
D = []
D1 = []
Yes
?-
*/
/*************************************************
%~ 10. inquiring generated beliefs
*************************************************/
% 27 Mar 2005
% revised: 31 Mar 2005 (model based)
is_absurd_belief_set(K):-
all_propositions(K).
is_aparently_contradicted_in_beliefs(A,K):-
belief_set(+,K),
belief(+,A),
belief(+,(-,A)),
!.
is_aparently_contradicted_in_beliefs(A,K):-
\+ var(K),
forall(member(X,K),proposition(X,_)),
member(A,K),
member((-,A),K),
!.
is_inconsistent_against_belief_set(A,K):-
belief_set(+,K),
is_aparently_contradicted_in_beliefs(A,K).
is_consistent_with_belief_set(A,K):-
belief_set(+,K),
proposition(A,_),
\+ is_inconsistent_against_belief_set(A,K).
% the notion of consistency above is week.
% unsatisfiabilities are not used:
is_unsatisfiable_against_belief_set(A,K):-
belief_set(+,K),
proposition(A,_),
logically_imply([A|K],[],(-,o)).
is_unsatisfiable_belief_set(K):-
belief_set(+,K),
logically_imply(K,[],(-,o)).
is_consistent_belief_set(K,Y):-
belief_set(+,K),
(
is_inconsistent_against_belief_set(_A,K)
->Y=no;Y=yes
),
!.
is_consistent_belief_set(K):-
is_consistent_belief_set(K,yes).
is_non_trivial_belief_model([A,B,C]):-
belief_set(+,K),
is_non_trivial_belief_model([A,B,C],K),
!.
is_non_trivial_belief_model(trivial).
is_non_trivial_belief_model([A,B,C],K):-
(var(K)->belief_set(+,K);true),
is_disjoint(A,B),
is_consistent_with_belief_set(A,K),
is_consistent_with_belief_set(B,K),
is_disjoint(C,B),
is_consistent_with_belief_set(C,K),
is_disjoint(C,A).
inquire_belief((NTP,Y),Kxno):-
Kxno=(K,X,N,O),
generate_belief_set(K,X,N,O,commit),
is_consistent_belief_set(K,Y),
is_non_trivial_belief_model(NTP).
/*
?- generate_belief_set(K,X,N,O,commit),
is_consistent_belief_set(K,Y),hexa_list(X,_,B),concat_list(H,B),
(is_non_trivial_belief_model(NTP)->true;NTP=fail).
K = [o, a, b, c, (-, o), (-, a), (-, b), (-, c), (..., ...)|...]
X = [1, 1, 1, 1, 1, 1, 1, 1, 1|...]
N = 72
O = [o, a, b, c, (-, o), (-, a), (-, b), (-, c), (..., ...)|...]
Y = no
B = [f, f, f, f, f, f, f, f, f|...]
H = ffffffffffffffffff
NTP = trivial ;
K = [o, a, b, c, (-, o), (-, a), (-, b), (-, c), (..., ...)|...]
X = [1, 1, 1, 1, 1, 1, 1, 1, 1|...]
N = 71
O = [o, a, b, c, (-, o), (-, a), (-, b), (-, c), (..., ...)|...]
Y = no
B = [f, f, f, f, f, f, f, f, f|...]
H = fffffffffffffffffe
NTP = trivial
Yes
?- generate_belief_set(K,X,N,O,commit),
hexa_list(X,_,B),concat_list(H,B),
is_non_trivial_belief_model(NTP),NTP\=trivial.
K = [o, a, b, c, (-, a), (-, b), (-, c), (o, ..., ...), (..., ...)|...]
X = [1, 1, 1, 1, 0, 1, 1, 1, 1|...]
N = 71
O = [o, a, b, c, (-, o), (-, a), (-, b), (-, c), (..., ...)|...]
B = [f, 7, f, f, f, f, f, f, f|...]
H = f7ffffffffffffffff
NTP = [o, o, o] ;
K = [a, b, c, (-, o), (-, a), (-, b), (-, c), (o, ..., ...), (..., ...)|...]
X = [0, 1, 1, 1, 1, 1, 1, 1, 1|...]
N = 71
O = [o, a, b, c, (-, o), (-, a), (-, b), (-, c), (..., ...)|...]
B = [7, f, f, f, f, f, f, f, f|...]
H = '7fffffffffffffffff'
NTP = [o, o, o]
Yes
?- inquire_belief((NTP,Consistency),(K,_,1,_)).
NTP = [o, o, o]
Consistency = yes
K = [o] ;
NTP = [o, o, o]
Consistency = yes
K = [a] ;
NTP = [o, o, o]
Consistency = yes
K = [b]
Yes
?-
*/
/*************************************************
%~ 11. truncated closed beliefs under LCs
*************************************************/
% 24-25, 28-29 Mar 2005
% revised: 30 Mar 2005.
% The rationality criteria on belief sets
%---------------------------------------------------%
% (rational) belief sets will be assumed to
% (i) include all all truth-functional totologies,
% (ii) be closed under logical consequences
% (See [1], p.83)
% We will give a script to generate and test
% (approximatedly) rational belief sets closed under
% logical consequence but with a truncation rule
% by the limit of the number of connectives
% used in a proposition.
:- dynamic belief_0/4.
:- dynamic current_state_of_beliefs/1.
% We will utilize state-event modeling to represent
% the state of beliefs.
% (See the state space section below.)
is_a_state_of_beliefs(E,X,Hx):-
hexa_event(E,X,Hx).
make_a_state_of_beliefs(E,X,Hx):-
is_a_state_of_beliefs(E,X,Hx),
abolish(current_state_of_beliefs/1),
assert(current_state_of_beliefs((E,X,Hx))).
generate_rational_belief_set(E,X,Hx):-
make_a_state_of_beliefs(E,X,Hx),
abolish(belief_0/4),
forall(proposition(Prop,Ops),
(
add_belief_if_satisfiable_by_models(Prop,Ops,E)
)
),
set_belief_set_0_if_empty.
add_belief_if_satisfiable_by_models(Prop,Ops,E):-
forall((member(B,E),M=(_,B,_)),
is_a_model(M,(+,Prop,Ops))
),
update_belief_by(+,Prop,Ops,B).
add_belief_if_satisfiable_by_models(_,_,_).
update_belief_by(Op,Prop,Ops,B):-
clause(belief_0(Op,Prop,Ops,B),true).
update_belief_by(Op,Prop,Ops,B):-
\+ clause(belief_0(Op,Prop,Ops,B),true),
assert(belief_0(Op,Prop,Ops,B)).
% added: 28-29 Mar 2005. exceptional handling.
set_belief_set_0_if_empty:-
\+ clause(belief_0(_,_,_,_),true),
abolish(belief_set_0/2),
assert(belief_set_0(+,[])),
!.
set_belief_set_0_if_empty.
/*
%%% demo %%%
% [story 1] there is a LC out of the default belief.
%---------------------------------------------------%
?- set_model(1,[a,b,c]).
complete
total:72 successful goals have asserted as temp_goal/3.
All generated data have replaced by proposition_0/2.
Yes
?- all_propositions(A),length(A,N).
A = [o, a, b, c, (-, o), (-, a), (-, b), (-, c), (..., ...)|...]
N = 72
Yes
?- belief_set(+,K),member(P,K),
is_a_logical_consequence(P->Q),\+ belief(+,Q).
K = [a, (a, &, a), (a, v, a), (a, (->), a)]
P = a
Q = -, o ;
K = [a, (a, &, a), (a, v, a), (a, (->), a)]
P = a
Q = o, v, a
Yes
?-
% [story 2] there is no LC out of rational beliefs. And
% all valid propositional formula are always contained.
%---------------------------------------------------%
?- generate_rational_belief_set(E,X,Hx),
E\=[],belief_set(+,K),length(K,L).
E = [[+, +, +], [+, +, -], [+, -, +], [+, -, -], [-, +, +], [-, +, -], [-, -|...], [-|...]]
X = [1, 1, 1, 1, 1, 1, 1, 1]
Hx = ff
K = [ (-, o), (a, (->), a), (b, (->), b), (c, (->), c), (o, (->), a), (o, (->), b), (o, (->), c), (o, ..., ...)]
L = 8
Yes
?- belief_set(+,K),member(P,K),
is_a_logical_consequence(P->Q), \+ member(Q, K).
No
?-
% Note:
% The above set of beliefs K consists of all (truncated)
% valid propositional formula.
?- proposition(A,L),\+ belief(+,A),
is_valid(A).
No
?- generate_rational_belief_set([[+,+,+]],X,H),
belief_set(+,K),length(K,L).
X = [1, 0, 0, 0, 0, 0, 0, 0]
H = '80'
K = [a, b, c, (-, o), (a, &, a), (a, &, b), (a, &, c), (a, ..., ...), (..., ...)|...]
L = 53
Yes
?- belief_set(+,K),member(P,K),
is_a_logical_consequence(P->Q), \+ member(Q, K).
No
?- proposition(A,L),\+ belief(+,A),,+,+]],X,H),
is_valid(A).
No
?- generate_rational_belief_set([[+,+,+],[-,+,+]],X,H),
belief_set(+,K),length(K,L).
X = [1, 0, 0, 0, 1, 0, 0, 0]
H = '88'
K = [b, c, (-, o), (a, (->), a), (a, (->), b), (a, (->), c), (a, >, b), (a, ..., ...), (..., ...)|...]
L = 38
Yes
?- belief_set(+,K),member(P,K),
is_a_logical_consequence(P->Q), \+ member(Q, K).
No
?- proposition(A,L),\+ belief(+,A),
is_valid(A).
No
?-
% [story 3] Empty model set consists of all propositions.
% (A belief set which has no model is absurd.)
%---------------------------------------------------%
?- generate_rational_belief_set([],X,H),
belief_set(+,K),length(K,L).
X = [0, 0, 0, 0, 0, 0, 0, 0]
H = '00'
K = [a, b, c, o, (-, a), (-, b), (-, c), (-, o), (..., ...)|...]
L = 72
Yes
?- proposition(A,L),\+ belief(+,A),
is_consistent(A).
No
% [story 4] a more complex belief
%---------------------------------------------------%
?- set_model(2,[a,b,c]),display_model.
complete
total:2316 successful goals have asserted as temp_goal/3.
All generated data have replaced by proposition_0/2.
upper_limit_of_steps:2
atomic_propositions:[a, b, c]
Yes
?- generate_rational_belief_set(E,X,'80'),
belief_set(+,K),length(K,L).
E = [[+, +, +]]
X = [1, 0, 0, 0, 0, 0, 0, 0]
K = [a, b, c, (-, o), (-, -, a), (-, -, b), (-, -, c), (-, ..., ...), (..., ...)|...]
L = 1723
Yes
?- propositions_satisfiable_by_model(+,Q,(_,[+,+,+],_)),
length(Q,L).
Q = [ (a, []), (b, []), (c, []), ((-, o), [-]), ((-, -, a), [-, -]), ((-, -, b), [-, -]), ((-, ..., ...), [-|...]), ((..., ...), [...|...]), (..., ...)|...]
L = 1723
Yes
?-
*/
/*************************************************
%~ 12. belief revision with conditionals
*************************************************/
% 26-28 Mar 2005
%---------------------------------------------------%
% 12.1 The theory of belief revision (G\"ardenfors, 1986)
%---------------------------------------------------%
% (,): a belief revision model
%---------------------------------------------------%
% A belief revision model is a pair (,), where
% is a set of belief sets and is a function
% from x to taking the pair (K,A) to K_A.
%%% see belief_revision/3, 4 below.
% K_A: minimal change of K by A
%---------------------------------------------------%
% For every belief set K and every proposition A in
% (instead of a bold L), there is a unique belief set K_A,
% the minimal change of K to accept A. (See [1], p.83)
%%% see minimal_change/3, 4 below.
% K/A: expansion of K by A
%---------------------------------------------------%
% An expansion of K by A, denoted K/A, is the set
% of logical consequences of K together with A, or,
% in other words, the set of propositions B such that
% A->B (- K.
% It will be assumed that is closed w.r.t. expansion
% ([1], p.85).
% K-A: the contraction of K by A
%---------------------------------------------------%
% The maxichoice(/partial meet) contraction of K by A
% is a removal of the maximal subset of belief set K
% (/the intersection of all the maximal subsets
% selected by a `selection function')
% which fail to imply A.
% And by a reduction in the sense of `Levi identity',
% the revison function K+A is the closure of consequences
% of the contraction K-A with A. (See [3])
% the Ramsey test: conditional as minimal change
%---------------------------------------------------%
% (R) A > B (- K iff B (- K_A
% i.e., Accept a proposition of the form "if A then C"
% in a state of belief K if and only if
% the minimal change of K needed to accept A
% also requires accepting C.
% (See [1], p.81 and p.84)
% the preservation criterion
%---------------------------------------------------%
% (P) if not (-A (- K) and B (- K, then B (- K_A,
% i.e., if a proposition B is accepted in a given state
% of belief K and A is consistent with the beliefs
% in K, then B is still accepted in the minimal
% change of K needed to accept A.
% ([1], p.82 and p.84)
% The rationale requires us `informational economy',
% i.e., we should not give up beliefs unnecessary.
% conditional as a necessary elements
%---------------------------------------------------%
% (0) Belief sets include propositions containing
% the conditional connective > as elements.
% (See [1], p.83)
has_conditional_connective:-
\+ \+ belief(+,(_,>,_)).
% Rules 1--2
%---------------------------------------------------%
% (1) A (- K_A,
% (2) if K \= K_[] and K_A \= K_[], then |- -A.
% Rules 3--4
%---------------------------------------------------%
% (3) (K/A)/B = K/(A&B),
% (4) K/(AvB) (= K/A.
% the monotonicity criterion
%---------------------------------------------------%
% (M) for all belief sets K and K' and all propositions
% A, if K (= K', then K_A (= K'_A.
% ((M) is implied by (R). See [1], p.84)
% the inclusion property
%---------------------------------------------------%
% (I) if not (-A (- K), then K/A (= K_A.
% ((P) and (1) implies (I). See [1], p.85)
% the inconsisteny theorem ([1])
%---------------------------------------------------%
% The Ramsey test and the preservation criterion is
% inconsistent with each other unless the belief revision
% model is trivial. That is
% there is no non-trivial belief revision model
% (,) that satisfies all conditions (1), (2),
% (M) and (P).
%---------------------------------------------------%
% 12.2 The script to generate all possible revisions
%---------------------------------------------------%
% test_belief_revision/0
% and test_belief_revision_0/3.
:- dynamic tmp_belief/2.
test_gen_rbs:-
abolish(tmp_belief/2),
test_gen_rbs(_,_),
fail.
test_gen_rbs.
test_gen_rbs((C,X,H),(K,L)):-
generate_rational_belief_set(C,X,H),
belief_set(+,K),
length(K,L),
assert(tmp_belief((C,X,H),(K,L))).
% a tool for the ex post analysis
update_belief_set((C,X,H),(K,L)):-
generate_tmp_belief_if_not_exist,
tmp_belief((C,X,H),(K,L)),
abolish(belief_set_0/2),
assert(belief_set_0(+,K)).
generate_tmp_belief_if_not_exist:-
\+ clause(tmp_belief(_,_),true),
test_gen_rbs,
!.
generate_tmp_belief_if_not_exist.
/*
%%% demo %%% (demo 12(1))
% every generated belief set are closed under logical consequence.
?- set_model(1,[a,b,c]),display_model.
complete
total:72 successful goals have asserted as temp_goal/3.
All generated data have replaced by proposition_0/2.
upper_limit_of_steps:1
atomic_propositions:[a, b, c]
Yes
?- test_gen_rbs.
Yes
?- findall(1,tmp_belief(A,B),L),length(L,N).
A = _G157
B = _G158
L = [1, 1, 1, 1, 1, 1, 1, 1, 1|...]
N = 256
Yes
?- tmp_belief((M,X,H),(K,L)).
M = [[+, +, +], [+, +, -], [+, -, +], [+, -, -], [-, +, +], [-, +, -], [-, -|...], [-|...]]
X = [1, 1, 1, 1, 1, 1, 1, 1]
H = ff
K = [ (-, o), (a, (->), a), (b, (->), b), (c, (->), c), (o, (->), a), (o, (->), b), (o, (->), c), (o, ..., ...)]
L = 8 ;
M = [[+, +, +], [+, +, -], [+, -, +], [+, -, -], [-, +, +], [-, +, -], [-, -|...]]
X = [1, 1, 1, 1, 1, 1, 1, 0]
H = fe
K = [ (-, o), (a, (->), a), (b, (->), b), (c, (->), c), (o, (->), a), (o, (->), b), (o, (->), c), (o, ..., ...)]
L = 8 ;
(...)
?- tmp_belief(A,(K,_)),member(B,K),
is_a_logical_consequence(B->C),\+ member(C,K).
No
?-
*/
%---------------------------------------------------%
% 12.2 A script to examine belief revision.
%---------------------------------------------------%
test_belief_revision:-
test_belief_revision_0(_,_,_).
test_belief_revision_0((M,K,L),(M1,K1,L1),Data):-
(var(M)->M=[[-,-,-]];true),
(var(M1)->M1=[[+,-,-]];true),
test_belief_revision_1(_),
test_belief_revision_2(_,[(M,K,L),(M1,K1,L1)]),
test_belief_revision_3(_,[K,K1|Data]),
test_belief_revision_4(_,[(M,L),(M1,L1)|Data]).
test_belief_revision_1(initialize):-
abolish(tmp_belief/2).
test_belief_revision_2(generate,[(M,K,L),(M1,K1,L1)]):-
test_gen_rbs((M,_),(K,L)),
test_gen_rbs((M1,_),(K1,L1)).
%tmp_belief((M,_),(K,L)),
%tmp_belief((M1,_),(K1,L1)).
test_belief_revision_3(analize,[K,K1,(D,LD),(C,LC),(I,LI)]):-
subtract(K1,K,D),
subtract(K,K1,C),
intersection(K,K1,I),
length(D,LD),
length(C,LC),
length(I,LI).
test_belief_revision_4(display,Data):-
Data=[(M,L),(M1,L1),(D,LD),(C,LC),(I,LI)],
forall_nl_write([
('K':M, length(L)),
('K1':M1, length(L1)),
('K1-K':D,length(LD)),
('K-K1':C,length(LC)),
(intersection:I,length(LI))
]).
/*
%%% demo %%% (demo 12(2))
% an experimentation by default model (1, [a,b,c]).
?- test_belief_revision.
K: [[-, -, -]], length(20)
K1: [[+ ,-, -]], length(29)
K1-K:[a, (a, &, a), (a, >, a), (a, v, a),
(a, v, b), (a, v, c), (a, v, o), (b, >, a), (b, v, a),
(c, >, a), (c, v, a), (o, >, a), (o, v, a)],
length(13)
K-K1:[ (-, a), (a, (->), b), (a, (->), c), (a, (->), o)],
length(4)
intersection:[ (-, b), (-, c), (-, o), (a, (->), a),
(b, (->), a), (b, (->), b), (b, (->), c), (b, (->), o),
(c, (->), a), (c, (->), b), (c, (->), c), (c, (->), o),
(o, (->), a), (o, (->), b), (o, (->), c), (o, (->), o)],
length(16)
No
?- M=[[-,-,-]],M1=[[+,-,-],[-,-,-]],
test_belief_revision_0((M,_),(M1,_),D).
K:[[-, -, -]], length(20)
K1:[[+, -, -], [-, -, -]], length(33)
K1-K:[a, (a, &, a), (a, >, a), (a, v, a), (a, v, b),
(a, v, c), (a, v, o), (b, >, a), (b, v, a),
(c, >, a), (c, v, a), (o, >, a), (o, v, a)],
length(13)
K-K1:[], length(0)
intersection:[ (-, a), (-, b), (-, c), (-, o),
(a, (->), a), (a, (->), b), (a, (->), c), (a, (->), o),
(b, (->), a), (b, (->), b), (b, (->), c), (b, (->), o),
(c, (->), a), (c, (->), b), (c, (->), c), (c, (->), o),
(o, (->), a), (o, (->), b), (o, (->), c), (o, (->), o)],
length(20)
M = [[-, -, -]]
M1 = [[+, -, -], [-, -, -]]
D = [ ([a, (a, &, a), (a, >, a), (a, v, a), (a, v, b), (a, ..., ...), (..., ...)|...], 13), ([], 0), ([ (-, a), (-, b), (-, c), (-, o), (..., ...)|...], 20)]
Yes
?- M1=[B|M],
test_belief_revision_0((M,_),(M1,_),[(_,L),(_,L1),(_,LI)]),
assert(d1(M1;k1-k:L;k-k1:L1;meet:LI)),fail.
(...)
Yes
?- display_goals(d1(A)).
d1(([[-, -, +], [-, -, -]];k1-k:13;k-k1:0;meet:20))
d1(([[-, +, -], [-, -, -]];k1-k:13;k-k1:0;meet:20))
d1(([[-, +, +], [-, -, -]];k1-k:26;k-k1:0;meet:20))
d1(([[+, -, -], [-, -, -]];k1-k:13;k-k1:0;meet:20))
d1(([[+, -, +], [-, -, -]];k1-k:26;k-k1:0;meet:20))
d1(([[+, +, -], [-, -, -]];k1-k:26;k-k1:0;meet:20))
d1(([[+, +, +], [-, -, -]];k1-k:39;k-k1:0;meet:20))
A = _G157
Yes
*/
%---------------------------------------------------%
% 12.3 belief revision and the minimal change
%---------------------------------------------------%
% The Result of a revision is summarized as
% Data=[(Removed,Added,Kept),(LR,LA,LK)],
% where the meaning of each term is respectively
% Removed: the contraction (length: LR),
% Added: the expansion (length: LA), and
% Kept: the preservation (length: LK)
% in the last argument both of minimal_change/4
% and of belief_revision/4.
% the minimality criteria is LR + LA -> min.
% This is not in same vein as the literature [1].
% (The AGM revision theory [3] posed the partial meet contraction
% to save the removed beliefs.)
minimal_change((K,L,E,H),A,(Ka,N,F,G),Data):-
generate_tmp_belief_if_not_exist,
(var(E)->tmp_belief((E,_,H),(K,L));true),
(var(A)->proposition(A,_);true),
min(LR+LA,
(
belief_revision((K,L,E,H),A,(Ka,N,F,G),Data),
Data=[_,(LR,LA,_)]
)
).
belief_revision((K,L,E,H),A,(K1,L1,E1,H1)):-
generate_tmp_belief_if_not_exist,
(var(E)->tmp_belief((E,_,H),(K,L));true),
(var(A)->proposition(A,_);true),
tmp_belief((E1,_,H1),(K1,L1)),
member(A,K1).
belief_revision((K,L,E,H),A,(Ka,L1,E1,H1),Data):-
belief_revision((K,L,E,H),A,(Ka,L1,E1,H1)),
subtract(K,Ka,Removed),
subtract(Ka,K,Added),
intersection(K,Ka,Kept),
length(Removed,LR),
length(Added,LA),
length(Kept,LK),
Data=[(Removed,Added,Kept),(LR,LA,LK)].
:- dynamic tmp_revision/1.
test_gen_mc:-
test_gen_mc(a).
test_gen_mc(A):-
proposition(A,_),
minimal_change((K,_,E,H),A,(_Ka,_,F,G),[(R,Ad,_),Len]),
\+ member(A,K),
assert(
tmp_revision(
[(k:H,k1:G,'#rai':Len),m:E,m1:F,remove:R,add:Ad]
)
),
fail.
test_gen_mc(_):-
nl,write('complete').
:- dynamic tmp_preserving_mc/2.
verify_mc(preservation):-
verify_mc(preservation,a).
verify_mc(preservation,A):-
proposition(A,_),
abolish(tmp_preserving_mc/2),
MC=minimal_change((K,_),A,(_Ka,_),[_,(LR,_)]),
MC,
(\+ member((-,a),K)->(LR=0->X=yes;X=no);X=yes),
assert(tmp_preserving_mc(X,MC)),
fail.
verify_mc(preservation,_A):-
member(X,[_,yes,no]),
findall(1,tmp_preserving_mc(X,_MC),L),
length(L,N),
nl,write(preservation:X;N),
fail.
verify_mc(preservation,A):-
verify_mc_triviality(A),
fail.
verify_mc(_,_):-
nl,write('complete').
verify_mc_triviality(A):-
forall(tmp_preserving_mc(yes,MC),
(
MC=minimal_change((K,L,_,H),A,_,_),
update_belief_set((_,_,H),(K,L)),
is_non_trivial_belief_model(NTBM),
(NTBM\=trivial
->(assert(tmp_ntbm(H,NTBM)),fail)
; true
)
)
),
!,
nl,
write('All the belief models are trivial.').
verify_mc_triviality(A):-
tmp_ntbm(H,NTBM),
nl,
write('Found nontrivial model for':(A,H,NTBM)).
/*
%%% demo %%% (demo 12(3) continued from 12(2))
% belief_revision/4:
% minimal_change/4:
belief_revision((K,L,E,H),a,(Ka,L1,F,G),[(D,A,K),Ldak]).
minimal_change((K,L,E,H),a,(Ka,L1,F,G),[DAK,Ldak]).
% D: deleted, A: added, K: kept.
% [story 1] The valid belief changes minimally by accepting all logical consequences
% (a special case of (I), the inclusion criterion.)
%---------------------------------------------------%
?- belief_revision((K,L,E,H),a,(Ka,L1,F,G),[DAK,Ldak]),
\+ member(a,K).
E = [[+, +, +], [+, +, -], [+, -, +], [+, -, -], [-, +, +], [-, +, -], [-, -|...], [-|...]]
H = ff
K = [ (-, o), (a, (->), a), (b, (->), b), (c, (->), c), (o, (->), a), (o, (->), b), (o, (->), c), (o, ..., ...)]
L = 8
Ka = [a, (-, o), (a, &, a), (a, (->), a), (a, >, a), (a, v, a), (a, v, b), (a, ..., ...), (..., ...)|...]
L1 = 23
F = [[+, +, +], [+, +, -], [+, -, +], [+, -, -]]
G = f0
DAK = [], [a, (a, &, a), (a, >, a), (a, v, a), (a, v, b), (a, ..., ...), (..., ...)|...], [ (-, o), (a, (->), a), (b, (->), b), (c, (->), c), (o, (->), a), (o, ..., ...), (..., ...)|...]
Ldak = 0, 15, 8
Yes
?- findall(P,is_a_logical_consequence(a->P),Q),length(Q,L).
P = _G161
Q = [a, (-, o), (a, &, a), (o, v, a), (a, v, o), (a, v, a), (a, v, b), (a, ..., ...), (..., ...)|...]
L = 23
Yes
?- minimal_change((K,L,E,H),a,(Ka,L1,F,G),[DAK,Ldak]).
K = [ (-, o), (a, (->), a), (b, (->), b), (c, (->), c), (o, (->), a), (o, (->), b), (o, (->), c), (o, ..., ...)]
L = 8
E = [[+, +, +], [+, +, -], [+, -, +], [+, -, -], [-, +, +], [-, +, -], [-, -|...], [-|...]]
H = ff
Ka = [a, (-, o), (a, &, a), (a, (->), a), (a, >, a), (a, v, a), (a, v, b), (a, ..., ...), (..., ...)|...]
L1 = 23
F = [[+, +, +], [+, +, -], [+, -, +], [+, -, -]]
G = f0
DAK = [], [a, (a, &, a), (a, >, a), (a, v, a), (a, v, b), (a, ..., ...), (..., ...)|...], [ (-, o), (a, (->), a), (b, (->), b), (c, (->), c), (o, (->), a), (o, ..., ...), (..., ...)|...]
Ldak = 0, 15, 8
Yes
% [story 2] revision of thinly supported (i.e., belief with singlton model)
%---------------------------------------------------%
?- belief_revision((K,L,E,H),a,(Ka,L1,F,G),[DAK,Ldak]),
length(E,1),\+ member(a,K).
K = [b, c, (-, a), (-, o), (a, (->), a), (a, (->), b), (a, (->), c), (a, ..., ...), (..., ...)|...]
L = 40
E = [[-, +, +]]
H = '08'
Ka = [a, (-, o), (a, &, a), (a, (->), a), (a, >, a), (a, v, a), (a, v, b), (a, ..., ...), (..., ...)|...]
L1 = 23
F = [[+, +, +], [+, +, -], [+, -, +], [+, -, -]]
G = f0
DAK = [b, c, (-, a), (a, (->), b), (a, (->), c), (a, (->), o), (a, ..., ...), (..., ...)|...], [a, (a, &, a), (a, >, a), (a, v, a), (a, v, o), (b, ..., ...), (..., ...)|...], [ (-, o), (a, (->), a), (a, v, b), (a, v, c), (b, (->), b), (b, ..., ...), (..., ...)|...]
Ldak = 28, 11, 12 ;
K = [b, c, (-, a), (-, o), (a, (->), a), (a, (->), b), (a, (->), c), (a, ..., ...), (..., ...)|...]
L = 40
E = [[-, +, +]]
H = '08'
Ka = [a, (-, o), (a, &, a), (a, (->), a), (a, >, a), (a, v, a), (a, v, b), (a, ..., ...), (..., ...)|...]
L1 = 25
F = [[+, +, +], [+, +, -], [+, -, +]]
G = e0
DAK = [b, c, (-, a), (a, (->), b), (a, (->), c), (a, (->), o), (a, ..., ...), (..., ...)|...], [a, (a, &, a), (a, >, a), (a, v, a), (a, v, o), (b, ..., ...), (..., ...)|...], [ (-, o), (a, (->), a), (a, v, b), (a, v, c), (b, (->), b), (b, ..., ...), (..., ...)|...]
Ldak = 26, 11, 14
Yes
?- minimal_change((K,L,E,H),a,(Ka,L1,F,G),[DAK,Ldak]),
length(E,1),\+ member(a,K).
K = [b, c, (-, a), (-, o), (a, (->), a), (a, (->), b), (a, (->), c), (a, ..., ...), (..., ...)|...]
L = 40
E = [[-, +, +]]
H = '08'
Ka = [a, b, c, (-, o), (a, &, a), (a, &, b), (a, &, c), (a, ..., ...), (..., ...)|...]
L1 = 53
F = [[+, +, +]]
G = '80'
DAK = [ (-, a), (a, (->), o)], [a, (a, &, a), (a, &, b), (a, &, c), (a, >, a), (a, ..., ...), (..., ...)|...], [b, c, (-, o), (a, (->), a), (a, (->), b), (a, ..., ...), (..., ...)|...]
Ldak = 2, 15, 38 ;
K = [b, (-, a), (-, c), (-, o), (a, (->), a), (a, (->), b), (a, (->), c), (a, ..., ...), (..., ...)|...]
L = 29
E = [[-, +, -]]
H = '04'
Ka = [a, b, (-, c), (-, o), (a, &, a), (a, &, b), (a, (->), a), (a, ..., ...), (..., ...)|...]
L1 = 40
F = [[+, +, -]]
G = '40'
DAK = [ (-, a), (a, (->), c), (a, (->), o)], [a, (a, &, a), (a, &, b), (a, >, a), (a, v, a), (a, ..., ...), (..., ...)|...], [b, (-, c), (-, o), (a, (->), a), (a, (->), b), (a, ..., ...), (..., ...)|...]
Ldak = 3, 14, 26
Yes
% [story 3] an ex post analysis for minimal changes by a.
%---------------------------------------------------%
?- test_gen_mc.
complete
Yes
?- tmp_revision([A,m:E,m1:F,_,_]),
intersection(E,F,EF),length(E,N),length(EF,L),Q is L/N.
A = k:ff, k1:f0, '#rai': (0, 15, 8)
E = [[+, +, +], [+, +, -], [+, -, +], [+, -, -], [-, +, +], [-, +, -], [-, -|...], [-|...]]
F = [[+, +, +], [+, +, -], [+, -, +], [+, -, -]]
EF = [[+, +, +], [+, +, -], [+, -, +], [+, -, -]]
N = 8
L = 4
Q = 0.5 ;
A = k:ff, k1:'70', '#rai': (0, 15, 8)
E = [[+, +, +], [+, +, -], [+, -, +], [+, -, -], [-, +, +], [-, +, -], [-, -|...], [-|...]]
F = [[+, +, -], [+, -, +], [+, -, -]]
EF = [[+, +, -], [+, -, +], [+, -, -]]
N = 8
L = 3
Q = 0.375 ;
A = k:fe, k1:f0, '#rai': (0, 15, 8)
E = [[+, +, +], [+, +, -], [+, -, +], [+, -, -], [-, +, +], [-, +, -], [-, -|...]]
F = [[+, +, +], [+, +, -], [+, -, +], [+, -, -]]
EF = [[+, +, +], [+, +, -], [+, -, +], [+, -, -]]
N = 7
L = 4
Q = 0.571429
Yes
?- min(Q,(tmp_revision([A,m:E,m1:F,_,_]),
intersection(E,F,EF),length(E,N),length(EF,L),Q is L/N)).
Q = 0
A = k:'01', k1:'10', '#rai': (4, 13, 16)
E = [[-, -, -]]
F = [[+, -, -]]
EF = []
N = 1
L = 0 ;
Q = 0
A = k:'02', k1:'20', '#rai': (3, 14, 26)
E = [[-, -, +]]
F = [[+, -, +]]
EF = []
N = 1
L = 0
Yes
?- tmp_revision([A,m:E,m1:F,_,_]),
intersection(E,F,EF),length(E,N),length(EF,L),Q is L/N,Q=1.
No
?- tmp_revision([A,m:E,m1:F,_:Add,_:Remove]),nl,write(A),fail.
(...)
k:11, k1:10, #rai: (0, 13, 16)
k:0c, k1:c0, #rai: (3, 15, 23)
k:0a, k1:a0, #rai: (3, 15, 23)
k:09, k1:90, #rai: (4, 15, 10)
k:06, k1:e0, #rai: (4, 15, 10)
k:06, k1:60, #rai: (4, 15, 10)
k:05, k1:50, #rai: (4, 14, 12)
k:03, k1:30, #rai: (4, 14, 12)
k:08, k1:80, #rai: (2, 15, 38)
k:04, k1:40, #rai: (3, 14, 26)
k:02, k1:20, #rai: (3, 14, 26)
k:01, k1:10, #rai: (4, 13, 16)
No
?-
% [story 4] Is minimality criteria (2) satisfied ?
%---------------------------------------------------%
?- tmp_belief(([],A),K).
A = [0, 0, 0, 0, 0, 0, 0, 0], '00'
K = [a, b, c, o, (-, a), (-, b), (-, c), (..., ...)|...], 72
Yes
?- belief_revision((K,L,E,H),a,(Ka,L1,F,G),[DAK,Ldak]),
\+ member(a,K),G='00'.
K = [ (-, o), (a, (->), a), (b, (->), b), (c, (->), c), (o, (->), a), (o, (->), b), (o, (->), c), (o, ..., ...)]
L = 8
E = [[+, +, +], [+, +, -], [+, -, +], [+, -, -], [-, +, +], [-, +, -], [-, -|...], [-|...]]
H = ff
Ka = [a, b, c, o, (-, a), (-, b), (-, c), (-, o), (..., ...)|...]
L1 = 72
F = []
G = '00'
DAK = [], [a, b, c, o, (-, a), (-, b), (..., ...)|...], [ (-, o), (a, (->), a), (b, (->), b), (c, (->), c), (o, (->), a), (o, ..., ...), (..., ...)|...]
Ldak = 0, 64, 8
Yes
?- minimal_change((K,L,E,H),a,(Ka,L1,F,G),[DAK,Ldak]),
\+ member(a,K),G='00'.
No
?- minimal_change((K,L,E,H),a,(Ka,N,F,G),[(R,Ad,I),(LR,LA,LI)]),
G='00'.
K = [a, b, c, o, (-, a), (-, b), (-, c), (-, o), (..., ...)|...]
L = 72
E = []
H = '00'
Ka = [a, b, c, o, (-, a), (-, b), (-, c), (-, o), (..., ...)|...]
N = 72
F = []
G = '00'
R = []
Ad = []
I = [a, b, c, o, (-, a), (-, b), (-, c), (-, o), (..., ...)|...]
LR = 0
LA = 0
LI = 72 ;
No
?- minimal_change((K,L,E,H),A,(Ka,L1,F,G),[DAK,Ldak]),
\+ member(A,K),G='00'.
K = [ (-, o), (a, (->), a), (b, (->), b), (c, (->), c), (o, (->), a), (o, (->), b), (o, (->), c), (o, ..., ...)]
L = 8
E = [[+, +, +], [+, +, -], [+, -, +], [+, -, -], [-, +, +], [-, +, -], [-, -|...], [-|...]]
H = ff
A = o
Ka = [a, b, c, o, (-, a), (-, b), (-, c), (-, o), (..., ...)|...]
L1 = 72
F = []
G = '00'
DAK = [], [a, b, c, o, (-, a), (-, b), (..., ...)|...], [ (-, o), (a, (->), a), (b, (->), b), (c, (->), c), (o, (->), a), (o, ..., ...), (..., ...)|...]
Ldak = 0, 64, 8
Yes
?- minimal_change((K,L,E,H),A,(Ka,L1,F,G),[DAK,Ldak]),
\+ member(A,K),G='00',is_consistent(A).
No
?-
% [story 5] minimal change always satisifies monotonicity
%---------------------------------------------------%
% the monotonicity criterion :
% (M) if K (= K' then K_A (= K'_A.
?- minimal_change((K,_),a,(Ka,_),_),
minimal_change((K1,_),a,(K1a,_),_),
subset(K,K1),\+ subset(Ka,K1a).
No
% [story 6] the inconsistency:
% is preservation confirming belief model always trivial ?
%---------------------------------------------------%
% the preservation criterion :
% (P) if not (-A (- K) and B (- K, then B (- K_A.
?- minimal_change((K,L,E,H),a,(Ka,N,F,G),[(R,Ad,I),(LR,LA,LI)]),
\+ member((-,a),K),LR>0.
K = [ (-, o), (a, (->), a), (a, (->), b), (b, (->), b), (c, (->), c), (o, (->), a), (o, (->), b), (o, ..., ...), (..., ...)]
L = 9
E = [[+, +, +], [+, +, -], [-, +, +], [-, +, -], [-, -, +], [-, -, -]]
H = cf
Ka = [a, (-, o), (a, &, a), (a, (->), a), (a, >, a), (a, v, a), (a, v, b), (a, ..., ...), (..., ...)|...]
N = 23
F = [[+, +, +], [+, +, -], [+, -, +], [+, -, -]]
G = f0
R = [ (a, (->), b)]
Ad = [a, (a, &, a), (a, >, a), (a, v, a), (a, v, b), (a, v, c), (a, v, o), (b, ..., ...), (..., ...)|...]
I = [ (-, o), (a, (->), a), (b, (->), b), (c, (->), c), (o, (->), a), (o, (->), b), (o, (->), c), (o, ..., ...)]
LR = 1
LA = 15
LI = 8
Yes
?- verify_mc(preservation).
preservation:_G160;400
preservation:yes;302
preservation:no;98
there is nontrivial beliefs
complete
Yes
?-
% Precisely, the rational belief model (1,[a,b,c]) is trivial.
?- update_belief_set((M,X,H),(K,L)),
\+ is_non_trivial_belief_model([A,B,C]).
No
?-
*/
/*************************************************
%~ Appendix 1. State space
*************************************************/
% cited and modified from: kglp01.pl
% the only modification is state/1 that
% we regard a tuple of truth asignment for
% atomic propositions. ('atomic' propositions
% are so called in this program, not
% in the literature.)
state(B):-
truth_assignment(_,B,_).
all_states(S):-
X=state(I),
findall(I,X,S).
% events
%---------------------------------------------------%
event(E):-
var(E),
event(E,_N).
event(E):-
\+ var(E),
event_def(E).
% generating a list of the given length
%--------------------------------------
event(E,N):-
\+ var(E),
event_def(E),
length(E,N).
event(E,N):-
var(E),
event(E,_P,N).
event(E,P,N):-
\+ var(E),
all_states(O),
list_projection(P,O,E),
length(E,N).
event(E,P,N):-
var(E),
all_states(O),
length(O,U),
choose_N_units_among(U,N,P),
list_projection(P,O,E).
% computing event from strategic description.
%----------------------------------
% added: 14 Feb 2005
event_description_1(E,D,Hx,CD):-
var(D),
CD=[_X1,_X2,_X3,_X4,_X5],
findall(W,state_description(W,_,CD),E),
event_description(E,_,D),
hexa_event(E,_,Hx).
% Hexa reprsentation for events
%---------------------------------------------------%
% added: 5-6 Feb 2005
hexa_event(E,X,Hx):-
event(E,X,_NE), % NE: length of E \= NX
hexa_list(X,_NX,GangOfFour),
concat_list(Hx,GangOfFour).
% hexa_list/3 ---> common programs
% complementation
%---------------------------------------------------%
% added: 4 Feb 2005
complement(E,N,C):-
all_states(O),
event(E,X,N),
c_list_projection(X,O,C).
% super/sub events
%---------------------------------------------------%
% added: 31 Jan 2005.
% modified: 1 Feb 2005.
super_event(E,F,N):-
super_event_with_length((E,N),(F,_M)).
super_event_with_length((X,N),(Y,M)):-
(var(X)->fail;true),
event(Y,M),
subset(Y,X),
length(X,N).
super_event_with_length((E,N),(F,L)):-
(var(E)->true;fail),
integer(N),
event(F,XF,L),
%nl,write([N,L:F]),
!,
L =< N,
super_projection_of_length((XE,N),(XF,L)),
% sup_projection(XE,XF),
event(E,XE,N),
subset(F,E).
super_event_with_length((E,N),(P,L)):-
(var(E)->true;fail),
var(N),
event(P,XP,L),
reverse(XP,RXP),
sup_projection(RXE,RXP),
reverse(RXE,XE),
event(E,XE,N).
super_projection_of_length((XE,N),(XF,L)):-
integer(N),
sum(XF,L),
length(XF,U),
length(XE,U),
K is N - L, % K: additional units required.
M is U - L, % M: the current number of zeros.
choose_N_units_among(M,K,Xadd),
findall(I,nth1(I,XF,0),Xzeros),
make_pairs(Xsubst,Xzeros,Xadd),
findall(Z,
(
nth1(I,XF,X),
(member((I-Y),Xsubst)->
Z is X + Y;Z = X)
),
XE).
/*************************************************
%~ Appendix 2. common programs
*************************************************/
% cited from: math1, set, moji, menu.
%---------------------------------------------------%
inductive_numbers([]).
inductive_numbers([N|H]):-
length(H,N),
inductive_numbers(H).
make_pairs([],[],[]).
make_pairs([A-X|Z],[A|B],[X|Y]):-
length(B,N),
length(Y,N),
length(Z,N),
make_pairs(Z,B,Y).
% intersection of list
%---------------------------------------------------%
intersection_of_lists([],_).
intersection_of_lists([X|H],Z):-
intersection_of_lists(H,Y),
intersection(X,Y,Z).
% concat list
%---------------------------------------------------%
concat_list(A,[A]).
concat_list(Z,[L|R]):-
concat_list(Q,R),
concat(L,Q,Z).
% super set projection
%---------------------------------------------------%
sup_projection([],[]).
sup_projection([W|Z],[X|Y]):-
member((X,W),[(1,1),(0,0),(0,1)]),
sup_projection(Z,Y).
% a naive program of distribution (index function).
% this is not useful for generate a long list.
%---------------------------------------------------%
project_N_things_of(N,O,P,Q):-
integer(N),
length(O,U),
N==N)
->!,true
; (
inductive_numbers([U|M]),
member(N,[U|M])
)),
length(P,U),
choose_N_units_0(P,N,_L).
% validation of bit sequence
is_a_bounded_bit_sequence_of_length(P,L):-
length(P,L),
forall(member(X,P),
(
\+ var(X),
member(X,[0,1])
)
).
% generation of bit sequence
choose_N_units_0([],0,0).
choose_N_units_0(Z,0,0):-
length(Z,R),
zeros(Z,R).
choose_N_units_0(Z,M,L):-
length(Z,R),
M>=R,
ones(Z,R),
L is M -R.
choose_N_units_0([X|Y],M,L1):-
length([X|Y],R),
M >0,
M U=0;integer(U)),
inductive_numbers([U|M]),
!,
reverse([U|M],[0|R]),
list_projection(P,R,W).
% hexa and bits (intended for abbreviation of event)
%---------------------------------------------------%
hexa_list(X,N,[Tx|Hx]):-
\+ var(X),
length(X,N),
R is N mod 4,
hexa_list_residual(R,X,Y,Tx),
hexa_list_0(Y,Hx).
hexa_list_0([],[]).
hexa_list_0([A,B,C,D|X],[Hx|Y]):-
hexa_list_0(X,Y),
hexa_1([A,B,C,D],Hx).
hexa_list_residual(0,[A,B,C,D|X],X,Hx):-
hexa_1([A,B,C,D],Hx).
hexa_list_residual(3,[A,B,C|X],X,Hx):-
hexa_1([0,A,B,C],Hx).
hexa_list_residual(2,[A,B|X],X,Hx):-
hexa_1([0,0,A,B],Hx).
hexa_list_residual(1,[A|X],X,Hx):-
hexa_1([0,0,0,A],Hx).
hexa_1(FourBits,Hx):-
list_projection(FourBits,[a,b,c,d],_),
bits(FourBits,Decimal,_B),
hexa_pattern(Hx,Decimal).
hexa_pattern(Hx,Hx):-
Hx <10,
!.
hexa_pattern(Hx,D):-
member((D,Hx),[
(10,a),(11,b),(12,c),(13,d),(14,e),(15,f)
]).
hexa(L,Decimal,Hx):-
concat_list(Hx,[0,x|L]),
atom_chars(Hx,Atoms),
number_chars(Decimal,Atoms).
bits(L,Decimal,B):-
concat_list(B,[0,b|L]),
atom_chars(B,Atoms),
number_chars(Decimal,Atoms).
% priority-considered version of bag0
%---------------------------------------------------%
variation_seek_sequence([],_A,0).
variation_seek_sequence([C|B],A,N):-
length([C|B],N),
member(C,A),
subtract(A,[C],D),
append(D,[C],E),
variation_seek_sequence(B,E,_N1).
:- dynamic temp_vss/1.
update_temp_vss(C):-
retract(temp_vss(H)),
assert(temp_vss([C|H])).
% cited from set.pl
%---------------------------------------------------%
bag0([],_A,0).
bag0([C|B],A,N):-
length([C|B],N),
bag0(B,A,_N1),
member(C,A).
zeros(Zero,N):-bag0(Zero,[0],N).
ones(One,N):-bag0(One,[1],N).
subset_of(A,N,As):-
length(As,L),
length(D,L),
list_projection(D,As,B),
length(B,N),
sort(B,A).
list_projection([],[],[]).
list_projection([X|Y],[_A|B],C):-
X = 0,
list_projection(Y,B,C).
list_projection([X|Y],[A|B],[A|C]):-
X = 1,
list_projection(Y,B,C).
c_list_projection([],[],[]).
c_list_projection([X|Y],[_A|B],C):-
X = 1,
c_list_projection(Y,B,C).
c_list_projection([X|Y],[A|B],[A|C]):-
X = 0,
c_list_projection(Y,B,C).
allocation(N,A,[X|Y]):-
allocation(N,A,A,[X|Y]).
allocation(0,_,0,[]).
allocation(N,A,B,[X|Y]):-
integer(A),
length([X|Y],N),
allocation(_N1,A,B1,Y),
K is A - B1 + 1,
length(L,K),
nth0(X,L,X),
B is B1 + X.
% cited from math1.pl
%---------------------------------------------------%
sumof(X,Goal,S):-
findall(X,Goal,Z),
sum(Z,S).
sum([],0).
sum([X|Members],Sum):-
sum(Members,Sum1),
%number(X),
Sum is Sum1 + X.
product([],1).
product([X|Members],Z):-
product(Members,Z1),
%number(X),
Z is Z1 * X.
product_sum([],[],[],0).
product_sum([P|Q],[A|B],[E|F],V):-
length(Q,N),
length(B,N),
product_sum(Q,B,F,V1),
E is P * A,
V is V1 + E.
% max,min
% ----------------------------------------------------------- %
max_of(X,[X]).
max_of(Z,[X|Y]):-
max_of(Z1,Y),
(X > Z1 -> Z=X; Z=Z1).
min_of(X,[X]).
min_of(Z,[X|Y]):-
min_of(Z1,Y),
(X < Z1 -> Z=X; Z=Z1).
% a solver : maximization of goal wrt arguments
% ----------------------------------------------------------- %
min(X,Goal):-
max(Z,(Goal,Z is -X)).
max(X,Goal):-
% X: the objective variable,
% Goal: the objective function and constraints,
setof((X,Goal),Goal,Z),
member((X,Goal),Z),
\+ (
member((Y,_),Z),
Y > X
).
% Utilities for file output and display
%---------------------------------------------------%
% cited from : menu.pl
% Display
%--------------------------------
forall_write(A):- forall(member(X,A),write(X)).
forall_nl_write(A):- forall(member(X,A),(nl,write(X))).
forall_write_goals(A,B):- B,nl,write(A),fail.
forall_write_goals(_,_):- nl,write(complete).
% 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).
% Save data to a file
%--------------------------------
tell_goal(File,G):-
(current_stream(File,write,S0)->close(S0);true),
open(File,write,S),
tell(File),
nl,
tstamp('% file output start time ',_),
nl,
write('%---------- start from here ------------%'),
nl,
G,
nl,
write('%---------- end of data ------------%'),
nl,
tstamp('% file output end time ',_),
tell(user),
close(S),
% The following is to cope with the duplicated stream problem.
(current_stream(File,write,S1)->close(S1);true).
% save all successful goals to file.
%--------------------------------
tell_goal(File,forall,G):-
G0 = (nl,write(G),write('.')),
G1 = forall(G,G0),
tell_goal(File,G1).
% the conditionalized version
% Aug 2003.
tell_goal(File,forall_such_that,G,Condition):-
% G should be occurred in the Condition.
WRITE = (nl,write(G),write('.')),
G1 = forall(Condition,WRITE),
tell_goal(File,G1).
% time stamp
%--------------------------------
tstamp(no,T):-
get_time(U),
convert_time(U,A,B,C,D,E,F,_G),
T = [date(A/B/C), time(D:E:F)],
nl.
tstamp(Word,T):-
\+ var(Word),
Word \= no,
get_time(U),
convert_time(U,A,B,C,D,E,F,_G),
T = [date(A/B/C), time(D:E:F)],
% format('~`.t~t~a~30|~`.t~t~70|~n',[Word]),
write((Word,T)),
nl.
% measuring time consumption
%--------------------------------
stopwatch_0(Goal,TD):-
get_time(TS),
Goal,
get_time(TF),
TD is TF - TS.
stopwatch(Goal,TD):-
stopwatch_0(Goal,TD),
nl,
write('% time elapsed (sec): '),
write(TD),
nl.
%---------------------------------------------------%
% Testing tools
%---------------------------------------------------%
% Equivalence
%--------------------------------
verify_equality_of_goals(G1:V1,G2:V2,S,D):-
findall(V1,G1,S1),
findall(V2,G2,S2),
subtract(S1,S2,D1),
subtract(S2,S1,D2),
S=[S1,S2],D=[D1,D2].
% a script for generating goals as facts
%---------------------------------------------------%
% a generalized version of factualize_strategies/0.
% 31 Jan 2005.
:- dynamic id_of_temp_goal/1.
:- dynamic temp_goal/3.
update_id_of_temp_goal(ID):-
retract(id_of_temp_goal(ID_0)),
ID is ID_0 +1,
assert(id_of_temp_goal(ID)).
preliminary_to_factualize_goals:-
abolish(id_of_temp_goal/1),
abolish(temp_goal/3),
assert(id_of_temp_goal(0)).
factualize_goals(G):-
warn_if_not_a_list(G),
preliminary_to_factualize_goals,
factualize_goals(G,LID),
finalize_factualization(LID).
factualize_goals([Goal|Constraint],ID):-
Goal,
Constraint,
update_id_of_temp_goal(ID),
assert(temp_goal(ID,Goal,Constraint)),
fail.
factualize_goals(_,ID):-
id_of_temp_goal(ID).
finalize_factualization(Last_ID):-
write(complete),
nl,
write(total:Last_ID),
write(' successful goals have asserted as temp_goal/3.').
warn_if_not_a_list(G):-
length(G,_),
forall(member(X,G),clause(X,_)),
!.
warn_if_not_a_list(_):-
write('**** warning : not a list of executable goals.'),
nl,
write('no data has generated.'),
fail.
:- initialize_system.
% end of program
%---------------------------------------------------%
return to front page.