Hilbert II - QEDEQ / News: Recent posts

The new release 0.04.07 concentrates on stabilizing the processing structure. Increasing the test coverage and bug fixing were the other focus.

The road goes on to 0.04.06. Most visual change is the icon usage for QEDEQ module status display. We use gray for not yet worked on modules, purple for loaded modules, cyan for loaded all required modules, red orange for all well formed modules und yellow for all fully proved modules. Errors and warnings are visualized by decorator icons. Modules which are in progress are represented by animated icons.
We did some tool updates (clover, findbugs). The main theme was the reorganization of process synchronization and process control. This work is not finished yet but nearly all module status changes are caused by (internal) plugins now. The process view shows more details and the chances for user interrupts were increased.

we are back again and have formal proofs for some more propositions
A -> (B -> (A & B)), ((A -> B) & (B -> C)) -> (A -> C), ((A -> C) & (B -> C)) -> ((A ∨ B) -> C), ((A & B) v C) -> ((A v C) & (B v C)), ((A ∨ C) & (B ∨ C)) -> ((A & B) ∨ C)
Various test classes and tests were added. Some minor bugs were fixed and now we can search in text areas.

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 http://www.qedeq.org/0_04_04/doc/math/qedeq_formal_logic_v1_en.pdf... read more

The new release 0.04.03 introduces a new proof method: conditional proof. Based on the deduction theorem you can make an assumption and draw conclusions from it. We show the unfolding of formal logic from axioms and inference rules to propositions of propositional calculus with formal proofs within qedeq_formal_logic_v1. For background informations see under Vilnis Detlovs and Karlis Podnieks http://www.ltn.lv/~podnieks/mlog/ml.htm

When we returned from the Blocksberg at Walpurgis night a small red mouse jumped out of our clothes. It ran in the direction of our mainframe computer and vanished. Later on we found a new software version at our CI server. We tested it and found a proof checker that can verify the integrity of simple formal proofs. Even a brute force proof finder for propositional logic was there. Because we didn't find any big flaws we made a new release. So now you can try out http://www.qedeq.org/0_04_02/ yourself. But be careful - one never knows what that small mouse has done exactly!

Finally the time has come for a new release. Now 0.04.01 is out. We can write down formal proofs at least. Soon we will catch up with the prototype!

We also have a short YouTube video for a first overview of the main application: http://www.youtube.com/watch?v=XXBOvfnZNuk

We improved the plugin integration. And just to test this concept we wrote an UTF-8 converter. Now QEDEQ modules can be shown as UTF-8 texts. Further on we developed a model tester. It is fascinating to see which axioms and propositions also hold for finite models.
We also found some typing errors in our set theory script in this context. Now the "four element model" is our approved model: {}, {{}}, {{}, {{}}} and {{{}}} are the four elements of our model.
And by the way we integrated new icons and made the look and feel for the application a little bit configurable.
Because the model tester costs some time we now have a process overview window. In this window all plugin processes and their status is shown. It is also possible to interrupt running processes. For the new plugins we have config dialogs. The plugin results (usually warnings) can be deleted completely. So we can keep an overview even if we change the model.

Christmas comes fast and we start the test of our release candidate for version 0.04.00. This candidate can handle the resolution of external predicate and function constants. This means testing, testing, testing! We want a new release under the Christmas tree!

We now decided to release the new version 0.03.12. 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.
See also http://www.qedeq.org/0_03_12 for further details...

We now decided to release the new version 0.03.12. 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.
See also http://www.qedeq.org/0.03.12 for further details...

Beside testing the release candidate under various constellations we try to transfer most of the hand made mathematical annotations into the QEDEQ modules. Also the last FIXMEs wait for their resolution.

The nightly build directory at http://qedeq.org/nightly/ contains now also a webstart section where you can start the brand new development version: http://qedeq.org/nightly/webstart/qedeq.jnlp.

After a huge refactoring feast the application is reorganized and the build process is shiny new. We still use Ant but also provide maven POMs. We updated Clover (btw. thanks for the open source license) and produced this report for the new release 0.03.11. The new release contains also the eclipse project directories in the magnified src directory. Here one can also find other project reports.

0.03.10 shows multiple errors per QEDEQ module. Also the source viewer jumps to error position if the error is clicked. Only one application instance is allowed. This version requires at least java 1.4.2.

a new release is ready

Now with 0.03.08 external QEDEQ module references are resolved. So predicates can be defined outside the current module and simply be used by referencing them. Formal checking is now also extended to all required modules.

Version 0.03.07 is ready. Some small improvements were made: better error presentation, a more formal qedeq_basic_logic_v1.xml and various refactorings took place. Also during logical checking all referenced modules are loaded.

Now Hilbert II is also web startable. Some small improvements were also done. As always see changes.txt for details.

The GUI is completely new in release 0.03.05. It has a tree that shows all QEDEQ modules and visualizes their state by certain icons. Not all previous features are yet integrated and some behaviour is still not very smooth but this release is a good basis for further development.

Now we have 0.03.04 and this release has a GUI window for transforming LaTeX formulas into QEDEQ XML.
Behind the scenes a huge refactoring took place. The project has now a kernel structure. The kernel can be initialized and offers methods for loading a module from the file system or out of the internet. The kernel buffers modules and keeps a log. The kernel is not finished yet but the basic structure is there...

*Hilbert II* has another release. There are no big changes to the last one. But there are more tests, more samples, more descriptions and some small adaptions and corrections.

We have a new version. It has only minor functional changes to the last one. But it has less bugs then the last 0.03 version.
See http://www.qedeq.org/0_03_02/doc/project/changes.txt

The .zip file was not transfered complete so the downloaded files were corrupt. We apologise for this accident! The file was replaced by a new one. One inconvenience: the text files in the new zip have unix line separators.

A new release ist out. This version 0.03.01 can check if a formula is well formed.

We provide a new release of *Hilbert II*. With this release you can formalize a great deal of set theory. This was already done with the script http://www.qedeq.org/current/doc/math/qedeq_set_theory_v1_en.pdf