Hilbert II

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

You should try to start the prototype with a click onto pmii. If you are lucky you get a security question at which you have to accept (against the suggestion) the signature of Michael Meyling. If starting the application fails you should take a look at Java Web Start. The prototype can also be installed as described in the following sections.

Preconditions for Installation

Precondition for a working prototype is a Java Runtime Environment, at least version 1.4. From Download Java 2 Platform you could get the Java Runtime Environment J2SE v 1.4.2 JRE.


The prototype including the source code can be received from: download. It consists of a ZIP archive or a tar file. Unpack the file into a directory pmii for example \Program Files or ~/pmii.

Directory Structure

The directory pmii has the following structure.

readme.txt release information
run.bat batch file to start the application
run.sh script file to start the application
com.meyling.principia.properties central configuration file
bin/ more batch files for non GUI operation
buffer/ local QEDEQ module buffer
doc/ documentation
   modules/ provided QEDEQ module files, only for documentation
generated/ generated HTML, LaTeX or QEDEQ files
javadoc/ Java program documentation
lib/ program libraries
local/ for newly generated QEDEQ files
log/ event journal and trace
src/ source code


If the bin path of the Java Runtime Environment has no entry in the executable path or a proxy is used for the internet access the files run.bat or run.sh must be edited. The necessary adaptations are described in comments of those files.

That was the standard configuration of the application. If the graphical user interface is not used, the next section should be read.

Special Configuration

The file com.meyling.principia.properties is a Java properties file and normally mustn't be edited manually. The values in this file are changeable in the application or only internally used. At each shutdown of the application the file is rewritten.

It contains a sequence of properties (key and element pairs) and must be read and written using the ISO 8859-1 character encoding. The character "#" starts a line comment. Each other non empty line is of the format <key>=<value>. The ASCII characters "\", tab, newline, and carriage return are written as "\\", "\t", "\n", and "\r", respectively. The characters "#", "!" and "=" are written with a preceding slash as "\#", "\!" and "\=". Leading space characters (but not embedded or trailing space characters) for values are also written as "\ ".Characters less than \u0020 and characters greater than \u007E are written as \uxxxx for the appropriate hexadecimal value xxxx. For further information about this format see Properties.store.

Key Possible Values Default Description
autoStartHtmlBrowser true, false true Start web browser automatically after HTML generation for a single QEDEQ module?
directResponse true, false true Open pop up message window for every action response? The messages can always be seen at the status line and in the log window.
oldHtml true, false true Start web browser (see above) with HTML document that uses the System-Font? If the shown web pages look not satisfactorily please try false. For more about HTML display problems see also under propositional calculus.
sessionAutoReload true, false true During restart of the application should be all QEDEQ modules loaded again which were successful loaded just before the last shutdown of the application?
startDirectory Application Directory   This entry is only written and not read by the application. If the application was not started by Java Web Start the config file is searched in the current directory. Otherwise the Java system variable jnlpx.deployment.user.home is used (and if there is no entry user.home) and the contained path extended with /pmii.
configFileLocation Config File Location   This entry is only written and not read by the application. In the (ascertained as described above) application path the config file com.meyling.principia.properties is searched. If the config file doesn't exist the default values are taken. At the end of the application a new config file is written.
bufferLocation Directory for QEDEQ File Buffer buffer/ From the internet loaded QEDEQ module files are saved in this directory.
generationLocation Generation Directory generated/ Generated documents are written into this directory.
localModulesDirectory Directory for new QEDEQ Module Files local/ If a new QEDEQ module is created within the GUI the file is saved in this directory.
checkedModule.n URL of a QEDEQ Module A successfully loaded QEDEQ module at last application shutdown.
moduleHistory.n URL of a QEDEQ Module History for directly loaded QEDEQ modules. The drop down list shows the last loaded URLs.

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