Hilbert II

Here is the description of a QEDEQ text module in BNF notation. For an example text file see: Axiomatic Set Theory (at least it is close to this definition).

<qedeq module> ::= <header>
                   <paragraphs>

<header>       ::= <spec>               % specifies this qedeq module
                   <title>
                   <abstract>           % describes contents
                   Module admin: <email>% email to this address if you want to inform the
                                        %  module administrator (e.g. about referencing
                                        %  this module)
                   <authors>
                   [<imports>]          % import these qedeq modules
                   [<usedby>]           % these qedeq modules use this module

<spec>         ::= Qedeq specification:
                   Name:      <name>    % name of this module, must be identical
                                        %  with first part of file name
                   Version:   <version> % must be identical with second part
                                        %  of file name
                   Rules:     <version> % this version of pmii is needed for
                                        %  checking the correctness of this file
                   Locations: {<location>} % web URL of this qedeq module

<authors>      ::= Author(s): {<author> [(<email>)]}



<imports>      ::=  Needs the following qedeq modules:
                    {import}

<import>       ::=  <spec>               % now relative URLs are ok to describe a location
                    <label>              % alias, label prefix to use for that module

<paragraphs>   ::= {<paragraph>}

<paragraph>    ::= "(" <label> ")"       % for referencing
                   [<latex>]             % preceding text

                   (<abbreviation> | <axiom> | <declaration> | <definition> | <proposition>)

                   [<latex>]             % following text

<abbreviation> ::= <formula> := <formula> % first formula has pattern variables as arguments
                                          % in the second formula the same pattern variables
                                          % must occur

<declaration>  ::= <name>                % name of rule to declare
                   <description>         % short description of rule
                   {<link>}              % reference(s) to needed axioms or propositions

<axiom>        ::= <formula>             % this is an axiom

<proposition>  ::= <sentence>
                   <proof>

<sentence>     ::= <formula>             % this formula could be proved, no pattern
                                         %  variable allowed

<proof>        ::= {<line>}              % last proof line formula must be equal to sentence
                                         %  formula

<line>         ::= <formula>             % formula that could be deduced by previous proof lines
                                         % or axioms, abbreviations, definitions or declared rules
                   {<lineref>}
                   {<link>}


Text could include links to labels
In proofs external references could be made by "alias.label",
internal references are made by <label>. (The alias must be
defined in the <import> list.)

Imports could have relative paths (relative to current module).