XML Schema Documentation

Table of Contents

top

Schema Document Properties

Target Namespace None
Element and Attribute Namespaces
  • Global element and attribute declarations belong to this schema's target namespace.
  • By default, local element declarations belong to this schema's target namespace.
  • By default, local attribute declarations have no namespace.
Documentation QEDEQ 1.0 Schema This file is part of the project "Hilbert II" - http://www.qedeq.org Copyright 2000-2006, Michael Meyling <mime@qedeq.org>.

Declared Namespaces

Prefix Namespace
xml http://www.w3.org/XML/1998/namespace
xs http://www.w3.org/2001/XMLSchema
Schema Component Representation
<xs:schema elementFormDefault="qualified">
...
</xs:schema>
top

Global Declarations

Element: AND

  • This element can be used wherever the following element is referenced:
Name AND
Type Locally-defined complex type
Nillable no
Abstract no
Documentation Logical language: Logical conjunction.
XML Instance Representation
<AND>
<FORMULATYPE> ... </FORMULATYPE> [1..*]
</AND>
Schema Component Representation
<xs:element name="AND" substitutionGroup="FORMULATYPE">
<xs:complexType>
<xs:sequence>
<xs:element ref=" FORMULATYPE " maxOccurs="unbounded"/>
</xs:sequence>
</xs:complexType>
</xs:element>
top

Element: AXIOM

  • This element can be used wherever the following element is referenced:
Name AXIOM
Type Locally-defined complex type
Nillable no
Abstract no
Documentation Mathematical axiom.
XML Instance Representation
<AXIOM>
<FORMULA> ... </FORMULA> [1] ?
<DESCRIPTION> [0..1] ?
<LATEX> ... </LATEX> [1..*]
</DESCRIPTION>
</AXIOM>
Schema Component Representation
<xs:element name="AXIOM" substitutionGroup="NODETYPE">
<xs:complexType>
<xs:sequence>
<xs:element ref=" FORMULA "/>
<xs:element name="DESCRIPTION" minOccurs="0">
<xs:complexType>
<xs:sequence>
<xs:element ref=" LATEX " minOccurs="1" maxOccurs="unbounded"/>
</xs:sequence>
</xs:complexType>
</xs:element>
</xs:sequence>
</xs:complexType>
</xs:element>
top

Element: CLASS

  • This element can be used wherever the following element is referenced:
Name CLASS
Type Locally-defined complex type
Nillable no
Abstract no
Documentation Logical language: Class described by property. For example {x | x = x }.
XML Instance Representation
<CLASS>
<VAR> ... </VAR> [1]
<FORMULATYPE> ... </FORMULATYPE> [1]
</CLASS>
Schema Component Representation
<xs:element name="CLASS" substitutionGroup="TERMTYPE">
<xs:complexType>
<xs:sequence>
<xs:element ref=" VAR " minOccurs="1" maxOccurs="1"/>
<xs:element ref=" FORMULATYPE " minOccurs="1" maxOccurs="1"/>
</xs:sequence>
</xs:complexType>
</xs:element>
top

Element: DEFINITION_FUNCTION

  • This element can be used wherever the following element is referenced:
Name DEFINITION_FUNCTION
Type Locally-defined complex type
Nillable no
Abstract no
Documentation Definition of a function. The attributes "name" and "arguments" must be unique within one QEDEQ module.
XML Instance Representation
<DEFINITION_FUNCTION
arguments=" xs:NMTOKEN [1] ?"
name=" xs:string [1] ?">
<LATEXPATTERN> xs:string </LATEXPATTERN> [1] ?
<VARLIST> [0..1] ?
<VAR> ... </VAR> [1..*]
</VARLIST>
<TERM> ... </TERM> [0..1]
<DESCRIPTION> [0..1] ?
<LATEX> ... </LATEX> [1..*]
</DESCRIPTION>
</DEFINITION_FUNCTION>
Schema Component Representation
<xs:element name="DEFINITION_FUNCTION" substitutionGroup="NODETYPE">
<xs:complexType>
<xs:sequence>
<xs:element name="LATEXPATTERN" type=" xs:string "/>
<xs:element name="VARLIST" minOccurs="0">
<xs:complexType>
<xs:sequence>
<xs:element ref=" VAR " minOccurs="1" maxOccurs="unbounded"/>
</xs:sequence>
</xs:complexType>
</xs:element>
<xs:element ref=" TERM " minOccurs="0"/>
<xs:element name="DESCRIPTION" minOccurs="0">
<xs:complexType>
<xs:sequence>
<xs:element ref=" LATEX " minOccurs="1" maxOccurs="unbounded"/>
</xs:sequence>
</xs:complexType>
</xs:element>
</xs:sequence>
<xs:attribute name="arguments" type=" xs:NMTOKEN " use="required"/>
<xs:attribute name="name" type=" xs:string " use="required"/>
</xs:complexType>
</xs:element>
top

