2014-02-05 We recalculated the signature of xercesImpl.jar and replaced it in the 0_04_07 Web Start directory. Now Java Web Start is working again. You might have to clean the Java Web Start cache if you unsuccessfully tried to start the application before.

2014-01-18 Due to various Java security updates from Oracle Hilbert II can not be started via Web Start with a new java installations. Downloading the application and starting it directly is still working.

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

2013-04-24 The sourceforge project migrated into a new structure. Some things changed there. For example, we have a new svn URL.

2013-04-08 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 and 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.

2013-02-10 A new release is published. 0.04.05 has some more formal proofs and much more test coverage. The increased number of tests revealed some minor bugs which are fixed now. And a little functional improvement: this release enables you to search in text areas.

2012-12-27 We are back again! We were stuck in other projects for more than a year. But even if they are not finished it's high time to pick up steam in Hilbert II.

2011-07-30 A new release 0.04.04 is ready. 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.

2011-06-13 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 Introduction to Mathematical Logic and wikipedia.org.

2011-06-11 With our upcoming new release we show how to put a formal proof into Hilbert II. Just watch the video at YouTube. Warning: the sound quality is poor and the sound is not synchronized.

2011-05-01 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 0.04.02 yourself. But be careful - one never knows what that small mouse has done exactly!

2011-03-05 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.

2011-02-04 Now we can parse primitive formal proofs. The XSD is extended and the first text views are working. LaTeX generation is still missing but we have a spike solution. Now we must smooth the code base and work on examples and tests. In a few weeks we might have a new release.

2010-12-28 The new release 0.04.00 is out. Merry Christmas and a happy new year!

2010-12-20 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!

2010-12-11 The discrepancies between the different model results were solved. 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.

2010-11-06 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 now. The plugin results (usually warnings) can be deleted completely. So we can keep an overview even if we change the model.

2010-10-23 Currently we improve 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 develop a model tester. It is fascinating to see which axioms and propositions also hold for finite models.

2010-09-19 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.

2010-08-16 In the Nightly Build directory you can also start the brand new development version now.

2010-08-14 The new about dialog is ready. We now also know that the httpclient integration fails under Java 1.4.2 when runing under Java Webstart via proxy.

2010-07-29 Integration of the mathematical "Amrum Notes" into QEDEQ module files started now.

2010-03-19 Architectural change: introduced new plugin structure. LaTeX generation is now a plugin execution. We also integrate warnings into our system. A plugin can produce warnings.

2010-03-05 Hudson runs stable under meyling.de:8080/hudson. And our new PreferencesDialog is ready.

2010-02-11 We have our own virtual server. Now we have to set up our CI system again....

2009-09-23 Now using JavaHelp 2.0.5.

2009-07-08 Bug tracking is now organized via QEDEQ Mantis.

2009-07-02 Http connections are now managed with apache's httpclient.

2009-06-10 More and more test code is written. At the same time some minor application errors are eliminated ...

2009-06-02 Now we solved the "Eclipse hangs on exit in futex" problem: Checkbox "Enable Assistive Technologies" must be switched off.

2009-05-30 Our build process is now adminstrated by Hudson. For developers it is accessible through internet. The software is now build and tested continuously.

2009-05-22 Now we changed our development environment changed to ubuntu. After suffering some subversion difficulties we finally did some successful commits.

2009-05-02 We play with Hudson as an continuos integration tool. It works out of the box and looks good.

2009-04-19 Installing tomcat as service and making it accessable from outside via dyndns.org.

2009-03-30 Changing main computer and using new operating system (ubuntu). This means various installation sessions in very long nights.

2008-08-04 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.

2008-05-17 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.

2008-03-30 The new release 0.03.09 can deal with external QEDEQ module references. Even if a module is removed all dependent modules change their state accordingly. Within LaTeX parts the new command \qref can reference to local or imported nodes of other QEDEQ modules.

