13
14:- include(ec_common). 15
16
17abdemo(Gs,R) :- init_gensym(t), abdemo(Gs,[[],[]],R,[],N).
18
19
20abdemo([],R,R,N,N).
21
22
23abdemo([holds_at(F1,T)|Gs1],R1,R3,N1,N4) :-
24 F1 \= neg(F2), abresolve(initially(F1),R1,Gs2,R1),
25 append(Gs2,Gs1,Gs3), add_neg([clipped(0,F1,T)],N1,N2),
26 abdemo_naf([clipped(0,F1,T)],R1,R2,N2,N3),
27 abdemo(Gs3,R2,R3,N3,N4).
28
29abdemo([holds_at(F1,T3)|Gs1],R1,R5,N1,N4) :-
30 F1 \= neg(F2), abresolve(initiates(A,F1,T1),R1,Gs2,R1),
31 abresolve(happens(A,T1,T2),R1,[],R2),
32 abresolve(before(T2,T3),R2,[],R3),
33 append(Gs2,Gs1,Gs3),
34 add_neg([clipped(T1,F1,T3)],N1,N2),
35 abdemo_nafs(N2,R3,R4,N2,N3),
36 abdemo(Gs3,R4,R5,N3,N4).
37
38abdemo([holds_at(neg(F),T)|Gs1],R1,R3,N1,N4) :-
39 abresolve(initially(neg(F)),R1,Gs2,R1),
40 append(Gs2,Gs1,Gs3), add_neg([declipped(0,F,T)],N1,N2),
41 abdemo_naf([declipped(0,F,T)],R1,R2,N2,N3),
42 abdemo(Gs3,R2,R3,N3,N4).
43
44abdemo([holds_at(neg(F),T3)|Gs1],R1,R5,N1,N4) :-
45 abresolve(terminates(A,F,T1),R1,Gs2,R1),
46 abresolve(happens(A,T1,T2),R1,[],R2),
47 abresolve(before(T2,T3),R2,[],R3),
48 append(Gs2,Gs1,Gs3),
49 add_neg([declipped(T1,F,T3)],N1,N2),
50 abdemo_nafs(N2,R3,R4,N2,N3),
51 abdemo(Gs3,R4,R5,N3,N4).
52
53abdemo([G|Gs1],R1,R3,N1,N2) :-
54 abresolve(G,R1,Gs2,R2), append(Gs2,Gs1,Gs3),
55 abdemo(Gs3,R2,R3,N1,N2).
56
57
58abresolve(terms_or_rels(A,F,T),R,Gs,R) :- axiom(releases(A,F,T),Gs).
59
60abresolve(terms_or_rels(A,F,T),R,Gs,R) :- axiom(terminates(A,F,T),Gs).
61
62abresolve(inits_or_rels(A,F,T),R,Gs,R) :- axiom(releases(A,F,T),Gs).
63
64abresolve(inits_or_rels(A,F,T),R,Gs,R) :- axiom(initiates(A,F,T),Gs).
65
66abresolve(happens(A,T),R1,Gs,R2) :- abresolve(happens(A,T,T),R1,Gs,R2).
67
68abresolve(happens(A,T1,T2),[HA,BA],[],[HA,BA]) :- member(happens(A,T1,T2),HA).
69
70abresolve(happens(A,T,T),[HA,BA],[],[[happens(A,T,T)|HA],BA]) :-
71 executable(A), skolemise(T).
72
73abresolve(before(X,Y),R,[],R) :- demo_before(X,Y,R).
74
75abresolve(before(X,Y),R1,[],R2) :-
76 \+ demo_before(X,Y,R1), \+ demo_beq(Y,X,R1), add_before(X,Y,R1,R2).
77
78abresolve(diff(X,Y),R,[],R) :- X \= Y.
79
80abresolve(G,R,Gs,R) :- axiom(G,Gs).
81
82
83abdemo_nafs([],R,R,N,N).
84
85abdemo_nafs([N|Ns],R1,R3,N1,N3) :-
86 abdemo_naf(N,R1,R2,N1,N2), abdemo_nafs(Ns,R2,R3,N2,N3).
87
88abdemo_naf([clipped(T1,F,T4)|Gs1],R1,R2,N1,N2) :-
89 findall(Gs3,
90 (abresolve(terms_or_rels(A,F,T2),R1,Gs2,R1),
91 abresolve(happens(A,T2,T3),R1,[],R1),
92 append([before(T1,T3),before(T2,T4)|Gs2],Gs1,Gs3)),Gss),
93 abdemo_nafs(Gss,R1,R2,N1,N2).
94
95abdemo_naf([declipped(T1,F,T4)|Gs1],R1,R2,N1,N2) :-
96 findall(Gs3,
97 (abresolve(inits_or_rels(A,F,T2),R1,Gs2,R1),
98 abresolve(happens(A,T2,T3),R1,[],R1),
99 append([before(T1,T3),before(T2,T4)|Gs2],Gs1,Gs3)),Gss),
100 abdemo_nafs(Gss,R1,R2,N1,N2).
101
102abdemo_naf([holds_at(F1,T)|Gs],R1,R2,N1,N2) :-
103 opposite(F1,F2), abdemo([holds_at(F2,T)],R1,R2,N1,N2).
104
105abdemo_naf([holds_at(F,T)|Gs],R1,R2,N1,N2) :-
106 abdemo_naf(Gs,R1,R2,N1,N2).
107
108abdemo_naf([before(X,Y)|Gs],R,R,N,N) :- X = Y.
109
110abdemo_naf([before(X,Y)|Gs],R,R,N,N) :- X \= Y, demo_before(Y,X,R).
111
112abdemo_naf([before(X,Y)|Gs],R1,R2,N1,N2) :-
113 X \= Y, \+ demo_before(Y,X,R1),
114 abdemo_naf(Gs,R1,R2,N1,N2).
115
116abdemo_naf([before(X,Y)|Gs],R1,R2,N,N) :-
117 X \= Y, \+ demo_before(Y,X,R1),
118 \+ demo_beq(X,Y,R1), add_before(Y,X,R1,R2).
119
120abdemo_naf([G|Gs1],R,R,N,N) :-
121 G \= clipped(T1,F,T2), G \= declipped(T1,F,T2), G \= holds_at(F,T),
122 G \= before(X,Y), \+ abresolve(G,R,Gs2,R).
123
124abdemo_naf([G1|Gs1],R1,R2,N1,N2) :-
125 G1 \= clipped(T1,F,T2), G1 \= declipped(T1,F,T2),
126 G1 \= holds_at(F,T), G1 \= before(X,Y),
127 findall(Gs3,(abresolve(G1,R1,Gs2,R1),append(Gs2,Gs1,Gs3)),Gss),
128 Gss \= [], abdemo_nafs(Gss,R1,R2,N1,N2).
129
130
131demo_before(X,Y,[HA,BA]) :- demo_before(X,Y,BA,[]).
132
133demo_before(0,Y,R,L) :- Y \= 0.
134
135demo_before(X,Y,R,L) :- X \= 0, member(before(X,Y),R).
136
137demo_before(X,Y,R,L) :- X \= 0, \+ member(before(X,Y),R), member(X,L).
138
139demo_before(X,Y,R,L) :-
140 X \= 0, \+ member(before(X,Y),R), \+ member(X,L),
141 member(before(X,Z),R), demo_before(Z,Y,R,[X|L]).
142
143
144demo_beq(X,X,R).
145
146demo_beq(X,Y,R) :- X \= Y, demo_before(X,Y,R).
147
148
149add_before(X,Y,[HA,BA]) :- member(before(X,Y),BA).
150
151add_before(X,Y,[HA,BA],[HA,[before(X,Y)|BA]]) :-
152 \+ member(before(X,Y),BA), \+ demo_beq(Y,X,[HA,BA]).
153
154
155add_neg(N,Ns,Ns) :- member(N,Ns).
156
157add_neg(N,Ns,[N|Ns]) :- \+ member(N,Ns).
158
159
160skolemise(T) :- gensym(t,T).
161
162
163opposite(neg(F),F).
164
165opposite(F1,neg(F1)) :- F1 \= neg(F2)