All releases of Hilbert II
Release Notes: The icon for QEDEQ module status display now has different colors to represent different stages. Errors and warnings are visualized by decorator icons. Modules which are in progress are represented by animated icons. The clover and findbugs tools were updated. Process synchronization and process control were reorganized. This work is not finished yet, but nearly all module status changes are now caused by plugins. The process view shows more detail, and the chances for user interrupts were increased.
Release Notes: The context menu of text area fields include now "find": one can search for strings. The initial window size for text viewing was optimized; now the window should fit the screen more likely. Various test classes and tests were added. The test coverage percentage is now at 78.6%. A positive side effect was the discovery of some minor bugs, which were directly fixed. A few formal proofs were added to qedeq_formal_logic_v1.xml.
Release Notes: There is now a parser that can read a propositional calculus proof written in ASCII text format and transform it into a QEDEQ XML NODE element. This helps speed up proof integration. It can be accessed via GUI menu entry "Tools / Proof Text to QEDEQ". A derivation rule now also has a version, and the combination of name and version must be unique. A "brief" parameter was introduced for the LaTeX and UTF-8 plugin to produce summary documents. More propositions with formal proofs are included.
Release Notes: This release introduced a new proof method: conditional proof. Based on the deduction theorem, you can make an assumption and draw conclusions from it. It shows the unfolding of formal logic from axioms and inference rules to propositions of propositional calculus with formal proofs within qedeq_formal_logic_v1. The new proof method is also integrated in the proof checker. In the log output pane, messages are now better structured and more readable.
Release Notes: Formal proofs can be checked. The first successfully checked QEDEQ module is "sample/qedeq_sample3.xml". Another new plugin can find simple propositional calculus proofs. You can test that with "sample/qedeq_sample4.xml", which contains propositions without formal proofs. Also added was "doc/math/qedeq_propositional_v1.xml", which contains new axioms for propositional calculus. Propositions with formal proofs will be added to develop the complete propositional calculus. Definitions are now direct equivalences or identity relations, thus definition formulas can be referenced in formal proofs directly.
Release Notes: 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". The reference syntax was slightly changed and extended to include proof line references. Under the hood, the kernel services were reorganized to fit better to the plugin structure. The text viewer now uses the "Monospaced" font, and more UTF-8 characters are now displayed correctly. Also, some more proofs were added to the mathematical content.
Release Notes: New real plugins: "Show module as UTF-8 text", "Create UTF-8", and "Model Tester". The first ones are self-explanatory. The last one allows testing the validity of formulas in different finite models. The "four element model" is the approved model. It contains the following four elements: {}, {{}}, {{}, {{}}}, and {{{}}}. Together with the usual "element of" relation, it can fulfill almost all formulas of the logic and set theory script. Quite a few typos were fixed. There is a new process window to watch over plugin processes. The GUI has some other additions and changes.
Release Notes: A new about dialog that shows the system properties (they can also be copied into the clipboard). Warnings are now supported: LaTeX generation problems lead to warnings. The locations for LaTeX parsing problems are now precisely given. Proxy settings can now be done in the new designed preferences dialog. Uniqueness of class definition and identity operator definition is now checked. The LaTeX output for modules contains extra printed (\tt) QEDEQ references in clear text, so module authors can easily reference that node. The first pages of a new online help system are working.
Release Notes: After a huge amount of refactoring, the application is reorganized and the build process is new. Ant is still used, but Maven POMs are also provided. The Eclipse project directories are also included in the magnified src directory, as well as various reports. The Apache Commons library is used (e.g. for thread safe date formatting). The reorganized build process and new package subdivision have lead to a new project structure.
Release Notes: All error locations of a QEDEQ module are highlighted in the source viewer now. A click on the error list jumps to the error position. Only one application instance can be started. The Java version is checked during startup and must be at least 1.4.2. The loading sequence for referenced modules changed: now modules are tried according their enumeration. Application for the WebStart mode is now the subdirectory ".qedeq" within the home directory.
