2014-02-05 Wir haben xercesImpl.jar neu signiert und in dem 0_04_07 Web Start Verzeichnis ersetzt. Nun funktioniert Java Web Start wieder. Falls das Starten zuvor nicht erfolgreich war, sollte der Java Web Start Cache gelöscht werden.

2014-01-18 Aufgrund von diversen Sicherheitsupdates vom Java-Hersteller Oracle kann Hilbert II nicht mehr via Web Start mit einer neuen Java-Installation gestartet werden. Das lokale Starten einer heruntergeladenen Anwendung funktioniert weiterhin.

2013-05-24 Im neuen Release 0.04.07 wurde die neu eingeführte Prozessturktur stabilisiert Außerdem wurde die Testabdeckung erhöht und einige Fehler behoben.

2013-04-24 Nun ist das Sourceforge-Projekt in die neue Struktur migriert. Dadurch ändert sich beispielsweise die svn URL.

2013-04-08 Weiter gehts mit 0.04.06. Sichtbarste Änderung ist die Verwendung von Icons zur Statusanzeige der QEDEQ-Module. Und zwar grau für noch nicht bearbeitete Module, lila für geladene Module, türkis für das Laden aller vorausgesetzten Module, orangerot für alle syntaktisch korrekten Module und gelb für alle vollständig bewiesenen Module. Fehler und Warnungen werden durch entsprechende "Verzierungen" der Icons visualisiert. Gerade im Übergangsprozess befindliche Module werden durch animierte Icons dargestellt.
Neben einigen Tool-Updates (clover, findbugs) war das Hauptthema die Überarbeitung der Prozesssynchronisierung und -steuerung. Dieser Vorgang ist noch nicht abgeschlossen, aber es sind inzwischen fast alle Modulstatusänderungen durch (interne) Plugins bewirkt. Auch die Unterbrechbarkeit wurde erweitert und die Anzeige der Prozessdetails angereichert.

2013-02-10 Ein neues Release ist veröffentlicht. 0.04.05 hat einige formale Beweise mehr und eine sehr viel grössere Testabdeckung. Die erhöhte Testanzahl offenbarte einige kleine Bugs, welche nun gefixt sind. Eine kleine funktionale Verbesserung gibt es auch: dieses Release ermöglicht die Suche in Textfeldern.

2012-12-27 So, wir sind wieder zurück! Über ein Jahr lang haben uns andere Projekte gefangen genommen. Aber auch wenn sie noch nicht abgeschlossen sind, ist es jetzt dringend an der Zeit wieder bei Hilbert II Fahrt aufzunehmen.

2011-07-30 Ein neues Release 0.04.04 ist fertig. Wir haben nun einen Parser, der aussagenlogische Beweise, die im ASCII format vorliegen, einlesen und in ein QEDEQ-XML-NODE-Element umwandeln kann. Das Programm ist nicht sehr komfortabel, aber wir konnten damit die Beweisintegration spürbar beschleunigen. Das Programm kann über den GUI-Menueintrag Tools / Proof Text to QEDEQ aufgerufen werden.
Eine Ableitungsregel muss nun auch eine Version besitzen und Name zusammen mit Version muss eindeutig sein (was auch überprüft wird). Wir können jetzt Übersichtsseiten (LaTeX und UTF-8-Plugin) erstellen mithilfe des brief-Parameters.
Schließlich haben wir einige Propositionen mit formalen Beweisen mehr in qedeq_formal_logic_v1. Auch die lästigen Beweise zur Assoziativität sind jetzt vorhanden.

2011-06-13 Das neue Release 0.04.03 führt eine neue Beweismethode ein: Conditional Proof. Basierend auf dem Deduktionstheorem kann eine Annahme getroffen werden und mit dieser Folgerungen gezogen werden. In qedeq_formal_logic_v1 zeigen wir die Entfaltung der formalen Logik aus den Axiomen und Ableitungsregeln zu den Propositionen der Aussagenlogik mit formalen Beweisen. Für Hintergrundinformationen bitte bei Vilnis Detlovs and Karlis Podnieks Introduction to Mathematical Logic oder bei wikipedia.org nachschauen.

2011-06-11 Mit unserem anstehenden neuen Release zeigen wir das Einfügen eines formalen Beweises in Hilbert II. Einfach auf YouTube angucken. Achtung, die Tonqualität ist schlecht und der Ton ist nicht synchron.

