QEDEQ 1.01 Schema This file is part of the project "Hilbert II" - http://www.qedeq.org Copyright 2000-2011, Michael Meyling <mime@qedeq.org>. Root element. Any QEDEQ document has this structure. If this XSD is changed don't forget to change also: the visitor org.qedeq.kernel.xml.mapper.Context2SimpleXPath, the traverser org.qedeq.kernel.se.visitor.QedeqNotNullTraverser, the builder org.qedeq.kernel.bo.service.QedeqVoBuilder, the visitor org.qedeq.kernel.se.visitor.QedeqVisitor, the visitor org.qedeq.kernel.se.visitor.AbstractModuleVisitor and the parsers. File specification, information 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>. Equivalence formula with two operands. First must be the predicate with pairwaise different subject variables as arguments. Second operand must be the defining formula for the predicate. 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 an initial predicate constant. The combination of attributes "name" and "arguments" must be unique within one QEDEQ module. LaTeX pattern for predicate with arguments as #<n>. Predicate constant we want to define. Arguments must be free subjectvariables. 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 an basic function constant. The combination of the attributes "name" and "arguments" must be unique within one QEDEQ module." LaTeX pattern for function with arguments as #<n>. Basic function constant that will be defined. Must have free subject variables as arguments (or none at all). 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. Definition of a function constant. The combination of the attributes "name" and "arguments" must be unique within one QEDEQ module. LaTeX pattern for function with arguments as #<n>. Defining formula for function constant. This must be an equals releation with the new function constant as first argument. 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. Axiom defines an operator. This operator can be elimnated by using this axiom. So this axiom is not neccessary for the theory. It leads just to a conservative language extension. A new meta rule. References to theorems or axioms. Additional description. Modifications to other existing rules. Version of this rule. In combination with the name it identifies a previous rule. Informal proof for this rule. Version of this rule. In combination with the name a rule must be unique. A theorem and it's proof. This formula is the theorem. Additional description. An informal proof. A formal proof. List of proof lines. Type for a proof line of a formal proof. A proofline that derives from previous derived formulas. New derived formula. References the rule and extra parameters that we need to get the new proof line. May be needed for back references. A proofline that includes a conditional proof. This is a usage of the deduction theorem. If the hypothesis formulas are H1, H2 and H3 and the last proof is A the proved formula is H1 & H2 & H3 -> A Can be used with rule version 0.02.00. We assume this formula. Replacement formula. May be needed for back references. Formal proof lines that can also make references to proof lines at higher level. We derive this formula as a conclusion. Replacement formula. May be needed for back references. Type for a rule that can derive a new formula. The rule Modus Ponens (or for short MP) is the sole rule of inference in propositional calculus. For rule version 0.01.00. Identifies a previous a proof line, axiom, definition or proposition. Must be of the form A -> B. Identifies a previous a proof line, axiom, definition or proposition. Must be same as B in ref1 Add already proven formula. For rule version 0.01.00. Identifies a previous a proof line, axiom, definition or proposition. Rename of bound subject variable at given occurrence by another one. For rule version 0.01.00. Replace this bound subject variable, by the second one. Marks the occurence of the bound subject variable. Substitute of free subject variable by term. For rule version 0.01.00. Replace this free subject variable. Replacement term. Substitute of function variable by term. For rule version 0.01.00. Replace this function variable. Replacement term. Substitute of predicate variable by formula. For rule version 0.01.00. Replace this predicate variable. Replacement formula. Rule of existential generalization. For rule version 0.01.00. Replace this free subject variable. Rule of universal generalization. For rule version 0.01.00. Replace this free subject variable. Type for an email. An email address. Type for a location. Location directory of module. Type for a level. Detail level.