%% UA

/*
 とりあえず、撤回効力発生要件から「取消不能（irrevocable）でないこと」という要件を取り除き、承諾効力発生要件に「取消効力が発生していないこと」というルールで検証しました。*/


%%%%%% General Program
:-unknown(P,fail).

%23
is_concluded(contract(A,B,C),T):-
	become_effective(acceptance(B,A,offer(A,B,C)),T).
        
%15(1)
become_effective(offer(A,B,C),T1):-
	reach(offer(A,B,C),B,T1),
        \+(become_effective(withdrawl(A,B,offer(A,B,C)),B,T2)).

%15(2)
become_effective(withdrawl(A,B,offer(A,B,C)),B,T2):-
        reach(withdrawl(A,B,offer(A,B,C)),B,T2),
        \+((reach(offer(A,B,C),B,T1),before(T1,T2))).

before(T1,T2):-
	T1@<T2.

%16(1)
become_effective(revocation(A,B,offer(A,B,C)),B,T3):-
	\+(irrevocable(offer(A,B,C))),
	reach(revocation(A,B,offer(A,B,C)),B,T3),
	(\+((dispatch(acceptance(B,A,D),A,T4)));
	(dispatch(acceptance(B,A,D),A,T4),before(T3,T4))).

%%H 二行目は、書かなくてもよい。書くとすれば次のようになる。「取消不能であってもなくても」の意見て、
	(irrevocable(offer(A,B,C));\+(irrevocable(offer(A,B,C))))

%18(2)
become_effective(acceptance(B,A,D),T):-
	become_effective(offer(A,B,C),T1),
	\+(become_effective(revocation(A,B,offer(A,B,C)),B,T3)),
	dispatch(acceptance(B,A,D),A,T4),
	reach(acceptance(B,A,D),A,T).

%%H 申込取消効力発生を承諾効力発生の障害要件と考えたのは、一つのよいアプローチだと思います。

%case3d
reach(offer(anzai,bernard,sale(agriculture_machine,'$10000')),bernard,t0408).
reach(revocation(anzai,bernard,offer(anzai,bernard,sale(agriculture_machine,'$10000'))),bernard,t0409).
dispatch(acceptance(bernard,anzai,offer(anzai,bernard,sale(agriculture_machine,'$10000'))),anzai,t0410).
reach(acceptance(bernard,anzai,offer(anzai,bernard,sale(agriculture_machine,'$10000'))),anzai,t0410).

%%%%推論実験

| ?- listing.
become_effective(offer(A,B,C), D) :-
        reach(offer(A,B,C), B, D),
        \+become_effective(withdrawl(A,B,offer(A,B,C)),B,_).
become_effective(acceptance(A,B,C), D) :-
        become_effective(offer(B,A,E), _),
        \+become_effective(revocation(B,A,offer(B,A,E)),A,_),
        dispatch(acceptance(A,B,C), B, _),
        reach(acceptance(A,B,C), B, D).

become_effective(withdrawl(A,B,offer(A,B,C)), B, D) :-
        reach(withdrawl(A,B,offer(A,B,C)), B, D),
        \+ (reach(offer(A,B,C),B,E),before(E,D)).
become_effective(revocation(A,B,offer(A,B,C)), B, D) :-
        \+irrevocable(offer(A,B,C)),
        reach(revocation(A,B,offer(A,B,C)), B, D),
        (   \+dispatch(acceptance(B,A,E),A,F)
        ;   dispatch(acceptance(B,A,E), A, F),
            before(D, F)
        ).

before(A, B) :-
        A@<B.

dispatch(acceptance(bernard,anzai,offer(anzai,bernard,sale(agriculture_machine,'$10000'))), anzai, t0410).

is_concluded(contract(A,B,C), D) :-
        become_effective(acceptance(B,A,offer(A,B,C)), D).