2011-05-01 Als wir vom Blocksberg in der Walpurgisnacht zurückkehrten, sprang ein rotes Mäuschen aus unseren Kleidern. Es rannte in Richtung unseres Hauptcomputers und war verschwunden. Später fanden wir eine neue Softwareversion auf unserem CI-Server. Wir testeten sie und fanden einen Theorem-Überprüfer der einfache formale Beweise auf Korrektheit überprüfen kann. Sogar einen Brute-Force-Beweisfinder für die Aussagenlogik haben wir entdeckt. Da wir keine grossen Mängel gefunden haben, haben wir ein neues Release erzeugt. So kann nun jeder selbst 0.04.02 ausprobieren. Aber Vorsicht - wir haben immer noch keine Ahnung was dieses Mäuschen genau gemacht hat!

2011-03-05 Endlich ist die Zeit für ein neues Release gekommen. Jetzt ist 0.04.01 fertig. Wir können nun formale Beweise zumindest aufschreiben. Bestimmt holen wir bald den Prototyp ein!
Es gibt nun auch ein kleines YouTube-Video, das einen ersten Überblick der Hauptanwendung zeigt.

2011-02-04 Nun können wir ganz simple formale Beweise parsen. Die XSD wurde entsprechend erweitert und die ersten Text-Viewer funktionieren. Die LaTeX-Erzeugung fehlt noch, aber wir haben einen Durchstich. Nun muss der Code noch etwas aufgeräumt werden und wir brauchen noch Beispiele und Tests. Möglicherweise haben wir in ein paar Wochen ein neues Release.

2010-12-28 Das neue Release 0.04.00 ist fertig. Fröhliche Weihnachten und ein gutes neues Jahr!

2010-12-20 Weihnachten naht mit Riesenschritten und wir beginnen mit dem Test unseres Release-Kandidaten für die Version 0.04.00. Dieser beherrscht auch die Auflösung externer Prädikats- und Funktionskonstanten bei der Modellberechnung. Nun heißt es testen, testen, testen. Wir wollen ein neues Release unterm Weihnachtsbaum!

2010-12-11 Die Abweichungen der verschiedenen Modellergebnisse konnten aufgeklärt werden. In diesem Zusammenhang wurden auch einige Tipp-Fehler im Mengenlehre-Skript gefunden. Das "Vier-Elemente-Modell" hat sich bewährt: {}, {{}}, {{}, {{}}} und {{{}}} lauten die vier Elemente unseres Modells.
Nebenbei haben wir noch neue Icons integriert und die ersten Konfigurationsmöglichkeiten für das Aussehen der Anwendung eingebaut.

2010-11-06 Da der Modelltester einiges an Zeit in Anspruch nimmt, gibt es nun auch eine Prozessübersicht. In dieser werden alle Plugin-Prozesse mit ihrem aktuellen Status festgehalten. Es ist auch möglich, laufende Prozesse zu unterbrechen. Für die neuen Plugins gibt es nun auch Konfigurationsdialoge. Die Ergebnisse von Plugin-Ausführungen (in der Regel Warnungen) können nun auch insgesamt gelöscht werden. So kann man den Überblick auch nach einer Änderung der Modellauswahl behalten.

2010-10-23 Aktuell verbessern wir die Plugin-Integration. Und um das ganze gleich zu testen, haben wir einen UTF-8-Konverter geschrieben. QEDEQ-Module können nun auch als UTF-8-Texte angezeigt werden. Weiterhin arbeiten wir an einem Modelltester. Es ist spannend zu sehen, welche Axiome und Propositionen auch für endliche Modelle gelten.

2010-09-19 Wir haben uns nun entschlossen die neue Version 0.03.12 freizugeben. Es wurden zwar nicht alle Tests durchgeführt, dennoch sollte es sich um ein recht stabiles Release handeln. Ab sofort gibt es zwei Sorten von Releases: "normal" und "development" In "development" sind auch die Software-Quellen und Metriken enthalten.

2010-08-16 Im Nightly-Build-Verzeichnis kann nun auch der brandaktuelle Stand der Anwendung gestartet werden.

2010-08-14 Der neue About-Dialog ist fertig. Wir wissen nun auch, dass die httpclient-Einbindung unter Java 1.4.2 mit Java Webstart via Proxy fehlschlägt.

2010-07-29 Die Einarbeitung der mathematischen "Amrum Notizen" in QEDEQ-Module hat jetzt begonnen.

2010-03-19 Architektonische Anpassungen: eine neue Plugin-Struktur wurde geschaffen. LaTeX-Erzeugung ist nun eine Plugin-Ausführung. Außerdem gibt es nun auch Warnungen. Ein Plugin kann solche produzieren.

2010-03-05 Hudson läft nun stabil unter meyling.de:8080/hudson. Und user neuer PreferencesDialog ist fertig.

2010-02-11 Wir haben nun unseren eigenen virtuellen Server. Nun müssen wir nur unser CI-System wieder aufsetzen...

