13
14:-module(inf_closure,
15 [
16 inf_closure/3,
17 inf_closure/4
18 ]). 19
20:- dynamic
21 inf_closure/3. 22
23
25
26inf_closure(State, not(true), _, Fml) :- !,
27 set_satisfiable_flag(0),
28 store_inconsistent(Fml),
29 pdl_write(State), pdl_write(' ** Unsatisfiable [not(true)] ** '), pdl_write(not(true)), pdl_nl,
30 print_proof_step(State, '** Unsatisfiable **', ['clash',not(true)]),
31 fail.
32
39inf_closure(State, not(A), [A|_], Fml) :-
40 atomic(A),
41 !,
42 set_satisfiable_flag(0),
43 store_inconsistent(Fml),
44 pdl_write(State), pdl_write(' ** Unsatisfiable [not(A)-A] ** '), pdl_write(not(A)), pdl_write(' - '), pdl_write(A), pdl_nl,
45 print_proof_step(State, '** Unsatisfiable **', ['clash',not(A),A]),
46 fail.
47
48inf_closure(State, A, [not(A)|_], Fml) :-
49 atomic(A),
50 !,
51 set_satisfiable_flag(0),
52 store_inconsistent(Fml),
53 pdl_write(State), pdl_write(' ** Unsatisfiable [not(A)-A] ** '), pdl_write(not(A)), pdl_write(' - '), pdl_write(A), pdl_nl,
54 print_proof_step(State, '** Unsatisfiable **', ['clash',A,not(A)]),
55 fail.
56
57inf_closure(_, _, [], _) :- !.
58
59inf_closure(State, Term, [_|Set], Fml) :- !,
60 inf_closure(State, Term, Set, Fml)