2008-01-26 With 0.03.08 we nearly reached gaffsie. Only because of much code TODOs and missing tests we still call it mongaga.

2007-12-22 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.

2007-10-14 Now the GUI is also startable via Java Web Start. Just click on START to start the current release.

2007-09-02 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.

2007-05-10 Now we have a kernel based release 0.03.04. The LaTeX formula parser is now GUI startable.

2007-03-11 We take small steps toward our big goals. So we have release 0.03.03.

2007-02-25 It is done, release 0.03.02 is out. We also found a major error in the last windows release: the downloadable zip file was corrupt. We apologise for this error!

2007-01-15 The mongaga version 0.03.01 is released.

2007-01-07 A nice adaption of the visitor pattern is developed and implemented.

2006-12-21 The formula checker ("is this formula well formed") is working.

2006-11-06 The basic features of the formula checker are working. And in fact we found an error within our set theory script!

2006-10-22 Version 0.02.01 released. This is a moster one.

2006-09-14 Further rework of home page finished.

2006-08-01 Trying to escape insular thinking on an island.

2006-07-06 Successful conversion of LaTeX text into QEDEQ module.

2006-04-03 Project sources are now in subversion repository.

2005-12-29 Development release version 0.01.09 is ready.

2005-10-18 Another development release, version: 0.01.08. Includes a script with the beginning of axiomatic set theory.

2005-09-05 Second "unstable" development release of the main project. Code Name: brigand, Version: 0.01.07.

2005-03-09 First "unstable" development release of the main project. Code Name: brigand, Version: 0.01.06.

2005-01-22 English project handbook generated out of QEDEQ module XML data. Look at the XML document and at the handbook.

2004-12-24 Main project uses XML as main data format. See the XML schema specification and it's documentation.

2004-10-24 Setup program for installing the prototype under MS windows available. See under download.

2004-09-26 Release of version 0.00.53.

2004-08-15 The discussion board was reorganized and it's language is now English.

2004-06-19 Code Freeze for version 0.00.53. The testing phase begins.

2004-04-29 Main development goals of next version are achieved. Local QEDEQ modules could be loaded, trace and logging functions and history features are implemented. A refactoring of the source code takes place.

2004-03-21 With Java Web Start the currently developed prototype could be started here: pmii 0.00.53. This version includes a GUI for starting tasks with a simple click.

2004-02-22 A new discussion board for people interested in Hilbert II has been set up.

2004-01-08 The page with links has been reworked and extended with important links to related projects.

2003-12-19 For logical implication and equivalence instead of '=>' and '<=>' now the more common symbols '->' and '<->' will be used.

2003-11-05 The project has been renamed to Hilbert II (formerly "Principia Mathematica II").

2003-10-03

F. Fritsche pointed out an alternative axiom system for propositional calculus, the axiom system by Gotlind and Rasiowa:

Ax 1		(P v P) -> P
Ax 2		P -> (P v Q)
Ax 3		(P -> Q) -> [(R v P) -> (Q v R)]

The axioms HA 3 (P v Q) -> (Q v P) and HA 4 (P -> Q) -> [(R v P) -> (R v Q)] of Hilbert & Ackermann's original system can be derived from this system.

2003-08-16 Logical documents of this project are now also available at PlanetMath.

2003-07-08 This project is now also visible in freshmeat.net.

2003-06-24 Version 0.00.52 is ready.

2003-05-11 A syntax parser for the QEDEQ format generates from the formal description of an QEDEQ module an XML-DTD. See QEDEQ DTD (comments in German).

2003-04-23 Fattening up the German project handbook.

2003-03-16 German web pages improved, the German project handbook is growing.

2003-01-27 German web pages online: Deutsch.

2003-01-02 A picture of experimental QEDEQ viewer.

2002-11-17 First launch of this web pages.

2000-08-04 Start of this project.

update 2016-03-27 23:37:02+0200