QEDEQ 1.0 Schema This file is part of the project "Hilbert II" - http://www.qedeq.org Copyright 2000-2008, Michael Meyling <mime@qedeq.org>. Root element. Any QEDEQ document has this structure. File specification, infromation about the authors, imports of other QEDEQ modules and so on are part of the header. File specification of this module. What is the name of this module and where to find it. Title of this QEDEQ module. Module contents description. List of authors of this module. Name and email address of author. Name of author. Email address of author. References to other QEDEQ modules that are a precondition for this one. A single reference to a QEDEQ module that must be imported. File specification of QEDEQ module to import. What is the name of this module and where to find it. Prefix for labels from referenced QEDEQ module. References to labels in the referenced module must be extended with this prefix. This label must be unique within this module. List of QEDEQ modules which use (import) this module. This information could be incorrect due to changes in the referenced modules. Also newly created modules could be missing. To keep these entries correct the external module administrator should email the module administrator of this module. This label must be unique within this module. File specification of QEDEQ module that depends on this one. What is the name of this module and where to find it. Email address for administration services of this QEDEQ module. This part corresponds to the LaTeX item chapter. Chapter title. Chapter contents description. Section of chapter. Section title. Section contents description. List of subsections. Should this section be numbered?. Should this section be numbered?. Literature references. Single literature reference. Label for this reference. This label must be unique within this module. Title of a text segment. For each supported language entry one can find a LaTeX text here. File specification of this module. What is the name of this module and where to find it. List of locations to find the QEDEQ module. Location of a QEDEQ module. URL to location of a QEDEQ module directory. Technical name of QEDEQ module. Also the main part of the file name. The complete name has ".xml" appended. Together with an LOCATION the complete path to a QEDEQ module can be build. Locical rule version that is needed to be able to make the derivations made in the QEDEQ module. Type for a term. Logical language: Term. Logical language: Subject variable. Identifies a subject variable. Also used as a LaTeX expression for this variable. Logical language: Function constant. References a function constant definition. The function constant must be defined within this or an imported module. For an external reference the name must begin with the appropiate label follwed by an dot. Logical language: Function variable. Identifies a function variable. Also used as a LaTeX expression for this variable. Logical language: Class described by property. For example {x | x = x }. Logical language: Intersection about all classes that fullfil a property. Logical language: Union about all classes that fullfil a property. Logical language: Formula. Type for a formula. Logical language: Predicate constant. References a predicate constant definition. The predicate constant must be defined within this or an imported module. For an external reference the name must begin with the appropiate label follwed by an dot. Logical language: Predicate variable. Identifies a predicate variable. Also used as a LaTeX expression for this variable. Logical language: Logical existential quantifier. Logical language: Logical uniqueness quantifier. Proposes the existence of an unique element. Logical language: Logical universal quantifier. Logical language: Logical conjunction. Logical language: Logical disjunction. Logical language: Logical equivalence. Logical language: Logical implication. Logical language: Logical negation. Type for a subsection. This a normal LaTeX subsection of a section. Subsection title. The LaTeX text of this subsection. Reference id for this subsection. Detail level of this subsection. This part is the smallest unit and corresponds to the LaTeX item subsection. But it also carries formal AXIOMs, THEOREMS or else. Short text to describe this item. Used when referencing to this. Subsection title. Mathematical meat. For example an axiom, proposition, definition etc. Reference id for this node. Detail level of this subsection. Text that precedes the mathematical meat. Text that succeeds mathematical meat. Type for a node. This might be an AXIOM, THEOREM or something else. Definition of a predicate constant. The attributes "name" and "arguments" must be unique within one QEDEQ module. LaTeX pattern for predicate with arguments as #<n>. List of predicate arguments. Additional description. Number of arguments for the new predicate. Name for the new predicate. This name must not occur as a label within this module. Definition of a function. The attributes "name" and "arguments" must be unique within one QEDEQ module. The " LaTeX pattern for function with arguments as #<n>. List of function arguments. Additional description. Number of arguments for the new function. Name for the new function. This name must not occur as a label within this module. Mathematical axiom. An axiom formula. Additional description. A new meta rule. References to theorems or axioms. Additional description. Informal proof for this rule. A theorem and it's proof. This formula is the theorem. Additional description. An informal proof. A formal proof. Type for an email. An email address. Type for a location. Location directory of module. Type for a level. Detail level.