www.qedeq.org

 Hilbert II

English   Deutsch
Hilbert II at SourceForge
introduction
news
mathematics
QEDEQ
planning
download
glossary
development
prototype
installation
manual
propositional calculus
predicate calculus
QEDEQ
module
formula
QEDEQ text
problems
links
contact
site map
Prototype / PMII QEDEQ Module / BNF text description

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).

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