<!-- $Revision: 0.00.46 $ -->

""= Text               atomic argument, could be any quoted text
n = Counter            atomic argument, could be any positive integer
                         (1, 2, 3, ...)
multiple arguments are separated by ","                         
? = optional occurrence
* = none till many occurrences
+ = one till many occurrences


MODULE(
  HEADER(
    SPEC(
      NAME("")         name of this module, must be identical with    
                        first part of file name
      VERSION("")      module version, must be identical with last part
                        of file name
      VERSION("")      needs this rule version
      LOCATIONS(
        LOCATION("")   + local or web or relative URL of this module 
                        file
      )
    )
    HEADLINE("")       headline of module
    DESCRIPTION("")    describes contents
    EMAIL("")          email to this address if you want to inform the
                        module administrator (e.g. about referencing
                        this module)
    AUTHORS(
      AUTHOR(          + author of this module
        ""             name of author
        EMAIL("")
      )
    )
  )
  IMPORTS(             ?
    IMPORT(            * these external modules are needed
      SPEC(
        NAME("")       name of needed module
        VERSION("")    version of needed module
        VERSION("")    rule version needed module needs
        LOCATIONS(     
          LOCATION("") + local or web or relative URL of module
        )
      )
      LABEL("")        ? label to use for that module
                        if missing, all labels of that module are
                        added directly
    )
  )
  USEDBY(              ?
    SPEC(              +
      NAME("")         name of module, must be identical with    
                        first part of file name
      VERSION("")      module version, must be identical with last part
                        of file name
      VERSION("")      needs this rule version
      LOCATIONS(
        LOCATION("")   + local or web or relative URL of module file
      )
    )
  )
  PARAGRAPHS(
    PARAGRAPH(         * the meat
      LABEL("")        for referencing
      ""               ? preceding text
      {ABBREVIATION |
       AXIOM |
       PROPOSITION
      }
      ""               ? following text        
  )
) 

ABBREVIATION (
  FORMULA              operator with pattern variables as arguments
  FORMULA              same pattern variables must occur
)

AXIOM (
  FORMULA              this is an axiom
)

PROPOSITION(
  SENTENCE(
    FORMULA            this formula could be proved, no pattern
                        variable allowed
  )
  PROOF (
    LINE(              + last proof line formula must be equal
                        to sentence formula
      FORMULA          formula (without pattern variables) that
                       could be deduced by previous proof lines
                       (or axioms or abbreviations) by using the
                       following rule:
      {ADDAXIOM |              adding an axiom
       ADDSENTENCE |           adding an already proved proposition
       MODUSPONENS |           applying modus ponens
       REPLACEPROP |           replacing a proposition variable
       USEABBREVIATION |       using an abbreviation
       REVERSEABBREVIATION |   reversing an abbreviation
       RENAMEFREEVARIABLE |    renaming a free subject variable
       RENAMEBOUNDVARIABLE |   renaming a bound subject variable
       REPLACEPREDICATE |      replacing a predicate by a formula
       GENERALIZATION |        applying generalization
       PARTICULARIZATION       applying particularization
      }
    )
  )
)


FORMULA(
  PROP(n) |                    proposition variable
  NOT(FORMULA) |               negation
  AND(FORMULA, FORMULA) |      conjunction (disjunct bound and free
                                subject variables)
  OR(FORMULA, FORMULA) |       disjunction (ditto)
  IMPL(FORMULA, FORMULA) |     implication (ditto)
  EQUI(FORMULA, FORMULA) |     equivalence (ditto)
  PREDVAR |                    predicate variable
  FORALL(VAR(n), FORMULA) |    universal quantifier (subject variable
                                must be free in formula, and is now
                                a bound one)
  EXISTS(VAR(n), FORMULA) |    existential quantifier (ditto)
  PATTERN(n)                   pattern variable
)

PREDVAR(
  n                    number of predicate, specifies together 
                        with argument number of following L a
                        predicate variable
  L(                   list of subject variables
    VAR(n)             +
  )
)

ADDAXIOM (             add axiom
  LINK("")             reference to axiom
)

ADDSENTENCE (          add sentence
  LINK("")             reference to already proved proposition
)

MODUSPONENS (          modus ponens
  n                    proof line number that references A
  n                    proof line number that references A => B
)

REPLACEPROP (
  n                    proof line number
  PROP(n)              search for this proposition variable
  PROP(n)              replacement proposition variable
)

USEABBREVIATION (
  n                    proof line number
  LINK("")             reference to abbreviation
  n                    occurrence of abbreviation
)

REVERSEABBREVIATION (
  n                    proof line number
  LINK("")             reference to abbreviation
  n                    occurrence of pattern to replace with
                        abbreviation
)

RENAMEFREEVARIABLE (
  n                    proof line number
  VAR(n)               rename this free subject variable
  VAR(n)               into this (non bound) subject variable
)

RENAMEBOUNDVARIABLE (
  n                    proof line number
  VAR(n)               rename this bound subject variable
  VAR(n)               into this (non free) subject variable
                        (as long as the new subject variable
                        didn't get bound a second time)
  n                    occurrence of quantifier with searched
                        bound subject variable
)

REPLACEPREDICATE (
  n                    proof line number
  PREDVAR(
    n,                 predicate number
    L(                 
      PATTERN(n)       + pair wise different pattern variables
    )
  FORMULA              formula that contains the same pattern
                        variables (for subject variables)
                       the set of free and bound subject variables
                       and the predicate variable shouldn't be
                       in reach of an quantor with subject variable
                       x, where x occurs in the replacement formula
)

GENERALIZATION (
  n 
  VAR(n)
)

PARTICULARIZATION (
  n
  VAR(n)
)


Text could include links to labels
In proofs external references could be made by "alias.label",
internal references are made by "label"

Version numbers are counted as follows:

,- main version, no compatibility guaranteed
| ,- compatible version, any reference should work further on 
| |   could have more paragraphs
| |   - compatible version (only different comments, or proofs, 
| |  |   no different imports. rule version might be lower
| |  |
0.00.00  normal formatting (could be extended: 0.00001.000001)

The file name is build by the name of the module, followed by 
a "." and the version number of the module and a "_" and the rule 
version number and the extension ".qedeq"


A local url will represent the web location it came from:

http://www.meyling.com/principia/logic/propaxiom_1.00.00_1.00.00.qedeq
 has the following local representation:
principia/buffer/http/www.meyling.com/principia/logic/propaxiom_1.00.00_1.00.00.qedeq

ftp://meyling.com/principia/logic/propaxiom_1.00.00_1.00.00.qedeq
 has the following local representation:
principia/buffer/ftp/www.meyling.com/principia/logic/basic_1.00.00_1.00.00.qedeq

Imports could have relative paths (relative to current module)

Once a module is successfully loaded it makes an entry into an 
global hash table (entry: local url). If there is already an entry
a conflict occurs.
If a module is needed (IMPORT), the urls are tried successive:
first the hash table is searched, then the urls itself.