Element: DEFINITION_PREDICATE

  • This element can be used wherever the following element is referenced:
Name DEFINITION_PREDICATE
Type Locally-defined complex type
Nillable no
Abstract no
Documentation Definition of a predicate constant. The attributes "name" and "arguments" must be unique within one QEDEQ module.
XML Instance Representation
<DEFINITION_PREDICATE
arguments=" xs:NMTOKEN [1] ?"
name=" xs:string [1] ?">
<LATEXPATTERN> xs:string </LATEXPATTERN> [1] ?
<VARLIST> [0..1] ?
<VAR> ... </VAR> [1..*]
</VARLIST>
<FORMULA> ... </FORMULA> [0..1]
<DESCRIPTION> [0..1] ?
<LATEX> ... </LATEX> [1..*]
</DESCRIPTION>
</DEFINITION_PREDICATE>
Schema Component Representation
<xs:element name="DEFINITION_PREDICATE" substitutionGroup="NODETYPE">
<xs:complexType>
<xs:sequence>
<xs:element name="LATEXPATTERN" type=" xs:string "/>
<xs:element name="VARLIST" minOccurs="0">
<xs:complexType>
<xs:sequence>
<xs:element ref=" VAR " minOccurs="1" maxOccurs="unbounded"/>
</xs:sequence>
</xs:complexType>
</xs:element>
<xs:element ref=" FORMULA " minOccurs="0"/>
<xs:element name="DESCRIPTION" minOccurs="0">
<xs:complexType>
<xs:sequence>
<xs:element ref=" LATEX " minOccurs="1" maxOccurs="unbounded"/>
</xs:sequence>
</xs:complexType>
</xs:element>
</xs:sequence>
<xs:attribute name="arguments" type=" xs:NMTOKEN " use="required"/>
<xs:attribute name="name" type=" xs:string " use="required"/>
</xs:complexType>
</xs:element>
top

Element: EQUI

  • This element can be used wherever the following element is referenced:
Name EQUI
Type Locally-defined complex type
Nillable no
Abstract no
Documentation Logical language: Logical equivalence.
XML Instance Representation
<EQUI>
<FORMULATYPE> ... </FORMULATYPE> [1..*]
</EQUI>
Schema Component Representation
<xs:element name="EQUI" substitutionGroup="FORMULATYPE">
<xs:complexType>
<xs:sequence>
<xs:element ref=" FORMULATYPE " maxOccurs="unbounded"/>
</xs:sequence>
</xs:complexType>
</xs:element>
top

Element: EXISTS

  • This element can be used wherever the following element is referenced:
Name EXISTS
Type Locally-defined complex type
Nillable no
Abstract no
Documentation Logical language: Logical existence quantor.
XML Instance Representation
<EXISTS>
<VAR> ... </VAR> [1]
<FORMULATYPE> ... </FORMULATYPE> [1]
<FORMULATYPE> ... </FORMULATYPE> [0..1]
</EXISTS>
Schema Component Representation
<xs:element name="EXISTS" substitutionGroup="FORMULATYPE">
<xs:complexType>
<xs:sequence>
<xs:element ref=" VAR " minOccurs="1"/>
<xs:element ref=" FORMULATYPE "/>
<xs:element ref=" FORMULATYPE " minOccurs="0"/>
</xs:sequence>
</xs:complexType>
</xs:element>
top

Element: EXISTSU

  • This element can be used wherever the following element is referenced:
Name EXISTSU
Type Locally-defined complex type
Nillable no
Abstract no
Documentation Logical language: Special logical existence quantor. Proposes the existence of an unique element.
XML Instance Representation
<EXISTSU>
<VAR> ... </VAR> [1]
<FORMULATYPE> ... </FORMULATYPE> [1]
<FORMULATYPE> ... </FORMULATYPE> [0..1]
</EXISTSU>
Schema Component Representation
<xs:element name="EXISTSU" substitutionGroup="FORMULATYPE">
<xs:complexType>
<xs:sequence>
<xs:element ref=" VAR " minOccurs="1"/>
<xs:element ref=" FORMULATYPE "/>
<xs:element ref=" FORMULATYPE " minOccurs="0"/>
</xs:sequence>
</xs:complexType>
</xs:element>
top

Element: FORALL

  • This element can be used wherever the following element is referenced:
Name FORALL
Type Locally-defined complex type
Nillable no
Abstract no
Documentation Logical language: Logical universal quantor.
XML Instance Representation
<FORALL>
<VAR> ... </VAR> [1]
<FORMULATYPE> ... </FORMULATYPE> [1]
<FORMULATYPE> ... </FORMULATYPE> [0..1]
</FORALL>
Schema Component Representation
<xs:element name="FORALL" substitutionGroup="FORMULATYPE">
<xs:complexType>
<xs:sequence>
<xs:element ref=" VAR " minOccurs="1"/>
<xs:element ref=" FORMULATYPE "/>
<xs:element ref=" FORMULATYPE " minOccurs="0"/>
</xs:sequence>
</xs:complexType>
</xs:element>
top

Element: FORMULA

Name FORMULA
Type Locally-defined complex type
Nillable no
Abstract no
Documentation Logical language: Formula.
XML Instance Representation
<FORMULA>
<FORMULATYPE> ... </FORMULATYPE> [1]
</FORMULA>
Schema Component Representation
<xs:element name="FORMULA">
<xs:complexType>
<xs:sequence>
<xs:element ref=" FORMULATYPE "/>
</xs:sequence>
</xs:complexType>
</xs:element>
top

Element: FORMULATYPE

Name FORMULATYPE
Type anyType
Nillable no
Abstract yes
Documentation Type for a formula.
XML Instance Representation
<FORMULATYPE> ... </FORMULATYPE>
Schema Component Representation
<xs:element name="FORMULATYPE" abstract="true"/>
top

Element: FUNCON

  • This element can be used wherever the following element is referenced:
Name FUNCON
Type Locally-defined complex type
Nillable no
Abstract no
Documentation Logical language: Function constant.
XML Instance Representation
<FUNCON
ref=" xs:string [1]">
<TERMTYPE> ... </TERMTYPE> [0..*]
</FUNCON>
Schema Component Representation
<xs:element name="FUNCON" substitutionGroup="TERMTYPE">
<xs:complexType>
<xs:sequence>
<xs:element ref=" TERMTYPE " minOccurs="0" maxOccurs="unbounded"/>
</xs:sequence>
<xs:attribute name="ref" type=" xs:string " use="required"/>
</xs:complexType>
</xs:element>
top

Element: FUNVAR

  • This element can be used wherever the following element is referenced:
Name FUNVAR
Type Locally-defined complex type
Nillable no
Abstract no
Documentation Logical language: Function variable.
XML Instance Representation
<FUNVAR
id=" xs:string [1]">
<TERMTYPE> ... </TERMTYPE> [1..*]
</FUNVAR>
Schema Component Representation
<xs:element name="FUNVAR" substitutionGroup="TERMTYPE">
<xs:complexType>
<xs:sequence>
<xs:element ref=" TERMTYPE " maxOccurs="unbounded"/>
</xs:sequence>
<xs:attribute name="id" type=" xs:string " use="required"/>
</xs:complexType>
</xs:element>
top

Element: IMPL

  • This element can be used wherever the following element is referenced:
Name IMPL
Type Locally-defined complex type
Nillable no
Abstract no
Documentation Logical language: Logical implication.
XML Instance Representation
<IMPL>
<FORMULATYPE> ... </FORMULATYPE> [1]
<FORMULATYPE> ... </FORMULATYPE> [1]
</IMPL>
Schema Component Representation
<xs:element name="IMPL" substitutionGroup="FORMULATYPE">
<xs:complexType>
<xs:sequence>
<xs:element ref=" FORMULATYPE "/>
<xs:element ref=" FORMULATYPE "/>
</xs:sequence>
</xs:complexType>
</xs:element>
top

