Hilbert II, Version 0.04.02 (gaffsie), 20110501 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 wellformed 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 UTF8 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.