-------------------------------------------------------------------------------
Release v3.0.0 - Thu Nov 11 12:55:48 EST 2004

+ This is the first public release

Changes to BNF
+ Reduced quantified variables to simple variables. The counted and typed
  options ...
    <qvariable>     ::= <typed variable> | <unsigned integer>:<typed variable>
    <typed variable>::= <variable> | <variable>:<variable type>
  ... may be revived in the future if there is demand.
+ Removed #... comments because Prolog can't deal wiith them.
+ Added <annotation> and removed <non-formula part>s

Changes to Problem Status Ontology
+ Moved Unknown into the Unsolved ontology
+ Added Assumed to Unsolved ontology
-------------------------------------------------------------------------------
Release v0.5.0 - Mon Sep 27 14:02:01 EDT 2004

Changes to BNF
+ equal/2 returned as a <theory atom> predicate
+ Moved old TPTP format stuff to end
+ Removed <language>s other than fof and cnf
+ Removed flexible formula types <formula>
+ Changed <logic formula> to <fol formula>
+ Renamed <rule name> to <inference rule>
+ Renamed <rule info> to <inference info>
+ Removed <replacement item> and <relevance item>
+ Added the missing <null> option for <formula selection> 

Changes to Problem Status Ontology
-------------------------------------------------------------------------------
Release v0.4.0 - Tue Sep 21 11:20:39 EDT 2004

Changes to BNF
+ Made a naming decision that this is the "new TPTP syntax (aka, the TSTP
  syntax)", and the old TPTP syntax is "the old TPTP syntax"
+ Separated out numbers and strings as special types of functions, so in the
  future they can be interpreted constants.
+ Added signs to numbers, and made <unsigned integer>
+ Removed assumption type - it is a synonym for hypothesis

Changes to Problem Status Ontology
+ Changed Unsolved to Unknown, to fit in with TPTP attitude.
+ Fixd what SatisfiabilityBijection, SatisfiabilityMapping, and  
  SatisfiabilityPreserving show about F (thanks to Larry Paulson)
-------------------------------------------------------------------------------
Release v0.3.0 - Tue Aug 24 12:09:14 EDT 2004

Changes to BNF
+ Added $ prefix to reserved constants $true and $false
+ Added infix equality, but still have to decide on "not equal" operator
+ Added the formula type "negated_conjecture"
+ Removed the formula type "assumption"

Changes to Problem Status Ontology
+ Undocumented
-------------------------------------------------------------------------------
Release v0.2.0 - Volker's book

Changes to BNF
+ Undocumented

Changes to Problem Status Ontology
+ Undocumented
-------------------------------------------------------------------------------
Release v0.1.0 - IJCAI 2004

+ This is the first beta release.
-------------------------------------------------------------------------------