Hilbert II, Version 0.04.02 (gaffsie), 2011-05-01 07:19:24

Version History

0.04.02
=======

Functional Changes
------------------  

  Extensions
  ----------
  - these formal proofs can be checked. First successfully checked module:
    "sample/qedeq_sample3.xml"
  - new plugins to find propositional calculus proofs; these can be tested
    with "sample/qedeq_sample4.xml"
  - under "bin/" are now executables for console programs that search for
    simple propositional proofs 
  
  Fixed Bugs
  ----------
  none 

  Other Changes
  -------------
  - more reports under src/reports/


XML Files
-----------

  Extensions
  ----------
  - added "sample/qedeq_sample4.xml" which contains propositions without
    formal proofs; these proofs can be found by the new proof finder
  - added "doc/math/qedeq_propositional_v1.xml"

  Fixed Bugs
  ----------
  sample/qedeq_sample3.xml
  - our proof checker found some errors - these were corrected

  Other Changes
  -------------
  - definitions are now direct equivalences or identity relations, thus
    we can reference definition formulas in formal proofs directly, all
    XML files with definitions were changed accordingly
  - QEDEQ modules in "doc/" are not duplicated in "sample/" any longer


Source Code
-----------

  Extensions
  ----------
  - KernelNodeBo uses (and "implements") now new interface CheckLevel for
    providing informations if this node is well-formed or proved. 
    


  Fixed Bugs
  ----------
  - "LoadingStateDescriptions" text of "LOADING_FROM_LOCAL_FILE_FAILED"
    corrected
  - 


  Other Changes
  -------------
  - refactoring: split "FunctionDefinitionVo" into "FunctionDefinitionVo"
    and "InitialFunctionDefinitionVo"; accordingly "PredicateDefinitionVo";
    this lead to other changes through all tiers; now NodeType has two more
    implementations
  - FunctionConstant and PredicateConstant work now directly with subject
    variables and not only with their string atoms
  - relocation:   "math/qedeq_sample*" -> "sample"
  - ToolTip uses now UTF-8 capable font, so we get the current proof line
    formula when looking at the proof finder plugin in the thread window
  - VariableList was removed due to changes in defining new predicates and
    functions


XSD
---

  Extensions
  ----------
  none

  Fixed Bugs
  ----------
  none

  Other Changes
  -------------
  - element VARLIST was removed; new definition types were introduced; now
    we have either an initial predicate or function constant definition,
    that is a definition without a formula, or we have a definition that
    is an equivalence between the new predicate and a defining formula, or
    an identity relation between the new function and a defining term.