6
7:-module(inf_closure,
8 [
9 inf_closure/3
10 ]). 11
12:- dynamic
13 inf_closure/3. 14
16
17inf_closure(State, not(true), _) :- !,
18 set_satisfiable_flag(0),
19 pdl_write(State), pdl_write(' ** Unsatisfiable [not(true)] ** '), pdl_write(not(true)), pdl_nl,
20 print_proof_step(State, '** Unsatisfiable **', ['clash',not(true)]),
21 fail.
22
23inf_closure(State, not(A), [A|_]) :- !,
24 set_satisfiable_flag(0),
25 pdl_write(State), pdl_write(' ** Unsatisfiable [not(A)-A] ** '), pdl_write(not(A)), pdl_write(' - '), pdl_write(A), pdl_nl,
26 print_proof_step(State, '** Unsatisfiable **', ['clash',not(A),A]),
27 fail.
28
29inf_closure(State, A, [not(A)|_]) :- !,
30 set_satisfiable_flag(0),
31 pdl_write(State), pdl_write(' ** Unsatisfiable [not(A)-A] ** '), pdl_write(A), pdl_write(' - '), pdl_write(not(A)), pdl_nl,
32 print_proof_step(State, '** Unsatisfiable **', ['clash',A,not(A)]),
33 fail.
34
35inf_closure(State, x(Y,A), [not(A)|_]) :- !,
36 set_satisfiable_flag(0),
37 pdl_write(State), pdl_write(' ** Unsatisfiable [x(Y,A)-not(A)] ** '), pdl_write(x(Y,A)), pdl_write(' - '), pdl_write(not(A)), pdl_nl,
38 print_proof_step(State, '** Unsatisfiable **', ['clash',x(Y,A),not(A)]),
39 fail.
40
41inf_closure(_, _, []) :- !.

47inf_closure(State, Term, [_|Set]) :- !,
48 inf_closure(State, Term, Set).
49
50