Element: LATEX

Name LATEX
Type Locally-defined complex type
Nillable no
Abstract no
Documentation For each supported language entry one can find a LaTeX text here.
XML Instance Representation
<LATEX
language=" xs:language [0..1]">
xs:string
</LATEX>
Schema Component Representation
<xs:element name="LATEX">
<xs:complexType>
<xs:simpleContent>
<xs:extension base=" xs:string ">
<xs:attribute name="language" type=" xs:language " use="optional"/>
</xs:extension>
</xs:simpleContent>
</xs:complexType>
</xs:element>
top

Element: NODE

  • This element can be used wherever the following element is referenced:
Name NODE
Type Locally-defined complex type
Nillable no
Abstract no
Documentation This part is the smallest unit and corresponds to the LaTeX item subsection. But it also carries formal AXIOMs, THEOREMS or else.
XML Instance Representation
<NODE
id=" xs:string [1] ?"
level=" xs:string [0..1] ?">
<NAME> [0..1] ?
<LATEX> ... </LATEX> [1..*]
</NAME>
<TITLE> ... </TITLE> [0..1] ?
<PRECEDING> [0..1] ?
<LATEX> ... </LATEX> [1..*]
</PRECEDING>
<NODETYPE> ... </NODETYPE> [1] ?
<SUCCEEDING> [0..1] ?
<LATEX> ... </LATEX> [1..*]
</SUCCEEDING>
</NODE>
Schema Component Representation
<xs:element name="NODE" substitutionGroup="SUBSECTIONTYPE">
<xs:complexType>
<xs:sequence>
<xs:element name="NAME" minOccurs="0">
<xs:complexType>
<xs:sequence>
<xs:element ref=" LATEX " maxOccurs="unbounded"/>
</xs:sequence>
</xs:complexType>
</xs:element>
<xs:element ref=" TITLE " minOccurs="0"/>
<xs:element name="PRECEDING" minOccurs="0">
<xs:complexType>
<xs:sequence>
<xs:element ref=" LATEX " minOccurs="1" maxOccurs="unbounded"/>
</xs:sequence>
</xs:complexType>
</xs:element>
<xs:element ref=" NODETYPE "/>
<xs:element name="SUCCEEDING" minOccurs="0">
<xs:complexType>
<xs:sequence>
<xs:element ref=" LATEX " minOccurs="1" maxOccurs="unbounded"/>
</xs:sequence>
</xs:complexType>
</xs:element>
</xs:sequence>
<xs:attribute name="id" type=" xs:string " use="required"/>
<xs:attribute name="level" type=" xs:string "/>
</xs:complexType>
</xs:element>
top

Element: NODETYPE

Name NODETYPE
Type anyType
Nillable no
Abstract yes
Documentation Type for a node. This might be an AXIOM, THEOREM or something else.
XML Instance Representation
<NODETYPE> ... </NODETYPE>
Schema Component Representation
<xs:element name="NODETYPE" abstract="true"/>
top

Element: NOT

  • This element can be used wherever the following element is referenced:
Name NOT
Type Locally-defined complex type
Nillable no
Abstract no
Documentation Logical language: Logical negation.
XML Instance Representation
<NOT>
<FORMULATYPE> ... </FORMULATYPE> [1]
</NOT>
Schema Component Representation
<xs:element name="NOT" substitutionGroup="FORMULATYPE">
<xs:complexType>
<xs:sequence>
<xs:element ref=" FORMULATYPE "/>
</xs:sequence>
</xs:complexType>
</xs:element>
top

Element: OR

  • This element can be used wherever the following element is referenced:
Name OR
Type Locally-defined complex type
Nillable no
Abstract no
Documentation Logical language: Logical disjunction.
XML Instance Representation
<OR>
<FORMULATYPE> ... </FORMULATYPE> [1..*]
</OR>
Schema Component Representation
<xs:element name="OR" substitutionGroup="FORMULATYPE">
<xs:complexType>
<xs:sequence>
<xs:element ref=" FORMULATYPE " maxOccurs="unbounded"/>
</xs:sequence>
</xs:complexType>
</xs:element>
top

