Hilbert II, Version 0.03.01 (mongaga), 2007-01-15 01:44:43 Version History 0.03.01 ======= Functional Changes ------------------ Extensions ---------- * check for "is well formed" added * XML export added * trace can be configured by editing "config/log4j.properties" change "FATAL" into "DEBUG" to get a detailed trace file in directory "log" Fixed Bugs ---------- * generated labels include chapter number Other Changes ------------- * "FormulaOrTerm" was split into "Formula" and "Term" XML Files ----------- Extensions ---------- * "qedeq_logic_language.xml" added Fixed Bugs ---------- * corrections because of changed XSD Other Changes ------------- Source Code ----------- Extensions ---------- * adapted visitor pattern implemented; see within package "control"; examples are QedeqBoFormalLogicChecker" and "Qedeq2Xml" * usage of log4j as trace library Fixed Bugs ---------- * empty LATEX nodes are correctly transfered * "kind" and "level" of "PROOF" are now transfered into "ProofVo" after extending "Proof" * refactoring to solve package cycles * "Specification.setLocationLIst()" removed Other Changes ------------- * rename of packages "*.elli" into "*.list" * new package "common" with generalized basic exception for this application * methods of "Trace" were renamed * "FormulaOrTerm" was split into "Formula" and "Term" this implies various changes * setter removed from "Specification" interface * visitor within old "*.elli" removed due to new visitor pattern usage * "*Vo" in "dto" package have now constructors or setters that require also "*Vo"s. * "handler" packages also work with "*Vo"s instead of the interfaces * "QedeqBoFactory "works creates now "*Vo" objects, nearly all "*Bo" in "bo.module" are removed to avoid duplicated code * adaptions to changed XSD, see below XSD --- Extensions ---------- Fixed Bugs ---------- Other Changes ------------- * element "LATEX" has no longer an "level" attribute TODOs ===== Later releases should solve the following problems: * error messages after check for logical consistence should contain more concrete problem description: e.g. in "30590: this predicate constant is unknown (at least for this argument number)" should occur the unknown name * Context2XPath must use visitor and Qedeq-Object to get XPath. This is necessary because an Atom (if it is the first in an ElementList) is always an attribute tag - therefore the XML element counting doesn't work (you have to subtract one if the first element is an Atom) * after solving the above problem the CheckException could be used directly to point to the error location * change Element creation in QedeqBoFactory (just comment code in and don't use Element.copy any longer) * consolidation of exceptions for restricted quantors: the definition all x phi(x): psi(y) <=> all x (phi(x) -> psi(y)) doesn`t match the current implementation because the restriction formula *must* contain the subject variable (see FormulaChecker) * implement wiki file output * implement txt file output * implement html file output * further improvement of LaTeX output for formulas; see "Proposition 1.7" in "qedeq_set_theory_v1_en.pdf" as an negative example