Hilbert II, Version 0.04.01 (gaffsie), 2011-03-04 21:45:39 Version History 0.04.01 ======= Functional Changes ------------------ Extensions ---------- - You can write formal proofs that use only the basic rules. These proofs can be seen in the text viewer and the generated LaTeX sources. They are still not checked for correctness. For an example see "sample\qedeq_sample3.xml" Fixed Bugs ---------- none Other Changes ------------- none XML Files ----------- Extensions ---------- math\qedeq_logic_v1.xml and math\qedeq_set_theory_v1.xml - further integration of Amrum notes (and some other) (made possible by the Ramada Cup in Hamburg Bergedorf ;-) project\qedeq_logic_language.xml - now with listing of basic formal proof rules project\qedeq_basic_concept.xml - some updates and extensions included sample\qedeq_sample3.xml - this file was added to demonstrate the new syntax for basic formal proofs Fixed Bugs ---------- math\qedeq_logic_v1.xml - math\qedeq_set_theory_v1.xml - theorem:powerProposition isSet(x) changed to isSet(x) Other Changes ------------- - rename of error sample XML files - label naming convention changed: labels are now parsed by ControlVisitor and have the following syntax: external module importLabel (external) node reference [importLabel].nodeLabel (external) node sub formula ref. [importLabel].nodeLabel/subFormula (external) node proof line ref. [[importLabel].nodeLabel!]lineLabel Source Code ----------- Extensions ---------- - DynamicDirectInterpreter uses now Latex2Utf8Parser to produce readable debug output - new constructor for dummy areas for SourceArea - various classes in different tiers for proof reason integration - Qedeq2Xml escapes XML entities now - new class Reference describes reference links Fixed Bugs ---------- - removed # in userinterface.html - loading from local file failed is now correctly noted - definedOperator is now set within QedeqVoBuilder Other Changes ------------- - InternalKernelServices (and implementations) must now provide an error code and text when creating errors - refactoring of error code and warnings: name convention implemented - FormulaChecker renamed into FormulaCheckerImpl and now we use a factory to produce instances of the new interface FormulaChecker, some methods are now in the new class FormulaUtility - KernelServices run now with QedeqBoFormalLogicCheckerPlugin which is more like a real plugin now - KernelServices (and implementations) loadModule and loadRequredModule doesn't throw a SourceFileExceptionList any longer - DefaultKernelQedeqBo's existence checker is now also set if logical check fails - refactoring of QedeqKernelSe: "se" package name inserted - SaxDefaultHandler accepts now only 20 XML errors and ignores the rest - copy QedeqKernelBoTest test data also to QedeqKernelXmlTest during build - TextPaneWindow uses now font "Monospaced" - StringUtility has new method to get a substring XSD --- Extensions ---------- - FORMAL_PROOF extended in following form ... [0..1] [1] ? ... [1..*] ... [0..1] And a proof line looks like: ... [1] ? ... [1] ? basic proof rules are (REASONTYPE) MP ADD RENAME SUBST_FREE SUBST_FUNVAR SUBST_PREDVAR EXISTENTIAL UNIVERSAL - EMAILTYPE has now a maximum length of 200 instead of 100 Fixed Bugs ---------- none Other Changes ------------- - documentation of classes to change if XSD changes