reach(offer(anzai,bernard,sale(agriculture_machine,'$10000')), bernard, t0408).
reach(revocation(anzai,bernard,offer(anzai,bernard,sale(agriculture_machine,'$10000'))), bernard, t0409).
reach(acceptance(bernard,anzai,offer(anzai,bernard,sale(agriculture_machine,'$10000'))), anzai, t0410).

yes
| ?- trace.
% The debugger will first creep -- showing everything (trace)
yes
% trace
| ?- is_concluded(X,T).
        1      1 Call: is_concluded(_463,_483) ?
        2      2 Call: become_effective(acceptance(_1106,_1105,offer(_1105,_1106,_1107)),_483) ?
        3      3 Call: become_effective(offer(_1105,_1106,_1790),_1793) ?
        4      4 Call: reach(offer(_1105,_1106,_1790),_1106,_1793) ?
        4      4 Exit: reach(offer(anzai,bernard,sale(agriculture_machine,'$10000')),bernard,t0408) ?
        5      4 Call: become_effective(withdrawl(anzai,bernard,offer(anzai,bernard,sale(agriculture_machine,'$10000'))),bernard,_2534) ?
        6      5 Call: reach(withdrawl(anzai,bernard,offer(anzai,bernard,sale(agriculture_machine,'$10000'))),bernard,_2534) ?
        6      5 Fail: reach(withdrawl(anzai,bernard,offer(anzai,bernard,sale(agriculture_machine,'$10000'))),bernard,_2534) ?
        5      4 Fail: become_effective(withdrawl(anzai,bernard,offer(anzai,bernard,sale(agriculture_machine,'$10000'))),bernard,_2534) ?
        3      3 Exit: become_effective(offer(anzai,bernard,sale(agriculture_machine,'$10000')),t0408) ?
        7      3 Call: become_effective(revocation(anzai,bernard,offer(anzai,bernard,sale(agriculture_machine,'$10000'))),bernard,_1781) ?
        8      4 Call: irrevocable(offer(anzai,bernard,sale(agriculture_machine,'$10000'))) ?
        8      4 Fail: irrevocable(offer(anzai,bernard,sale(agriculture_machine,'$10000'))) ?
        9      4 Call: reach(revocation(anzai,bernard,offer(anzai,bernard,sale(agriculture_machine,'$10000'))),bernard,_1781) ?
        9      4 Exit: reach(revocation(anzai,bernard,offer(anzai,bernard,sale(agriculture_machine,'$10000'))),bernard,t0409) ?
       10      4 Call: dispatch(acceptance(bernard,anzai,_5340),anzai,_5344) ?
       10      4 Exit: dispatch(acceptance(bernard,anzai,offer(anzai,bernard,sale(agriculture_machine,'$10000'))),anzai,t0410) ?
       11      4 Call: dispatch(acceptance(bernard,anzai,_5340),anzai,_5344) ?
       11      4 Exit: dispatch(acceptance(bernard,anzai,offer(anzai,bernard,sale(agriculture_machine,'$10000'))),anzai,t0410) ?
       12      4 Call: before(t0409,t0410) ?
       13      5 Call: t0409@<t0410 ?
       13      5 Exit: t0409@<t0410 ?
       12      4 Exit: before(t0409,t0410) ?
        7      3 Exit: become_effective(revocation(anzai,bernard,offer(anzai,bernard,sale(agriculture_machine,'$10000'))),bernard,t0409) ?
        2      2 Fail: become_effective(acceptance(_1106,_1105,offer(_1105,_1106,_1107)),_483) ?
        1      1 Fail: is_concluded(_463,_483) ?
no
% trace
| ?-

%%%% 今後の方針

第四弾では、
 
 承諾効力発生：−
   申し込み効力がある,
   承諾を発信している,
   承諾が到達している.
 
%%H 二行目の「効力がある」は時点が決まっていないと言えないのではないか。時点を先に決めるのにはどうしたらよいか。考え下さい。
 
 申し込み効力がある：−
   申し込み効力発生,
   取消効力不発生.
 
というルールで作ってみたいと思います。

%%H 期待しています。