Element: PREDCON

  • This element can be used wherever the following element is referenced:
Name PREDCON
Type Locally-defined complex type
Nillable no
Abstract no
Documentation Logical language: Predicate constant.
XML Instance Representation
<PREDCON
ref=" xs:NMTOKEN [1]">
<TERMTYPE> ... </TERMTYPE> [0..*]
</PREDCON>
Schema Component Representation
<xs:element name="PREDCON" substitutionGroup="FORMULATYPE">
<xs:complexType>
<xs:sequence>
<xs:element ref=" TERMTYPE " minOccurs="0" maxOccurs="unbounded"/>
</xs:sequence>
<xs:attribute name="ref" type=" xs:NMTOKEN " use="required"/>
</xs:complexType>
</xs:element>
top

Element: PREDVAR

  • This element can be used wherever the following element is referenced:
Name PREDVAR
Type Locally-defined complex type
Nillable no
Abstract no
Documentation Logical language: Predicate variable.
XML Instance Representation
<PREDVAR
id=" xs:string [1]">
<TERMTYPE> ... </TERMTYPE> [0..*]
</PREDVAR>
Schema Component Representation
<xs:element name="PREDVAR" substitutionGroup="FORMULATYPE">
<xs:complexType>
<xs:sequence>
<xs:element ref=" TERMTYPE " minOccurs="0" maxOccurs="unbounded"/>
</xs:sequence>
<xs:attribute name="id" type=" xs:string " use="required"/>
</xs:complexType>
</xs:element>
top

Element: QEDEQ

Name QEDEQ
Type Locally-defined complex type
Nillable no
Abstract no
Documentation Root element. Any QEDEQ document has this structure.
XML Instance Representation
<QEDEQ>
<HEADER
email=" EMAILTYPE [0..1] ?"> [1] ?
<SPECIFICATION> ... </SPECIFICATION> [1] ?
<TITLE> ... </TITLE> [1] ?
<ABSTRACT> [1] ?
<LATEX> ... </LATEX> [1..*]
</ABSTRACT>
<AUTHORS> [1] ?
<AUTHOR
email=" EMAILTYPE [0..1] ?"> [1] ?
<NAME> [1] ?
<LATEX> ... </LATEX> [1]
</NAME>
</AUTHOR>
</AUTHORS>
<IMPORTS> [0..1] ?
<IMPORT
label=" xs:NMTOKEN [1] ?"> [1..*] ?
</IMPORT>
</IMPORTS>
<USEDBY> [0..1] ?
</USEDBY>
</HEADER>
<CHAPTER
noNumber=" xs:boolean [0..1] ?"> [1..*] ?
<TITLE> ... </TITLE> [1] ?
<INTRODUCTION> [1] ?
<LATEX> ... </LATEX> [1..*]
</INTRODUCTION>
<SECTION
noNumber=" xs:boolean [0..1] ?"> [0..*] ?
<TITLE> ... </TITLE> [1] ?
<INTRODUCTION> [0..1] ?
<LATEX> ... </LATEX> [1..*]
</INTRODUCTION>
<SUBSECTIONS> [0..1] ?
</SUBSECTIONS>
</SECTION>
</CHAPTER>
<BIBLIOGRAPHY> [0..1] ?
<ITEM
label=" xs:NMTOKEN [1] ?"> [1..*] ?
<LATEX> ... </LATEX> [1..*]
</ITEM>
</BIBLIOGRAPHY>
</QEDEQ>
Schema Component Representation
<xs:element name="QEDEQ">
<xs:complexType>
<xs:sequence>
<xs:element name="HEADER">
<xs:complexType>
<xs:sequence>
<xs:element ref=" SPECIFICATION "/>
<xs:element ref=" TITLE "/>
<xs:element name="ABSTRACT">
<xs:complexType>
<xs:sequence>
<xs:element ref=" LATEX " maxOccurs="unbounded"/>
</xs:sequence>
</xs:complexType>
</xs:element>
<xs:element name="AUTHORS">
<xs:complexType>
<xs:sequence>