# Project "Principia"
#
# Michael Meyling
# Stoltenstrasse 38
# 22119 Hamburg
# Germany
#
# @version $Revision: 0.00.51$
# @author  Michael Meyling
#
# Changes by Scott Little:
#     Lines 23, 33, (spelling);
#     36-37 (readability)

This text describes the format of a MODULE file for the rule version
1.00.00. A MODULE file contains a list of arguments in ASCII format.
An argument could be a list of argument itself.

There are two atomic arguments:
"" = Text              atomic argument, could be any quoted text
                        the character sequence "" within the quoted
                        text will be replaced by ":
                          "Alice said ""Hello"" to the queen."
n  = Counter           atomic argument, could be any positive integer
                        (1, 2, 3, ...)
Multiple arguments are separated by ","  (mostly left out in the
following description). White space between the arguments is
optional.


This description shows an explanation of the arguments that are used.

The following characters that precede an explanation have a special
meaning:
? = optional occurrence, this argument could be left out
* = zero or more occurrences
+ = one or more occurrences


MODULE (               A
  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 ("")     her or his email address
      )
    )
  )
  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
                        addressed directly
    )
  )
  USEDBY (             ? references to modules that use this one
    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 |
       DECLARATION |
       PROPOSITION
      }
      ""               ? following text
  )
)

DECLARATION (
  ""                   name of rule to declare
  ""                   short description of rule
  LINK("")             * reference(s) to needed axioms or propositions
)

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 (       A => B (referenced proof line)
                        and subject variable x doesn't occur in A
                        but x is free in B
                        then
                        A => For All x is B
                        could be concluded
  n                    proof line number
  VAR(n)               generaralize over this variable
)

PARTICULARIZATION (    A => B (referenced proof line)
                        and subject variable x doesn't occur in B
                        but x is free in A
                        then
                        Exists x with A => B
                        could be concluded
  n                    proof line number
  VAR(n)               specialize over this variable
)


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

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"
It is checked that the file name and the arguments of
HEADER( SPEC .. fit together.
All rules require the rule version to be greater or equal to
1.00.00

Every loaded module is saved in a local file buffer
Its file path represents the web location it came from:

http://www.meyling.com/principia/0_00_50/propaxiom_1.00.00_1.00.00.qedeq
 has the following local representation:
com/meyling/principia/buffer/http/www.meyling.com/principia/0_00_50/propaxiom_1.00.00_1.00.00.qedeq

ftp://www.meyling.com/principia/0_00_50/predaxiom_1.00.00_1.00.00.qedeq
 has the following local representation:
com/meyling/principia/buffer/ftp/www.meyling.com/principia/0_00_49/predaxiom_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.
If a module is needed (IMPORT), the urls are tried successive:
first the hash table is searched, then the local file buffer,
then the urls itself.