2009-09-23 Nun können wir auch JavaHelp 2.0.5.

2009-07-08 Das Bug Tracking wird nun durch QEDEQ Mantis vorgenommen.

2009-07-02 Http Verbindungen werden nun mit Apache's httpclient gemanaget.

2009-06-10 Mehr und mehr Test Code wird geschrieben. Gleichzeitig werden ein paar kleine Fehler in der Anwendung eliminiert...

2009-06-02 Nun haben wir auch das Problem "Eclipse hangs on exit in futex" gelöst: Checkbox "Enable Assistive Technologies" ausschalten.

2009-05-30 Unser Build-Prozess wird nun durch Hudson durchgeführt. Für Entwickler gibt es einen Zugriff über das Internet. Die Software wird nun kontinuierlich gebaut und getestet.

2009-05-22 Nun wurde die Entwicklungsumgebung auch unter Ubuntu zum Fliegen gebracht. Nach einigen Schwierigkeiten mit Subversion konnten letztlich doch erfolgreich Commits durfgeführt werden.

2009-05-02 Wir spielen ein wenig mit Hudson als Continuos Integration Tool herum. Es läuft sofort nach dem Auspacken und sieht gut aus.

2009-04-19 Installation von tomcat als service und das Zugänglich machen von aussen via dyndns.org.

2009-03-30 Wechsel des Computers und Einsatz eines neuen Betriebssystems (ubuntu). Das bedeutet viele Installationen in sehr langen Nächten.

2008-08-04 Nach einer riesigen Refactoring-Orgie ist die Anwendung nun reorganisiert und mit einem strahlend neuen Build-Prozess versehen. Wir benutzen weiterhin Ant, stellen aber auch Maven POMs zur Verfügung. Wir setzen nun eine neue Clover-Version ein (übrigens vielen Dank für die Open-Source-Lizenz) und haben damit diesen Report für das neue Release 0.03.11 erzeugt. Das neue Release enthält auch die Eclipse-Projektverzeichnisse in dem inzwischen enormen src-Verzeichnis. Hier befinden sich auch weitere Projektreports.

2008-05-17 0.03.10 zeigt alle Fehler eines QEDEQ-Moduls. Weiterhin springt der Source-Viewer an die Fehlerposition, wenn der Fehler in der Fehlerliste angeklickt wird. Es kann nur noch eine Instanz der Anwendung gestartet werden. Diese Version erfordert zumindest Java 1.4.2.

2008-03-30 Das neue Release 0.03.09 kann mit externen QEDEQ-Modulreferenzen umgehen. Selbst wenn ein Modul entfernt wird ändern alle abhängigen Module ihren Status entsprechend. Innerhalb von LaTeX-Teilen kann mit dem neuen Kommando \qref auf lokale oder importierte Knoten von anderen QEDEQ-Modulen verwiesen werden.

2008-01-26 Mit 0.03.08 haben wir fast schon gaffsie erfüllt. Nur aufgrund der vielen TODOs und fehlender Tests nennen wir es noch mongaga.

2007-12-22 Version 0.03.07 ist fertig. Einige kleine Verbesserungen wurden durchgeführt: eine bessere Fehlerdarstellung, ein etwas mehr formales qedeq_basic_logic_v1.xml und diverse Refactorings haben statgefunden. Desweiteren werden bei Prüfung auf logische Korrektheit auch alle abhängigen Module geladen.

2007-10-14 Nun kann die GUI auch mit Java Web Start gestartet werden. Dazu nur auf START klicken, um die aktuelle Version zu starten.

2007-09-02 Die GUI wurde in Release 0.03.05 komplett neu gemacht. Sie besitzt nun einen Baum, der alle QEDEQ-Module anzeigt und ihren jeweiligen Status mit Symbolen darstellt. Nicht alle vorherigen Funktionen sind schon integriert und manches Verhalten ist noch nicht sehr ansehnlich, aber dieses Release ist eine gute Basis für die weitere Entwicklung.

2007-05-10 Nun haben wir ein Kernel-Release 0.03.04. Der LaTeX-Formel-Parser kann nun aus der GUI gestartet werden.

2007-03-11 Wir machen weitere kleine Schritte in Richtung unserer grossen Ziele. So haben wir nun Release 0.03.03.

2007-02-25 Es ist getan, die Version 0.03.02 ist fertig. Bei der Erstellung haben wir einen schweren Fehler in der letzten Windows-Version gefunden: das herunterladbare ZIP-File war defekt. Wir entschuldigen uns für diesen Fehler!

2007-01-15 Die mongaga Version 0.03.01 steht bereit.

