10
11normalise([], []).
12normalise([Fml|FmlList], [NFFml|NFList]) :-
13 normalise(Fml, [], NFFml, Paths),
14 write(' '), print(NFFml), nl,
15 write('Paths = '), print(Paths), nl,
16 normalise(FmlList, NFList).
17
25
27
28normalise(implies(A, B), FreeV, NF, Paths) :- !,
29 normalise(or(not(A), B), FreeV, NF, Paths).
30
31normalise(not(implies(A, B)), FreeV, NF, Paths) :- !,
32 normalise(not(or(not(A), B)), FreeV, NF, Paths).
33
34normalise(conv(implies(A, B)), FreeV, NF, Paths) :- !,
35 normalise(or(not(conv(A)), conv(B)), FreeV, NF, Paths).
36
38
39normalise(implied(B, A), FreeV, NF, Paths) :- !,
40 normalise(or(not(A), B), FreeV, NF, Paths).
41
42normalise(not(implied(B, A)), FreeV, NF, Paths) :- !,
43 normalise(not(or(not(A), B)), FreeV, NF, Paths).
44
45normalise(conv(implied(B, A)), FreeV, NF, Paths) :- !,
46 normalise(or(not(conv(A)), conv(B)), FreeV, NF, Paths).
47
49
50normalise(equiv(A, B), FreeV, NF, Paths) :- !,
51 normalise(not(or(not(or(not(A), B)), not(or(not(B), A)))), FreeV, NF, Paths).
52
53normalise(not(equiv(A, B)), FreeV, NF, Paths) :- !,
54 normalise(or(not(or(not(A), B)), not(or(not(B), A))), FreeV, NF, Paths).
55
56normalise(conv(equiv(A, B)), FreeV, NF, Paths) :- !,
57 normalise(not(or(not(or(not(conv(A)), conv(B))), not(or(not(conv(A)), conv(B))))), FreeV, NF, Paths).
58
60
61normalise(box(R,A), FreeV, NF, Paths) :- !,
62 normalise(not(dia(R,not(A))), FreeV, NF, Paths).
63
64normalise(not(box(R,A)), FreeV, NF, Paths) :- !,
65 normalise(dia(R,not(A)), FreeV, NF, Paths).
66
68
69normalise(and(A,B), FreeV, NF, Paths) :- !,
70 normalise(not(or(not(A),not(B))), FreeV, NF, Paths).
71
72normalise(not(and(A,B)), FreeV, NF, Paths) :- !,
73 normalise(or(not(A),not(B)), FreeV, NF, Paths).
74
76
77normalise(false, FreeV, NF, Paths) :- !,
78 normalise(not(true), FreeV, NF, Paths).
79
80normalise(not(false), FreeV, NF, Paths) :- !,
81 normalise(true, FreeV, NF, Paths).
82
83normalise(conv(false), FreeV, NF, Paths) :- !,
84 normalise(not(true), FreeV, NF, Paths).
85
88
89normalise(id, FreeV, NF, Paths) :- !,
90 normalise(or(test('ID'),test(not('ID'))), FreeV, NF, Paths).
91
92normalise(dia(id,A), FreeV, NF, Paths) :- !,
93 normalise(A, FreeV, NF, Paths).
94
95normalise(dia(conv(id),A), FreeV, NF, Paths) :- !,
96 normalise(A, FreeV, NF, Paths).
97
98normalise(not(dia(id,A)), FreeV, NF, Paths) :- !,
99 normalise(not(A), FreeV, NF, Paths).
100
101normalise(not(dia(conv(id),A)), FreeV, NF, Paths) :- !,
102 normalise(not(A), FreeV, NF, Paths).
103
104normalise(comp(id,R), FreeV, NF, Paths) :- !,
105 normalise(R, FreeV, NF, Paths).
106
107normalise(comp(R,id), FreeV, NF, Paths) :- !,
108 normalise(R, FreeV, NF, Paths).
109
110normalise(comp(conv(id),R), FreeV, NF, Paths) :- !,
111 normalise(R, FreeV, NF, Paths).
112
113normalise(comp(R,conv(id)), FreeV, NF, Paths) :- !,
114 normalise(R, FreeV, NF, Paths).
115
116normalise(or(conv(id),R), FreeV, NF, Paths) :- !,
117 normalise(or(id,R), FreeV, NF, Paths).
118
119normalise(or(R,conv(id)), FreeV, NF, Paths) :- !,
120 normalise(or(R,id), FreeV, NF, Paths).
121
122normalise(star(id), FreeV, NF, Paths) :- !,
123 normalise(id, FreeV, NF, Paths).
124
125normalise(star(conv(id)), FreeV, NF, Paths) :- !,
126 normalise(id, FreeV, NF, Paths).
127
128normalise(conv(id), FreeV, NF, Paths) :- !,
129 normalise(id, FreeV, NF, Paths).
130
132
133normalise(plus(R), FreeV, NF, Paths) :- !,
134 normalise(comp(R,star(R)), FreeV, NF, Paths).
135
136normalise(conv(plus(R)), FreeV, NF, Paths) :- !,
137 normalise(conv(comp(R,star(R))), FreeV, NF, Paths).
138
141
143
144normalise(not(not(A)), FreeV, NF, Paths) :- !,
145 normalise(A, FreeV, NF, Paths).
146
147normalise(not(test(A)), FreeV, NF, Paths) :- !,
148 normalise(test(not(A)), FreeV, NF, Paths).
149
151
152normalise(or(A, A), FreeV, NF, Paths) :- !,
153 normalise(A, FreeV, NF, Paths).
154
155normalise(or(not(A), A), FreeV, NF, Paths) :- !,
156 normalise(true, FreeV, NF, Paths).
157
158normalise(or(A, not(A)), FreeV, NF, Paths) :- !,
159 normalise(true, FreeV, NF, Paths).
160
161normalise(or(_,true), FreeV, NF, Paths) :- !,
162 normalise(true, FreeV, NF, Paths).
163
164normalise(or(true,_), FreeV, NF, Paths) :- !,
165 normalise(true, FreeV, NF, Paths).
166
167normalise(or(A, not(true)), FreeV, NF, Paths) :- !,
168 normalise(A, FreeV, NF, Paths).
169
170normalise(or(not(true), A), FreeV, NF, Paths) :- !,
171 normalise(A, FreeV, NF, Paths).
172
173normalise(or(test(not(A)), test(A)), FreeV, NF, Paths) :- !,
174 normalise(test(true), FreeV, NF, Paths).
175
176normalise(or(test(A), test(not(A))), FreeV, NF, Paths) :- !,
177 normalise(test(true), FreeV, NF, Paths).
178
179normalise(or(A, test(not(true))), FreeV, NF, Paths) :- !,
180 normalise(A, FreeV, NF, Paths).
181
182normalise(or(test(not(true)), A), FreeV, NF, Paths) :- !,
183 normalise(A, FreeV, NF, Paths).
184
185normalise(or(A, B), FreeV, NF, Paths) :- !,
186 normalise(A, FreeV, NF1, Paths1),
187 normalise(B, FreeV, NF2, Paths2),
188 (Paths1 > Paths2 ->
189 OrdNF = or(NF2, NF1);
190 OrdNF = or(NF1, NF2)),
191 (A = NF1, B = NF2 ->
192 (NF = OrdNF,
193 Paths is Paths1 + Paths2);
194 normalise(OrdNF, FreeV, NF, Paths)).
195
197
198normalise(not(or(A, A)), FreeV, NF, Paths) :- !,
199 normalise(not(A), FreeV, NF, Paths).
200
201normalise(not(or(not(A), A)), FreeV, NF, Paths) :- !,
202 normalise(not(true), FreeV, NF, Paths).
203
204normalise(not(or(A, not(A))), FreeV, NF, Paths) :- !,
205 normalise(not(true), FreeV, NF, Paths).
206
207normalise(not(or(A,not(true))), FreeV, NF, Paths) :- !,
208 normalise(not(A), FreeV, NF, Paths).
209
210normalise(not(or(not(true),A)), FreeV, NF, Paths) :- !,
211 normalise(not(A), FreeV, NF, Paths).
212
213normalise(not(or(_, true)), FreeV, NF, Paths) :- !,
214 normalise(not(true), FreeV, NF, Paths).
215
216normalise(not(or(true, _)), FreeV, NF, Paths) :- !,
217 normalise(not(true), FreeV, NF, Paths).
218
219normalise(not(or(A,test(not(true)))), FreeV, NF, Paths) :- !,
220 normalise(not(A), FreeV, NF, Paths).
221
222normalise(not(or(test(not(true)),A)), FreeV, NF, Paths) :- !,
223 normalise(not(A), FreeV, NF, Paths).
224
225normalise(not(or(A, B)), FreeV, NF, Paths) :- !,
226 normalise(A, FreeV, NF1, Paths1),
227 normalise(B, FreeV, NF2, Paths2),
228 (Paths1 > Paths2 ->
229 OrdNF = not(or(NF2, NF1));
230 OrdNF = not(or(NF1, NF2))),
231 (A = NF1, B = NF2 ->
232 (NF = OrdNF,
233 Paths is Paths1 + Paths2);
234 normalise(OrdNF, FreeV, NF, Paths)).
235
237
238normalise(dia(_,not(true)), FreeV, NF, Paths) :- !,
239 normalise(not(true), FreeV, NF, Paths).
240
241normalise(dia(test(not(true)),_), FreeV, NF, Paths) :- !,
242 normalise(not(true), FreeV, NF, Paths).
243
244normalise(dia(test(true),A), FreeV, NF, Paths) :- !,
245 normalise(A, FreeV, NF, Paths).
246
247normalise(dia(comp(R,S),A), FreeV, NF, Paths) :- !,
248 normalise(dia(R,dia(S,A)), FreeV, NF, Paths).
249
250normalise(dia(or(R,S),A), FreeV, NF, Paths) :- !,
251 normalise(or(dia(R,A),dia(S,A)), FreeV, NF, Paths).
252
253normalise(dia(R,A), FreeV, NF, Paths) :- !,
254 normalise(R, FreeV, NF1, Paths1),
255 normalise(A, FreeV, NF2, Paths2),
256 (R = NF1, A = NF2 ->
257 (NF = dia(NF1, NF2),
258 Paths is Paths1 * Paths2);
259 normalise(dia(NF1, NF2), FreeV, NF, Paths)).
260
262
263normalise(not(dia(_,not(true))), FreeV, NF, Paths) :- !,
264 normalise(true, FreeV, NF, Paths).
265
266normalise(not(dia(not(true),_)), FreeV, NF, Paths) :- !,
267 normalise(true, FreeV, NF, Paths).
268
269normalise(not(dia(test(true),A)), FreeV, NF, Paths) :- !,
270 normalise(not(A), FreeV, NF, Paths).
271
272normalise(not(dia(comp(R,S),A)), FreeV, NF, Paths) :- !,
273 normalise(not(dia(R,dia(S,A))), FreeV, NF, Paths).
274
275normalise(not(dia(or(R,S),A)), FreeV, NF, Paths) :- !,
276 normalise(not(or(dia(R,A),dia(S,A))), FreeV, NF, Paths).
277
278normalise(not(dia(R,A)), FreeV, NF, Paths) :- !,
279 normalise(R, FreeV, NF1, Paths1),
280 normalise(A, FreeV, NF2, Paths2),
281 (R = NF1, A = NF2 ->
282 (NF = not(dia(NF1, NF2)),
283 Paths is Paths1 * Paths2);
284 normalise(not(dia(NF1, NF2)), FreeV, NF, Paths)).
285
287
290
291normalise(test(A), FreeV, NF, Paths) :- !,
292 normalise(A, FreeV, NF1, Paths1),
293 (A = NF1 ->
294 (NF = test(NF1),
295 Paths = Paths1); 296 normalise(test(NF1), FreeV, NF, Paths)).
297
299
300normalise(not(test(not(true))), FreeV, NF, Paths) :- !,
301 normalise(test(true), FreeV, NF, Paths).
302
303normalise(not(test(A)), FreeV, NF, Paths) :- !,
304 normalise(A, FreeV, NF1, Paths1),
305 (A = NF1 ->
306 (NF = not(test(NF1)),
307 Paths = Paths1); 308 normalise(not(test(NF1)), FreeV, NF, Paths)).
309
311
312normalise(comp(true,true), FreeV, NF, Paths) :- !,
313 normalise(true, FreeV, NF, Paths).
314
315normalise(comp(_,not(true)), FreeV, NF, Paths) :- !,
316 normalise(not(true), FreeV, NF, Paths).
317
318normalise(comp(not(true),_), FreeV, NF, Paths) :- !,
319 normalise(not(true), FreeV, NF, Paths).
320
321normalise(comp(test(true),R), FreeV, NF, Paths) :- !,
322 normalise(R, FreeV, NF, Paths).
323
324normalise(comp(R,test(true)), FreeV, NF, Paths) :- !,
325 normalise(R, FreeV, NF, Paths).
326
327normalise(comp(_,test(not(true))), FreeV, NF, Paths) :- !,
328 normalise(test(not(true)), FreeV, NF, Paths).
329
330normalise(comp(test(not(true)),_), FreeV, NF, Paths) :- !,
331 normalise(test(not(true)), FreeV, NF, Paths).
332
333normalise(comp(R,S), FreeV, NF, Paths) :- !,
334 normalise(R, FreeV, NF1, Paths1),
335 normalise(S, FreeV, NF2, Paths2),
336 (R = NF1, S = NF2 ->
337 (NF = comp(NF1, NF2),
338 Paths is Paths1 * Paths2);
339 normalise(comp(NF1, NF2), FreeV, NF, Paths)).
340
342
343normalise(not(comp(true,true)), FreeV, NF, Paths) :- !,
344 normalise(test(not(true)), FreeV, NF, Paths).
345
346normalise(not(comp(_,not(true))), FreeV, NF, Paths) :- !,
347 normalise(true, FreeV, NF, Paths).
348
349normalise(not(comp(not(true),_)), FreeV, NF, Paths) :- !,
350 normalise(true, FreeV, NF, Paths).
351
352normalise(not(comp(test(true),R)), FreeV, NF, Paths) :- !,
353 normalise(not(R), FreeV, NF, Paths).
354
355normalise(not(comp(R,test(true))), FreeV, NF, Paths) :- !,
356 normalise(not(R), FreeV, NF, Paths).
357
358normalise(not(comp(_,test(not(true)))), FreeV, NF, Paths) :- !,
359 normalise(test(true), FreeV, NF, Paths).
360
361normalise(not(comp(test(not(true)),_)), FreeV, NF, Paths) :- !,
362 normalise(test(true), FreeV, NF, Paths).
363
364normalise(not(comp(R,S)), FreeV, NF, Paths) :- !,
365 normalise(R, FreeV, NF1, Paths1),
366 normalise(S, FreeV, NF2, Paths2),
367 (R = NF1, S = NF2 ->
368 (NF = not(comp(NF1, NF2)),
369 Paths is Paths1 + Paths2);
370 normalise(not(comp(NF1, NF2)), FreeV, NF, Paths)).
371
373
374normalise(star(not(true)), FreeV, NF, Paths) :- !,
375 normalise(test(not(true)), FreeV, NF, Paths).
376
377normalise(star(true), FreeV, NF, Paths) :- !,
378 normalise(test(true), FreeV, NF, Paths).
379
380normalise(star(test(not(true))), FreeV, NF, Paths) :- !,
381 normalise(test(not(true)), FreeV, NF, Paths).
382
383normalise(star(test(true)), FreeV, NF, Paths) :- !,
384 normalise(test(true), FreeV, NF, Paths).
385
386normalise(star(A), FreeV, NF, Paths) :- !,
387 normalise(A, FreeV, NF1, Paths1),
388 (A = NF1 ->
389 (NF = star(NF1),
390 Paths = Paths1); 391 normalise(star(NF1), FreeV, NF, Paths)).
392
394
395normalise(conv(R), FreeV, NF, Paths) :- !,
396 normalise(R, FreeV, NF1, Paths1),
397 (R = NF1 ->
398 (NF = conv(NF1),
399 Paths = Paths1); 400 normalise(conv(NF1), FreeV, NF, Paths)).
401
404
405normalise(Lit, _, Lit, 1)