|
Prototype / PMII QEDEQ Module / Module
This is an description of a qedeq module file (for version 0.00.53).
This text describes the format of a qedeq MODULE file for the rule version
1.00.00. A qedeq 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 ( main structure
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) generalize 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.qedeq.org/0_00_53/propaxiom_1.00.00_1.00.00.qedeq
has the following local representation:
buffer/http/www.qedeq.org/0_00_53/propaxiom_1.00.00_1.00.00.qedeq
ftp://www.qedeq.org/0_00_53/predaxiom_1.00.00_1.00.00.qedeq
has the following local representation:
buffer/ftp/www.qedeq.org/0_00_53/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 during runtime.
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.
|