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	!