1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    2%
    3% Copyright 2003,    Renate Schmidt,  University of Manchester
    4%  Modified 2009-10, Ullrich Hustadt, University of Liverpool
    5%
    6% Uses
    7%
    8%   p, -p
    9%   ----- (p must be atomic and X-free)
   10%   clash
   11%
   12%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   13
   14:-module(inf_closure, 
   15    [
   16        inf_closure/3,
   17	inf_closure/4
   18    ]).   19
   20:- dynamic
   21        inf_closure/3.   22	
   23
   24%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   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
   33% Definitions 7 and 23 in (De Giacomo and Massacci, 2000) give different
   34% conditions for the simplest form of an inconsistency: Definition 7 only
   35% recognises an inconsistency between A and not(A) where A is atomic,
   36% while Definition 23 recognises an inconsistency between F and not(F) where
   37% F can be an arbitrary formula. However, using Definition 23, gives incorrect
   38% results for some formulae. Therefore, we only use Definition 7.
   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)