```    1/*
2
3   ABDUCTIVE EVENT CALCULUS
4
5   MURRAY SHANAHAN
6
7   Version 4.2
8   Stripped down, cut-free version, without comments
9
10   Written for LPA MacProlog 32
11
12*/
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),
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(b(T2,T3),R2,[],R3),
33     append(Gs2,Gs1,Gs3),
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),
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(b(T2,T3),R2,[],R3),
48     append(Gs2,Gs1,Gs3),
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(b(X,Y),R,[],R) :- demo_before(X,Y,R).
74
75abresolve(b(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([b(T1,T3),b(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([b(T1,T3),b(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([b(X,Y)|Gs],R,R,N,N) :- X = Y.
109
110abdemo_naf([b(X,Y)|Gs],R,R,N,N) :- X \= Y, demo_before(Y,X,R).
111
112abdemo_naf([b(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([b(X,Y)|Gs],R1,R2,N,N) :-
117     X \= Y, \+ demo_before(Y,X,R1),
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 \= b(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 \= b(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(b(X,Y),R).
136
137demo_before(X,Y,R,L) :- X \= 0, \+ member(b(X,Y),R), member(X,L).
138
139demo_before(X,Y,R,L) :-
140     X \= 0, \+ member(b(X,Y),R), \+ member(X,L),
141     member(b(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
150
152     \+ member(b(X,Y),BA), \+ demo_beq(Y,X,[HA,BA]).
153
154