%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                    The CIFF Proof Procedure                     %%%
%%%        for Abductive Logic Programming with Constraints         %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Ulle Endriss (ue@doc.ic.ac.uk)

History:

30/11/2003: 
CIFF v1.3 published.
This is the first fully stable version of CIFF.

02/03/2004:
Optimisation: Moved some of the cuts in sat/7 and simplify_equalities/4 
to allow for tail recursion.

19/05/2004:
Guided propagation: Implemented a second variant of the propagation 
rule, which is now the default setting.

26/05/2004:
(1) Factoring can be switched on and off.
(2) Added "stats" debugging mode for proof statistics. 
(3) Added "short" debugging mode to display rule names alone.

20/08/2004:
(1) Early equality-constraint rewriting: Changed substitution rule 
for atoms to rewrite equalities as constraints straight away if they 
contain variables that are already known to be constraint variables.
This change can help avoid looping for some examples.
(2) Optimisation: Integrated unary disjunction rewriting into unfolding 
and logical simplification (based on work by Giacomo Terreni).
(3) Optimisation: Changed the rule order in sat/7 to give some of the 
simple rules that do not apply very often lower priority (based on
work by Giacomo Terreni).

26/08/2004:
Implemented the dynamic allowedness rule (DAR).

02/09/2004:
Corrected the quantification conditions (in relation to DAR) for
the substitution within implications.

03/09/2004: 
CIFF v2.0 published.

23/06/2005:
CIFF v3.0 published, including the following improvements and 
extensions (mostly implemented by Markos Hatzitaskos):
(1) Constraints in the answer are simplified more rigorously and 
projected onto the query and answer variables. 
(2) Negation-as-failure integrated (optional; see switch_naf/1).
(3) Basic GUI (optional; consult ciff-gui.pl and run setup/0). 
(4) Two new proof rules for formulas of the form "Constraints -> A".
(5) Completion of ALPs now integrated into ciff/3.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%