Changes in Bliksem 1.10
-----------------------

There has been quite a long time between Bliksem 103, and Bliksem 110.
and I do (probably) not remember all the changes.

- Two bugs were fixed. Sometimes the number of variables in a clause was 
   incorrectly counted. (Given in the header of printed clauses)
   This was due to the fact that the number of variables was counted in the 
   substitution. When a literal is dropped, there may be more variables
   in the substitution, than in the resulting clause.

   Sometimes the a priori sorting of clauses missed maximal literals.

-  The derivation mechanism has been rewritten, mainly in order to make it 
   more modular. We observed no significant improvement on the ability to 
   find proofs.
   
-  The automode has been improved. Bliksem 1.10 is able to recognize the 
   decidable classes S+, E+, and the guarded fragment.

-  Bliksem 1.10 is able to output totally explicit proofs, which
   can be easily checked by other programs. In order to facilitate
   rechecking of proofs, Bliksem 1.10 is able to output its proofs
   in Prolog syntax. 

-  New (and not yet known) bugs were introduced, but at least the output
   of Bliksem can be checked. 


Bliksem 1.10a

-  When the flag prologoutput is set, it is checked whether or not a valid
   Bliksem identifier, is a valid Prolog identifier. If not, the identifier
   is properly quoted.


Bliksem 1.12 (July 4th  2000) 
-----------------------------

-  The static arrays termspace/termends [], clauses [], justifications [] are 
   now dynamically allocated. Their fixed sizes were the main source of 
   user complaints.


Oktober 2002
------------

-  The Bliksem project is terminated. 

August 2006 
-----------

- After reassesment, the health status from Bliksem is
  upgraded from 'dead' to 'in coma'.