2007-01-07 Eine nette Abwandlung des Visitor Patterns ist entwickelt und implementiert.

2006-12-21 Der Formelüberprüfer ("ist diese Formel wohlgeformt") funktioniert.

2006-11-06 Die Basisfunktionalität des Formelüberprüfers läuft. Und tatsächlich haben wir in unserem Mengenlehreskript einen Fehler gefunden!

2006-10-22 Version 0.02.01 fertig. Hierbei handelt es sich um ein moster-Release.

2006-09-14 Erneute Überarbeitung der Projektseiten abgeschlossen.

2006-08-01 Inselluft soll frische Gedanken bringen.

2006-07-06 Erfolgreiche Umwandlung eines LaTeX-Textes in ein QEDEQ-Modul.

2006-04-03 Zur Archivierung und Versionsverwaltung von Programm-Code wird nun Subversion benutzt.

2005-12-29 Entwicklerrelease Version 0.01.09 ist fertig.

2005-10-18 Ein weiteres Entwicklerrelease, Version: 0.01.08. Enthält ein Skript über den Anfang der axiomatioschen Mengenlehre.

2005-09-05 Zweites "unstable" Entwicklerrelease des Hauptprojekts. Code Name: brigand, Version: 0.01.07.

2005-03-09 Erstes "unstable" Entwicklerrelease des Hauptprojekts. Code Name: brigand, Version: 0.01.06.

2005-01-22 Das Englische Projekthandbuch wird nun aus einem XML-Qedeq-Modul generiert. Hier ist das XML-Dokument und hier das Handbuch.

2004-12-24 Das Hauptprojekt nutzt nun XML als Datenformat. Siehe die XML-Schema-Spezifikation und ihre Dokumentation.

2004-10-24 Setup-Programm zur Installation des Prototypen unter MS-Windows ist da. Siehe unter download.

2004-09-26 Release von Version 0.00.53.

2004-08-15 Das Diskussionsforum wurde neu organisiert und liegt nun in englischer Sprache vor.

2004-06-19 Code Freeze für die Version 0.00.53. Nun wird nur noch getestet.

2004-04-29 Die Hauptziele der Entwicklung für die nächste Version sind errreicht. Lokale Qedeq-Module können geladen werden, Trace- und Logging-Funktionen und History-Listen sind realisiert. Es findet ein Refactoring des alten Programm-Codes statt.

2004-03-21 Hier kann der aktuell in Entwicklung befindliche Prototyp direkt per Java-Web-Start aufgerufen werden: pmii 0.00.53. Diese Version besitzt eine GUI und kann bequem mit der Maus bedient werden.

2004-02-22 Ein eigenes Diskussionsforum für Projekt-Interessierte wurde eingerichtet.

2004-01-08 Die Link-Seite wurde überarbeitet und um wichtige Links zu verwandten Projekten ergänzt.

2003-12-19 Für die Implikation und die Äquivalenz werden nun zukünftig statt '=>' und '<=>' die Symbole '->' und '<->' verwendet. Wir habe uns damit einer international gebräuchlichen Symbolik angeschlossen.

2003-11-05 Das Projekt wurde in Hilbert II umbenannt (ursprünglich "Principia Mathematica II").

2003-10-03

F. Fritsche machte auf ein alternatives Axiomensystem für die Aussagenlogik aufmerksam, das Axiomensystem von Gotlind und Rasiowa:

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

Die Axiome HA 3 (P v Q) -> (Q v P) and HA 4 (P -> Q) -> [(R v P) -> (R v Q)] des Axiomensystems von Hilbert & Ackermann können daraus abgeleitet werden.

2003-08-16 Die logischen Texte dieses Projekts sind nun auch hier zu sehen: PlanetMath.

2003-07-08 Dieses Projekt ist nun auch in freshmeat.net zu finden.

2003-06-29 Die Version 0.00.52 ist fertig.

2003-05-11 Ein Syntax-Parser für das QEDEQ-Format erzeugt aus der Beschreibung des QEDEQ-Formats eine XML-DTD. Siehe QEDEQ DTD.

2003-04-23 Das Grobkonzept wird immer umfangreicher.

2003-03-09 Die Fertigstellung des Grobkonzepts steht immer noch an erster Stelle: Projektbeschreibung.

2003-02-06 Das Grobkonzept ist weiter in Arbeit...

2003-01-27 Deutsche Webseiten online, mit dabei: eine erste Version eines Grobkonzepts für dieses Projekt: Projektbeschreibung.

2003-01-02 Ein Bild von dem experimentellen QEDEQ viewer.

2002-11-17 Start dieser Webseiten.

2000-08-04 Start dieses Projekts.

update 2016-03-27 23:36:55+0200