Hilbert II

English   Deutsch
Hilbert II at SourceForge
propositional calculus
predicate calculus
site map
Prototype / Manual

Fast Lane

After starting the prototype a window with an empty left side and a right side with tabs appears. At the left the currently used QEDEQ modules are shown. At the right side information about the selected (left side) QEDEQ module are shown. For loading a module choose the menu entries "File" and "Check and Load Module". After selecting the module http://www.qedeq.org/0_00_53/proptheo1_1.00.00_1.00.00.qedeq the prototype loads this QEDEQ module from the internet and saves it locally. The module is analyzed and checked. By doing this the prototype detects that another QEDEQ module is referenced. This module propaxiom is also loaded, locally saved and checked. Both verifications were (hopefully) successful and at the left side appear two green circles beside the two module names. Now a message box pops up telling about the successful loading of the original asked for module.

After clicking at proptheo1 there will be some information displayed at the right side. After selecting the tab "Qedeq" the QEDEQ module is displayed in simple text form. By choosing the menu points "Generate" and "HTML" a HTML document (well, in fact two documents, see below) is generated out of the selected module. After affirming the message the default web browser is automatically started and shows the newly generated document (if everything goes well).


For configuration of different parameters open the preferences window by selecting "Settings / Preferences" in the menu. There the annoying pop up windows can be cut off by deselecting the check box "Direct message response for actions".

The autostart of the default web browser can be de- or activated. If activated the property "Use System font HTML at web browser start" is used to decide which HTML document to show. Either the HTML document which uses the System font to display special mathematical characters (file ends with "o.html") or the "regular" HTML document which uses character entities (e.g. ∧) is opened. The last document can be viewed better with web browsers like Mozilla and Netscape. To learn more about the HTML display problems look under propositional calculus.

The setting "Auto loading of in last session successfully checked modules" is evaluated at the startup phase. If checked all at the time of the last shutdown successfully loaded modules are loaded again.

Furthermore different paths can be edited. See also under configuration.

File Names and Versions of QEDEQ Modules

The file name of a QEDEQ module is concatenated by the name of the module (alphanumeric) an underline the version number of that module (in the format n.nn.nn) another underline and the rule version number (also in the format n.nn.nn). The module version number makes one module version distinguishable from another. If the module version number equals 1.00.00 it is omitted from the display at the left side.

The rule version determines the possible rules that can be used by the QEDEQ module. Only a rule with a version number smaller or equal is allowed. Nevertheless each rule must be declared, before it can be used. The rule version number is not displayed at the left side. Modules with a rule version equal to 1.02.00 however are marked with the character '.

The basic rules have the version number 1.00.00. An overview about all rules and their belonging version number can be found under rules.

Loading and Closing of QEDEQ Modules

Loading of QEDEQ modules can be done with the "File" menu. Beside the above mentioned "Check and Load Module" which enables the input of an URL, it is also possible to load a local QEDEQ file by using "Check and Load Local File Module".

By starting "Load All Modules From Project Home Page" all QEDEQ modules known to the prototype are downloaded from the website, loaded and checked (see propositional calculus and predicate calculus).

All (non local) QEDEQ modules are buffered in the file system, so every new access can be done by loading the module from the local file system. A complete removal of this buffer is possible by calling "Special / Clear Local File Buffer". Then a new try to load a module doesn't find any local buffered file and loads the requested module from the internet and makes a local copy.

To close one and all modules respectively so that they vanish from the display (and memory) the menu entries "Remove Module" and "Remove All Modules" must be chosen. With a module all dependent modules are also removed. By removing the QEDEQ module propaxiom for example, (nearly) all other modules vanish also.

Creation and Edit of new QEDEQ Modules

With the menu entry "File / Create New Local Module" a new QEDEQ module can be created. It is saved as a file named new_1.00.n_1.02.00. The number n is counted up (and formatted to at least two digits).

After that the new module can be edited and saved.


The tab "Log" shows the event history of the current session.

update 2014-01-20 09:20:48+0100