1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 2% 3% Copyright 2003, Renate Schmidt, University of Manchester 4% Modified 2009, Ullrich Hustadt, University of Liverpool 5% 6% Uses 7% 8% F, -F 9% ----- (F must be X-free) 10% clash 11% 12% X_{<a*>p}, -<a*>p 13% ----------------- 14% clash 15% 16%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 17 18:-module(inf_closure, 19 [ 20 inf_closure/3, 21 inf_closure/4 22 ]). 23 24:- dynamic 25 inf_closure/3. 26 27 28%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 29 30inf_closure(State, not(true), _, Fml) :- !, 31 set_satisfiable_flag(0), 32 store_inconsistent(Fml), 33 pdl_write(State), pdl_write(' ** Unsatisfiable [not(true)] ** '), pdl_write(not(true)), pdl_nl, 34 print_proof_step(State, '** Unsatisfiable **', ['clash',not(true)]), 35 fail. 36 37% Definitions 7 and 23 in (De Giacomo and Massacci, 2000) give different 38% conditions for the simplest form of an inconsistency: Definition 7 only 39% recognises an inconsistency between A and not(A) where A is atomic, 40% while Definition 23 recognises an inconsistency between F and not(F) where 41% F can be an arbitrary formula. However, in both cases F is not allowed to 42% contain an occurrence of X. 43inf_closure(State, not(A), [A|_], Fml) :- 44 x_free(A), 45 !, 46 set_satisfiable_flag(0), 47 store_inconsistent(Fml), 48 pdl_write(State), pdl_write(' ** Unsatisfiable [not(A)-A] ** '), pdl_write(not(A)), pdl_write(' - '), pdl_write(A), pdl_nl, 49 print_proof_step(State, '** Unsatisfiable **', ['clash',not(A),A]), 50 fail. 51 52inf_closure(State, A, [not(A)|_], Fml) :- 53 x_free(A), 54 !, 55 set_satisfiable_flag(0), 56 store_inconsistent(Fml), 57 pdl_write(State), pdl_write(' ** Unsatisfiable [not(A)-A] ** '), pdl_write(not(A)), pdl_write(' - '), pdl_write(A), pdl_nl, 58 print_proof_step(State, '** Unsatisfiable **', ['clash',A,not(A)]), 59 fail. 60 61% The following rule corresponds to condition 2 of Definition 23. 62inf_closure(State, x(Y,A), [not(A)|_], Fml) :- 63% atomic(A), 64 !, 65 set_satisfiable_flag(0), 66 store_inconsistent(Fml), 67 pdl_write(State), pdl_write(' ** Unsatisfiable [x(Y,A)-not(A)] ** '), pdl_write(x(Y,A)), pdl_write(' - '), pdl_write(not(A)), pdl_nl, 68 print_proof_step(State, '** Unsatisfiable **', ['clash',x(Y,A),not(A)]), 69 fail. 70 71inf_closure(_, _, [], _) :- !.

`inf_closure(State, x(_,_), _)`

:- !.`inf_closure(State, not(x(_,_)), _)`

:- !.

77inf_closure(State, Term, [_|Set], Fml) :- !, 78 inf_closure(State, Term, Set, Fml). 79 80 81x_free(dia(_P,F)) :- 82 x_free(F), 83 !. 84x_free(box(_P,F)) :- 85 x_free(F), 86 !. 87x_free(not(F)) :- 88 x_free(F), 89 !. 90x_free(or(F,G)) :- 91 x_free(F), 92 x_free(G), 93 !. 94x_free(and(F,G)) :- 95 x_free(F), 96 x_free(G), 97 !. 98x_free(A) :- 99 atomic(A), 100 !