Hilbert II 0.04.04 - Changelog

What's new in Hilbert II 0.04.04:

August 1st, 2011

· We have now a parser that can read a propositional calculus proof written in ASCII text format and transform it into a QEDEQ XML NODE element. It was quickly hacked together but enables us to speed up proof integration. It can be accessed via GUI menu entry Tools / Proof Text to QEDEQ.
· A derivation rule has now a version too and name plus version must be unique (which is checked).
· We introduce a "brief" parameter for LaTeX and UTF-8 plugin to produce summary documents.
· And last but not least we included more propositions with formal proofs in qedeq_formal_logic_v1. Now even the tedious proofs for associativity can be found.

What's new in Hilbert II 0.04.03:

June 17th, 2011

· Introduces a new proof method: conditional proof. Based on the deduction theorem you can make an assumption and draw conclusions from it.

What's new in Hilbert II 0.04.01:

March 24th, 2011

· 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"


· 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

What's new in Hilbert II 0.03.12:

September 28th, 2010

· Not all the tests were done but it should be a quite stable release. Now a release comes in two main flavours: common and development. The development release contains also the software sources and metrics