1:- dynamic contrapos_recorded/1. 2:- style_check(- singleton). 3:- style_check(- discontiguous). 4
6:- dynamic ex_not_diag/5. 7:- dynamic ex_tru_diag/5. 8:- dynamic prove_not_diag/4. 9:- dynamic prove_tru_diag/4. 10
12:- dynamic ex_not_val/5. 13:- dynamic ex_tru_val/5. 14:- dynamic prove_not_val/4. 15:- dynamic prove_tru_val/4. 16
18prove_tru_gate(x1, xor, _, _).
19ex_tru_gate(x1, xor, ths(A, A, B, B), _, ans(C, C)).
20
22prove_tru_gate(x2, xor, _, _).
23ex_tru_gate(x2, xor, ths(A, A, B, B), _, ans(C, C)).
24
26prove_tru_gate(a1, and, _, _).
27ex_tru_gate(a1, and, ths(A, A, B, B), _, ans(C, C)).
28
30prove_tru_gate(a2, and, _, _).
31ex_tru_gate(a2, and, ths(A, A, B, B), _, ans(C, C)).
32
34prove_tru_gate(o1, or, _, _).
35ex_tru_gate(o1, or, ths(A, A, B, B), _, ans(C, C)).
36
38prove_tru_conn(in(1, f1), in(1, x1), _, _).
39ex_tru_conn(in(1, f1), in(1, x1), ths(A, A, B, B), _, ans(C, C)).
40
42prove_tru_conn(in(1, f1), in(1, a1), _, _).
43ex_tru_conn(in(1, f1), in(1, a1), ths(A, A, B, B), _, ans(C, C)).
44
46prove_tru_conn(in(2, f1), in(2, x1), _, _).
47ex_tru_conn(in(2, f1), in(2, x1), ths(A, A, B, B), _, ans(C, C)).
48
50prove_tru_conn(in(2, f1), in(2, a1), _, _).
51ex_tru_conn(in(2, f1), in(2, a1), ths(A, A, B, B), _, ans(C, C)).
52
54prove_tru_conn(in(3, f1), in(2, x2), _, _).
55ex_tru_conn(in(3, f1), in(2, x2), ths(A, A, B, B), _, ans(C, C)).
56
58prove_tru_conn(in(3, f1), in(1, a2), _, _).
59ex_tru_conn(in(3, f1), in(1, a2), ths(A, A, B, B), _, ans(C, C)).
60
62prove_tru_conn(out(1, x1), in(1, x2), _, _).
63ex_tru_conn(out(1, x1), in(1, x2), ths(A, A, B, B), _, ans(C, C)).
64
66prove_tru_conn(out(1, x1), in(2, a2), _, _).
67ex_tru_conn(out(1, x1), in(2, a2), ths(A, A, B, B), _, ans(C, C)).
68
70prove_tru_conn(out(1, a1), in(2, o1), _, _).
71ex_tru_conn(out(1, a1), in(2, o1), ths(A, A, B, B), _, ans(C, C)).
72
74prove_tru_conn(out(1, a2), in(1, o1), _, _).
75ex_tru_conn(out(1, a2), in(1, o1), ths(A, A, B, B), _, ans(C, C)).
76
78prove_tru_conn(out(1, x2), out(1, f1), _, _).
79ex_tru_conn(out(1, x2), out(1, f1), ths(A, A, B, B), _, ans(C, C)).
80
82prove_tru_conn(out(1, o1), out(2, f1), _, _).
83ex_tru_conn(out(1, o1), out(2, f1), ths(A, A, B, B), _, ans(C, C)).
84
86prove_tru_val(in(_, _), anything, _, _).
87ex_tru_val(in(_, _), anything, ths(A, A, B, B), _, ans(C, C)).
88
90prove_tru_ok(A, B, _) :-
91 member(ok(A), B).
92ex_tru_ok(D, ths(A, A, B, B), _, ans(C, C)) :-
93 member(ok(D), A).
94ex_tru_ok(A, ths(B, [ok(A)|B], C, C), _, ans(D, D)) :-
95 variable_free(ok(A)),
96 \+ member(ok(A), B),
97 \+ prove_not_ok(A, [ok(A)|B], anc([], [])).
98ex_tru_ok(B, ths(A, A, C, [ok(B)|C]), _, ans(D, D)) :-
99 \+ variable_free(ok(B)).
100
102prove_tru_val(out(1, A), C, B, anc(D, E)) :-
103 prove_tru_ok(A,
104 B,
105 anc([val(out(1, A), C)|D], E)),
106 prove_tru_gate(A,
107 F,
108 B,
109 anc([val(out(1, A), C)|D], E)),
110 prove_tru_ttable(F,
111 G,
112 H,
113 C,
114 B,
115 anc([val(out(1, A), C)|D], E)),
116 prove_tru_val(in(1, A),
117 G,
118 B,
119 anc([val(out(1, A), C)|D], E)),
120 prove_tru_val(in(2, A),
121 H,
122 B,
123 anc([val(out(1, A), C)|D], E)).
124ex_tru_val(out(1, A), D, ths(B, U, C, W), anc(E, F), ans(G, Y)) :-
125 ex_tru_ok(A,
126 ths(B, H, C, I),
127 anc([val(out(1, A), D)|E], F),
128 ans(G, J)),
129 ex_tru_gate(A,
130 K,
131 ths(H, L, I, M),
132 anc([val(out(1, A), D)|E], F),
133 ans(J, N)),
134 ex_tru_ttable(K,
135 O,
136 S,
137 D,
138 ths(L, P, M, Q),
139 anc([val(out(1, A), D)|E], F),
140 ans(N, R)),
141 ex_tru_val(in(1, A),
142 O,
143 ths(P, T, Q, V),
144 anc([val(out(1, A), D)|E], F),
145 ans(R, X)),
146 ex_tru_val(in(2, A),
147 S,
148 ths(T, U, V, W),
149 anc([val(out(1, A), D)|E], F),
150 ans(X, Y)).
151prove_not_ok(A, B, anc(C, D)) :-
152 ( prove_tru_gate(A,
153 E,
154 B,
155 anc(C, [ok(A)|D])),
156 prove_tru_ttable(E,
157 F,
158 G,
159 H,
160 B,
161 anc(C, [ok(A)|D])),
162 prove_tru_val(in(1, A),
163 F,
164 B,
165 anc(C, [ok(A)|D])),
166 prove_tru_val(in(2, A),
167 G,
168 B,
169 anc(C, [ok(A)|D]))
170 ),
171 prove_not_val(out(1, A),
172 H,
173 B,
174 anc(C, [ok(A)|D])).
175ex_not_ok(A, ths(B, U, C, W), anc(D, E), ans(F, Y)) :-
176 ( ex_tru_gate(A,
177 G,
178 ths(B, H, C, I),
179 anc(D, [ok(A)|E]),
180 ans(F, J)),
181 ex_tru_ttable(G,
182 K,
183 O,
184 S,
185 ths(H, L, I, M),
186 anc(D, [ok(A)|E]),
187 ans(J, N)),
188 ex_tru_val(in(1, A),
189 K,
190 ths(L, P, M, Q),
191 anc(D, [ok(A)|E]),
192 ans(N, R)),
193 ex_tru_val(in(2, A),
194 O,
195 ths(P, T, Q, V),
196 anc(D, [ok(A)|E]),
197 ans(R, X))
198 ),
199 ex_not_val(out(1, A),
200 S,
201 ths(T, U, V, W),
202 anc(D, [ok(A)|E]),
203 ans(X, Y)).
204prove_not_gate(D, A, B, anc(C, E)) :-
205 ( prove_tru_ttable(A,
206 F,
207 G,
208 H,
209 B,
210 anc(C, [gate(D, A)|E])),
211 prove_tru_val(in(1, D),
212 F,
213 B,
214 anc(C, [gate(D, A)|E])),
215 prove_tru_val(in(2, D),
216 G,
217 B,
218 anc(C, [gate(D, A)|E]))
219 ),
220 prove_tru_ok(D, B, anc(C, [gate(D, A)|E])),
221 prove_not_val(out(1, D),
222 H,
223 B,
224 anc(C, [gate(D, A)|E])).
225ex_not_gate(E, A, ths(B, U, C, W), anc(D, F), ans(G, Y)) :-
226 ( ex_tru_ttable(A,
227 H,
228 L,
229 S,
230 ths(B, I, C, J),
231 anc(D, [gate(E, A)|F]),
232 ans(G, K)),
233 ex_tru_val(in(1, E),
234 H,
235 ths(I, M, J, N),
236 anc(D, [gate(E, A)|F]),
237 ans(K, O)),
238 ex_tru_val(in(2, E),
239 L,
240 ths(M, P, N, Q),
241 anc(D, [gate(E, A)|F]),
242 ans(O, R))
243 ),
244 ex_tru_ok(E,
245 ths(P, T, Q, V),
246 anc(D, [gate(E, A)|F]),
247 ans(R, X)),
248 ex_not_val(out(1, E),
249 S,
250 ths(T, U, V, W),
251 anc(D, [gate(E, A)|F]),
252 ans(X, Y)).
253prove_not_ttable(D, A, E, F, B, anc(C, G)) :-
254 ( prove_tru_val(in(1, H),
255 A,
256 B,
257 anc(C,
258 [ttable(D, A, E, F)|G])),
259 prove_tru_val(in(2, H),
260 E,
261 B,
262 anc(C,
263 [ttable(D, A, E, F)|G]))
264 ),
265 prove_tru_gate(H,
266 D,
267 B,
268 anc(C,
269 [ttable(D, A, E, F)|G])),
270 prove_tru_ok(H,
271 B,
272 anc(C,
273 [ttable(D, A, E, F)|G])),
274 prove_not_val(out(1, H),
275 F,
276 B,
277 anc(C,
278 [ttable(D, A, E, F)|G])).
279ex_not_ttable(E, A, F, G, ths(B, U, C, W), anc(D, H), ans(I, Y)) :-
280 ( ex_tru_val(in(1, J),
281 A,
282 ths(B, K, C, L),
283 anc(D,
284 [ttable(E, A, F, G)|H]),
285 ans(I, M)),
286 ex_tru_val(in(2, J),
287 F,
288 ths(K, N, L, O),
289 anc(D,
290 [ttable(E, A, F, G)|H]),
291 ans(M, P))
292 ),
293 ex_tru_gate(J,
294 E,
295 ths(N, Q, O, R),
296 anc(D, [ttable(E, A, F, G)|H]),
297 ans(P, S)),
298 ex_tru_ok(J,
299 ths(Q, T, R, V),
300 anc(D, [ttable(E, A, F, G)|H]),
301 ans(S, X)),
302 ex_not_val(out(1, J),
303 G,
304 ths(T, U, V, W),
305 anc(D,
306 [ttable(E, A, F, G)|H]),
307 ans(X, Y)).
308prove_not_val(in(1, A), D, B, anc(C, E)) :-
309 prove_tru_val(in(2, A),
310 F,
311 B,
312 anc(C, [val(in(1, A), D)|E])),
313 prove_tru_ttable(G,
314 D,
315 F,
316 H,
317 B,
318 anc(C, [val(in(1, A), D)|E])),
319 prove_tru_gate(A,
320 G,
321 B,
322 anc(C, [val(in(1, A), D)|E])),
323 prove_tru_ok(A,
324 B,
325 anc(C, [val(in(1, A), D)|E])),
326 prove_not_val(out(1, A),
327 H,
328 B,
329 anc(C, [val(in(1, A), D)|E])).
330ex_not_val(in(1, A), E, ths(B, U, C, W), anc(D, F), ans(G, Y)) :-
331 ex_tru_val(in(2, A),
332 H,
333 ths(B, I, C, J),
334 anc(D, [val(in(1, A), E)|F]),
335 ans(G, K)),
336 ex_tru_ttable(L,
337 E,
338 H,
339 S,
340 ths(I, M, J, N),
341 anc(D, [val(in(1, A), E)|F]),
342 ans(K, O)),
343 ex_tru_gate(A,
344 L,
345 ths(M, P, N, Q),
346 anc(D, [val(in(1, A), E)|F]),
347 ans(O, R)),
348 ex_tru_ok(A,
349 ths(P, T, Q, V),
350 anc(D, [val(in(1, A), E)|F]),
351 ans(R, X)),
352 ex_not_val(out(1, A),
353 S,
354 ths(T, U, V, W),
355 anc(D, [val(in(1, A), E)|F]),
356 ans(X, Y)).
357prove_not_val(in(2, A), D, B, anc(C, E)) :-
358 prove_tru_val(in(1, A),
359 F,
360 B,
361 anc(C, [val(in(2, A), D)|E])),
362 prove_tru_ttable(G,
363 F,
364 D,
365 H,
366 B,
367 anc(C, [val(in(2, A), D)|E])),
368 prove_tru_gate(A,
369 G,
370 B,
371 anc(C, [val(in(2, A), D)|E])),
372 prove_tru_ok(A,
373 B,
374 anc(C, [val(in(2, A), D)|E])),
375 prove_not_val(out(1, A),
376 H,
377 B,
378 anc(C, [val(in(2, A), D)|E])).
379ex_not_val(in(2, A), E, ths(B, U, C, W), anc(D, F), ans(G, Y)) :-
380 ex_tru_val(in(1, A),
381 H,
382 ths(B, I, C, J),
383 anc(D, [val(in(2, A), E)|F]),
384 ans(G, K)),
385 ex_tru_ttable(L,
386 H,
387 E,
388 S,
389 ths(I, M, J, N),
390 anc(D, [val(in(2, A), E)|F]),
391 ans(K, O)),
392 ex_tru_gate(A,
393 L,
394 ths(M, P, N, Q),
395 anc(D, [val(in(2, A), E)|F]),
396 ans(O, R)),
397 ex_tru_ok(A,
398 ths(P, T, Q, V),
399 anc(D, [val(in(2, A), E)|F]),
400 ans(R, X)),
401 ex_not_val(out(1, A),
402 S,
403 ths(T, U, V, W),
404 anc(D, [val(in(2, A), E)|F]),
405 ans(X, Y)).
406
408prove_tru_faulty(A, B, _) :-
409 member(faulty(A), B).
410ex_tru_faulty(D, ths(A, A, B, B), _, ans(C, C)) :-
411 member(faulty(D), A).
412ex_tru_faulty(A, ths(B, [faulty(A)|B], C, C), _, ans(D, D)) :-
413 variable_free(faulty(A)),
414 \+ member(faulty(A), B),
415 \+ prove_not_faulty(A, [faulty(A)|B], anc([], [])).
416ex_tru_faulty(B, ths(A, A, C, [faulty(B)|C]), _, ans(D, D)) :-
417 \+ variable_free(faulty(B)).
418
420prove_tru_val(out(1, A), C, B, anc(D, E)) :-
421 prove_tru_faulty(A,
422 B,
423 anc([val(out(1, A), C)|D], E)),
424 prove_tru_gate(A,
425 F,
426 B,
427 anc([val(out(1, A), C)|D], E)),
428 prove_tru_ttable(F,
429 H,
430 I,
431 G,
432 B,
433 anc([val(out(1, A), C)|D], E)),
434 prove_tru_opp(G,
435 C,
436 B,
437 anc([val(out(1, A), C)|D], E)),
438 prove_tru_val(in(1, A),
439 H,
440 B,
441 anc([val(out(1, A), C)|D], E)),
442 prove_tru_val(in(2, A),
443 I,
444 B,
445 anc([val(out(1, A), C)|D], E)).
446ex_tru_val(out(1, A), D, ths(B, Y, C, A1), anc(E, F), ans(G, C1)) :-
447 ex_tru_faulty(A,
448 ths(B, H, C, I),
449 anc([val(out(1, A), D)|E], F),
450 ans(G, J)),
451 ex_tru_gate(A,
452 K,
453 ths(H, L, I, M),
454 anc([val(out(1, A), D)|E], F),
455 ans(J, N)),
456 ex_tru_ttable(K,
457 S,
458 W,
459 O,
460 ths(L, P, M, Q),
461 anc([val(out(1, A), D)|E], F),
462 ans(N, R)),
463 ex_tru_opp(O,
464 D,
465 ths(P, T, Q, U),
466 anc([val(out(1, A), D)|E], F),
467 ans(R, V)),
468 ex_tru_val(in(1, A),
469 S,
470 ths(T, X, U, Z),
471 anc([val(out(1, A), D)|E], F),
472 ans(V, B1)),
473 ex_tru_val(in(2, A),
474 W,
475 ths(X, Y, Z, A1),
476 anc([val(out(1, A), D)|E], F),
477 ans(B1, C1)).
478prove_not_faulty(A, B, anc(C, D)) :-
479 ( prove_tru_gate(A,
480 E,
481 B,
482 anc(C, [faulty(A)|D])),
483 prove_tru_ttable(E,
484 G,
485 H,
486 F,
487 B,
488 anc(C, [faulty(A)|D])),
489 prove_tru_opp(F,
490 I,
491 B,
492 anc(C, [faulty(A)|D])),
493 prove_tru_val(in(1, A),
494 G,
495 B,
496 anc(C, [faulty(A)|D])),
497 prove_tru_val(in(2, A),
498 H,
499 B,
500 anc(C, [faulty(A)|D]))
501 ),
502 prove_not_val(out(1, A),
503 I,
504 B,
505 anc(C, [faulty(A)|D])).
506ex_not_faulty(A, ths(B, Y, C, A1), anc(D, E), ans(F, C1)) :-
507 ( ex_tru_gate(A,
508 G,
509 ths(B, H, C, I),
510 anc(D, [faulty(A)|E]),
511 ans(F, J)),
512 ex_tru_ttable(G,
513 O,
514 S,
515 K,
516 ths(H, L, I, M),
517 anc(D, [faulty(A)|E]),
518 ans(J, N)),
519 ex_tru_opp(K,
520 W,
521 ths(L, P, M, Q),
522 anc(D, [faulty(A)|E]),
523 ans(N, R)),
524 ex_tru_val(in(1, A),
525 O,
526 ths(P, T, Q, U),
527 anc(D, [faulty(A)|E]),
528 ans(R, V)),
529 ex_tru_val(in(2, A),
530 S,
531 ths(T, X, U, Z),
532 anc(D, [faulty(A)|E]),
533 ans(V, B1))
534 ),
535 ex_not_val(out(1, A),
536 W,
537 ths(X, Y, Z, A1),
538 anc(D, [faulty(A)|E]),
539 ans(B1, C1)).
540prove_not_gate(D, A, B, anc(C, E)) :-
541 ( prove_tru_ttable(A,
542 G,
543 H,
544 F,
545 B,
546 anc(C, [gate(D, A)|E])),
547 prove_tru_opp(F,
548 I,
549 B,
550 anc(C, [gate(D, A)|E])),
551 prove_tru_val(in(1, D),
552 G,
553 B,
554 anc(C, [gate(D, A)|E])),
555 prove_tru_val(in(2, D),
556 H,
557 B,
558 anc(C, [gate(D, A)|E]))
559 ),
560 prove_tru_faulty(D,
561 B,
562 anc(C, [gate(D, A)|E])),
563 prove_not_val(out(1, D),
564 I,
565 B,
566 anc(C, [gate(D, A)|E])).
567ex_not_gate(E, A, ths(B, Y, C, A1), anc(D, F), ans(G, C1)) :-
568 ( ex_tru_ttable(A,
569 L,
570 P,
571 H,
572 ths(B, I, C, J),
573 anc(D, [gate(E, A)|F]),
574 ans(G, K)),
575 ex_tru_opp(H,
576 W,
577 ths(I, M, J, N),
578 anc(D, [gate(E, A)|F]),
579 ans(K, O)),
580 ex_tru_val(in(1, E),
581 L,
582 ths(M, Q, N, R),
583 anc(D, [gate(E, A)|F]),
584 ans(O, S)),
585 ex_tru_val(in(2, E),
586 P,
587 ths(Q, T, R, U),
588 anc(D, [gate(E, A)|F]),
589 ans(S, V))
590 ),
591 ex_tru_faulty(E,
592 ths(T, X, U, Z),
593 anc(D, [gate(E, A)|F]),
594 ans(V, B1)),
595 ex_not_val(out(1, E),
596 W,
597 ths(X, Y, Z, A1),
598 anc(D, [gate(E, A)|F]),
599 ans(B1, C1)).
600prove_not_ttable(D, E, F, A, B, anc(C, G)) :-
601 ( prove_tru_opp(A,
602 I,
603 B,
604 anc(C,
605 [ttable(D, E, F, A)|G])),
606 prove_tru_val(in(1, H),
607 E,
608 B,
609 anc(C,
610 [ttable(D, E, F, A)|G])),
611 prove_tru_val(in(2, H),
612 F,
613 B,
614 anc(C,
615 [ttable(D, E, F, A)|G]))
616 ),
617 prove_tru_gate(H,
618 D,
619 B,
620 anc(C,
621 [ttable(D, E, F, A)|G])),
622 prove_tru_faulty(H,
623 B,
624 anc(C,
625 [ttable(D, E, F, A)|G])),
626 prove_not_val(out(1, H),
627 I,
628 B,
629 anc(C,
630 [ttable(D, E, F, A)|G])).
631ex_not_ttable(E, F, G, A, ths(B, Y, C, A1), anc(D, H), ans(I, C1)) :-
632 ( ex_tru_opp(A,
633 W,
634 ths(B, J, C, K),
635 anc(D,
636 [ttable(E, F, G, A)|H]),
637 ans(I, L)),
638 ex_tru_val(in(1, M),
639 F,
640 ths(J, N, K, O),
641 anc(D,
642 [ttable(E, F, G, A)|H]),
643 ans(L, P)),
644 ex_tru_val(in(2, M),
645 G,
646 ths(N, Q, O, R),
647 anc(D,
648 [ttable(E, F, G, A)|H]),
649 ans(P, S))
650 ),
651 ex_tru_gate(M,
652 E,
653 ths(Q, T, R, U),
654 anc(D, [ttable(E, F, G, A)|H]),
655 ans(S, V)),
656 ex_tru_faulty(M,
657 ths(T, X, U, Z),
658 anc(D,
659 [ttable(E, F, G, A)|H]),
660 ans(V, B1)),
661 ex_not_val(out(1, M),
662 W,
663 ths(X, Y, Z, A1),
664 anc(D,
665 [ttable(E, F, G, A)|H]),
666 ans(B1, C1)).
667prove_not_opp(C, D, A, anc(B, E)) :-
668 ( prove_tru_val(in(1, F),
669 G,
670 A,
671 anc(B, [opp(C, D)|E])),
672 prove_tru_val(in(2, F),
673 H,
674 A,
675 anc(B, [opp(C, D)|E]))
676 ),
677 prove_tru_ttable(I,
678 G,
679 H,
680 C,
681 A,
682 anc(B, [opp(C, D)|E])),
683 prove_tru_gate(F,
684 I,
685 A,
686 anc(B, [opp(C, D)|E])),
687 prove_tru_faulty(F,
688 A,
689 anc(B, [opp(C, D)|E])),
690 prove_not_val(out(1, F),
691 D,
692 A,
693 anc(B, [opp(C, D)|E])).
694ex_not_opp(D, E, ths(A, Y, B, A1), anc(C, F), ans(G, C1)) :-
695 ( ex_tru_val(in(1, H),
696 L,
697 ths(A, I, B, J),
698 anc(C, [opp(D, E)|F]),
699 ans(G, K)),
700 ex_tru_val(in(2, H),
701 M,
702 ths(I, N, J, O),
703 anc(C, [opp(D, E)|F]),
704 ans(K, P))
705 ),
706 ex_tru_ttable(Q,
707 L,
708 M,
709 D,
710 ths(N, R, O, S),
711 anc(C, [opp(D, E)|F]),
712 ans(P, T)),
713 ex_tru_gate(H,
714 Q,
715 ths(R, U, S, V),
716 anc(C, [opp(D, E)|F]),
717 ans(T, W)),
718 ex_tru_faulty(H,
719 ths(U, X, V, Z),
720 anc(C, [opp(D, E)|F]),
721 ans(W, B1)),
722 ex_not_val(out(1, H),
723 E,
724 ths(X, Y, Z, A1),
725 anc(C, [opp(D, E)|F]),
726 ans(B1, C1)).
727prove_not_val(in(1, A), D, B, anc(C, E)) :-
728 prove_tru_val(in(2, A),
729 F,
730 B,
731 anc(C, [val(in(1, A), D)|E])),
732 prove_tru_opp(G,
733 I,
734 B,
735 anc(C, [val(in(1, A), D)|E])),
736 prove_tru_ttable(H,
737 D,
738 F,
739 G,
740 B,
741 anc(C, [val(in(1, A), D)|E])),
742 prove_tru_gate(A,
743 H,
744 B,
745 anc(C, [val(in(1, A), D)|E])),
746 prove_tru_faulty(A,
747 B,
748 anc(C, [val(in(1, A), D)|E])),
749 prove_not_val(out(1, A),
750 I,
751 B,
752 anc(C, [val(in(1, A), D)|E])).
753ex_not_val(in(1, A), E, ths(B, Y, C, A1), anc(D, F), ans(G, C1)) :-
754 ex_tru_val(in(2, A),
755 K,
756 ths(B, H, C, I),
757 anc(D, [val(in(1, A), E)|F]),
758 ans(G, J)),
759 ex_tru_opp(L,
760 W,
761 ths(H, M, I, N),
762 anc(D, [val(in(1, A), E)|F]),
763 ans(J, O)),
764 ex_tru_ttable(P,
765 E,
766 K,
767 L,
768 ths(M, Q, N, R),
769 anc(D, [val(in(1, A), E)|F]),
770 ans(O, S)),
771 ex_tru_gate(A,
772 P,
773 ths(Q, T, R, U),
774 anc(D, [val(in(1, A), E)|F]),
775 ans(S, V)),
776 ex_tru_faulty(A,
777 ths(T, X, U, Z),
778 anc(D, [val(in(1, A), E)|F]),
779 ans(V, B1)),
780 ex_not_val(out(1, A),
781 W,
782 ths(X, Y, Z, A1),
783 anc(D, [val(in(1, A), E)|F]),
784 ans(B1, C1)).
785prove_not_val(in(2, A), D, B, anc(C, E)) :-
786 prove_tru_val(in(1, A),
787 F,
788 B,
789 anc(C, [val(in(2, A), D)|E])),
790 prove_tru_opp(G,
791 I,
792 B,
793 anc(C, [val(in(2, A), D)|E])),
794 prove_tru_ttable(H,
795 F,
796 D,
797 G,
798 B,
799 anc(C, [val(in(2, A), D)|E])),
800 prove_tru_gate(A,
801 H,
802 B,
803 anc(C, [val(in(2, A), D)|E])),
804 prove_tru_faulty(A,
805 B,
806 anc(C, [val(in(2, A), D)|E])),
807 prove_not_val(out(1, A),
808 I,
809 B,
810 anc(C, [val(in(2, A), D)|E])).
811ex_not_val(in(2, A), E, ths(B, Y, C, A1), anc(D, F), ans(G, C1)) :-
812 ex_tru_val(in(1, A),
813 K,
814 ths(B, H, C, I),
815 anc(D, [val(in(2, A), E)|F]),
816 ans(G, J)),
817 ex_tru_opp(L,
818 W,
819 ths(H, M, I, N),
820 anc(D, [val(in(2, A), E)|F]),
821 ans(J, O)),
822 ex_tru_ttable(P,
823 K,
824 E,
825 L,
826 ths(M, Q, N, R),
827 anc(D, [val(in(2, A), E)|F]),
828 ans(O, S)),
829 ex_tru_gate(A,
830 P,
831 ths(Q, T, R, U),
832 anc(D, [val(in(2, A), E)|F]),
833 ans(S, V)),
834 ex_tru_faulty(A,
835 ths(T, X, U, Z),
836 anc(D, [val(in(2, A), E)|F]),
837 ans(V, B1)),
838 ex_not_val(out(1, A),
839 W,
840 ths(X, Y, Z, A1),
841 anc(D, [val(in(2, A), E)|F]),
842 ans(B1, C1)).
843
845prove_not_ok(A, B, anc(C, D)) :-
846 prove_tru_faulty(A, B, anc(C, [ok(A)|D])).
847ex_not_ok(A, B, anc(C, D), E) :-
848 ex_tru_faulty(A, B, anc(C, [ok(A)|D]), E).
849prove_not_faulty(A, B, anc(C, D)) :-
850 prove_tru_ok(A, B, anc(C, [faulty(A)|D])).
851ex_not_faulty(A, B, anc(C, D), E) :-
852 ex_tru_ok(A, B, anc(C, [faulty(A)|D]), E).
853
855prove_tru_opp(on, off, _, _).
856ex_tru_opp(on, off, ths(A, A, B, B), _, ans(C, C)).
857
859prove_tru_opp(off, on, _, _).
860ex_tru_opp(off, on, ths(A, A, B, B), _, ans(C, C)).
861
863prove_tru_ttable(and, on, on, on, _, _).
864ex_tru_ttable(and, on, on, on, ths(A, A, B, B), _, ans(C, C)).
865
867prove_tru_ttable(and, off, anything, off, _, _).
868ex_tru_ttable(and, off, anything, off, ths(A, A, B, B), _, ans(C, C)).
869
871prove_tru_ttable(and, anything, off, off, _, _).
872ex_tru_ttable(and, anything, off, off, ths(A, A, B, B), _, ans(C, C)).
873
875prove_tru_ttable(or, off, off, off, _, _).
876ex_tru_ttable(or, off, off, off, ths(A, A, B, B), _, ans(C, C)).
877
879prove_tru_ttable(or, on, anything, on, _, _).
880ex_tru_ttable(or, on, anything, on, ths(A, A, B, B), _, ans(C, C)).
881
883prove_tru_ttable(or, anything, on, on, _, _).
884ex_tru_ttable(or, anything, on, on, ths(A, A, B, B), _, ans(C, C)).
885
887prove_tru_ttable(xor, off, on, on, _, _).
888ex_tru_ttable(xor, off, on, on, ths(A, A, B, B), _, ans(C, C)).
889
891prove_tru_ttable(xor, off, off, off, _, _).
892ex_tru_ttable(xor, off, off, off, ths(A, A, B, B), _, ans(C, C)).
893
895prove_tru_ttable(xor, on, A, B, C, anc(D, E)) :-
896 prove_tru_opp(A,
897 B,
898 C,
899 anc([ttable(xor, on, A, B)|D], E)).
900ex_tru_ttable(xor, on, A, B, C, anc(D, E), F) :-
901 ex_tru_opp(A,
902 B,
903 C,
904 anc([ttable(xor, on, A, B)|D], E),
905 F).
906prove_not_opp(A, B, C, anc(D, E)) :-
907 prove_not_ttable((xor),
908 on,
909 A,
910 B,
911 C,
912 anc(D, [opp(A, B)|E])).
913ex_not_opp(A, B, C, anc(D, E), F) :-
914 ex_not_ttable((xor),
915 on,
916 A,
917 B,
918 C,
919 anc(D, [opp(A, B)|E]),
920 F).
921
923prove_tru_val(C, A, B, anc(D, E)) :-
924 prove_tru_ne(A,
925 anything,
926 B,
927 anc([val(C, A)|D], E)),
928 prove_tru_conn(F,
929 C,
930 B,
931 anc([val(C, A)|D], E)),
932 prove_tru_val(F,
933 A,
934 B,
935 anc([val(C, A)|D], E)).
936ex_tru_val(D, A, ths(B, M, C, O), anc(E, F), ans(G, Q)) :-
937 ex_tru_ne(A,
938 anything,
939 ths(B, H, C, I),
940 anc([val(D, A)|E], F),
941 ans(G, J)),
942 ex_tru_conn(K,
943 D,
944 ths(H, L, I, N),
945 anc([val(D, A)|E], F),
946 ans(J, P)),
947 ex_tru_val(K,
948 A,
949 ths(L, M, N, O),
950 anc([val(D, A)|E], F),
951 ans(P, Q)).
952prove_not_ne(C, anything, A, anc(B, D)) :-
953 ( prove_tru_conn(E,
954 F,
955 A,
956 anc(B, [ne(C, anything)|D])),
957 prove_tru_val(E,
958 C,
959 A,
960 anc(B, [ne(C, anything)|D]))
961 ),
962 prove_not_val(F,
963 C,
964 A,
965 anc(B, [ne(C, anything)|D])).
966ex_not_ne(D, anything, ths(A, M, B, O), anc(C, E), ans(F, Q)) :-
967 ( ex_tru_conn(G,
968 K,
969 ths(A, H, B, I),
970 anc(C, [ne(D, anything)|E]),
971 ans(F, J)),
972 ex_tru_val(G,
973 D,
974 ths(H, L, I, N),
975 anc(C, [ne(D, anything)|E]),
976 ans(J, P))
977 ),
978 ex_not_val(K,
979 D,
980 ths(L, M, N, O),
981 anc(C, [ne(D, anything)|E]),
982 ans(P, Q)).
983prove_not_conn(A, D, B, anc(C, E)) :-
984 prove_tru_val(A,
985 F,
986 B,
987 anc(C, [conn(A, D)|E])),
988 prove_tru_ne(F,
989 anything,
990 B,
991 anc(C, [conn(A, D)|E])),
992 prove_not_val(D,
993 F,
994 B,
995 anc(C, [conn(A, D)|E])).
996ex_not_conn(A, E, ths(B, M, C, O), anc(D, F), ans(G, Q)) :-
997 ex_tru_val(A,
998 H,
999 ths(B, I, C, J),
1000 anc(D, [conn(A, E)|F]),
1001 ans(G, K)),
1002 ex_tru_ne(H,
1003 anything,
1004 ths(I, L, J, N),
1005 anc(D, [conn(A, E)|F]),
1006 ans(K, P)),
1007 ex_not_val(E,
1008 H,
1009 ths(L, M, N, O),
1010 anc(D, [conn(A, E)|F]),
1011 ans(P, Q)).
1012prove_not_val(A, D, B, anc(C, E)) :-
1013 prove_tru_conn(A,
1014 F,
1015 B,
1016 anc(C, [val(A, D)|E])),
1017 prove_tru_ne(D,
1018 anything,
1019 B,
1020 anc(C, [val(A, D)|E])),
1021 prove_not_val(F,
1022 D,
1023 B,
1024 anc(C, [val(A, D)|E])).
1025ex_not_val(A, E, ths(B, M, C, O), anc(D, F), ans(G, Q)) :-
1026 ex_tru_conn(A,
1027 K,
1028 ths(B, H, C, I),
1029 anc(D, [val(A, E)|F]),
1030 ans(G, J)),
1031 ex_tru_ne(E,
1032 anything,
1033 ths(H, L, I, N),
1034 anc(D, [val(A, E)|F]),
1035 ans(J, P)),
1036 ex_not_val(K,
1037 E,
1038 ths(L, M, N, O),
1039 anc(D, [val(A, E)|F]),
1040 ans(P, Q)).
1041
1043ex_tru_ne(D, E, ths(A, A, B, B), _, ans(C, C)) :-
1044 ne(D, E).
1045prove_tru_ne(A, B, _, _) :-
1046 ne(A, B).
1047
1049
1051prove_not_val(A, off, B, anc(C, D)) :-
1052 prove_tru_val(A, on, B, anc(C, [val(A, off)|D])).
1053ex_not_val(A, off, B, anc(C, D), E) :-
1054 ex_tru_val(A,
1055 on,
1056 B,
1057 anc(C, [val(A, off)|D]),
1058 E).
1059prove_not_val(A, on, B, anc(C, D)) :-
1060 prove_tru_val(A, off, B, anc(C, [val(A, on)|D])).
1061ex_not_val(A, on, B, anc(C, D), E) :-
1062 ex_tru_val(A,
1063 off,
1064 B,
1065 anc(C, [val(A, on)|D]),
1066 E).
1067
1069prove_tru_diag(A, C, B, anc(D, E)) :-
1070 prove_tru_val(out(1, f1),
1071 A,
1072 B,
1073 anc([diag(A, C)|D], E)),
1074 prove_tru_val(out(2, f1),
1075 C,
1076 B,
1077 anc([diag(A, C)|D], E)).
1078ex_tru_diag(A, D, ths(B, I, C, K), anc(E, F), ans(G, M)) :-
1079 ex_tru_val(out(1, f1),
1080 A,
1081 ths(B, H, C, J),
1082 anc([diag(A, D)|E], F),
1083 ans(G, L)),
1084 ex_tru_val(out(2, f1),
1085 D,
1086 ths(H, I, J, K),
1087 anc([diag(A, D)|E], F),
1088 ans(L, M)).
1089prove_not_val(out(1, f1), C, A, anc(B, D)) :-
1090 prove_tru_val(out(2, f1),
1091 E,
1092 A,
1093 anc(B, [val(out(1, f1), C)|D])),
1094 prove_not_diag(C,
1095 E,
1096 A,
1097 anc(B, [val(out(1, f1), C)|D])).
1098ex_not_val(out(1, f1), D, ths(A, I, B, K), anc(C, E), ans(F, M)) :-
1099 ex_tru_val(out(2, f1),
1100 G,
1101 ths(A, H, B, J),
1102 anc(C, [val(out(1, f1), D)|E]),
1103 ans(F, L)),
1104 ex_not_diag(D,
1105 G,
1106 ths(H, I, J, K),
1107 anc(C, [val(out(1, f1), D)|E]),
1108 ans(L, M)).
1109prove_not_val(out(2, f1), C, A, anc(B, D)) :-
1110 prove_tru_val(out(1, f1),
1111 E,
1112 A,
1113 anc(B, [val(out(2, f1), C)|D])),
1114 prove_not_diag(E,
1115 C,
1116 A,
1117 anc(B, [val(out(2, f1), C)|D])).
1118ex_not_val(out(2, f1), D, ths(A, I, B, K), anc(C, E), ans(F, M)) :-
1119 ex_tru_val(out(1, f1),
1120 G,
1121 ths(A, H, B, J),
1122 anc(C, [val(out(2, f1), D)|E]),
1123 ans(F, L)),
1124 ex_not_diag(G,
1125 D,
1126 ths(H, I, J, K),
1127 anc(C, [val(out(2, f1), D)|E]),
1128 ans(L, M))