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.

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 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 An axiom formula.
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: DEFINITION

  • This element can be used wherever the following element is referenced:
Name DEFINITION
Type Locally-defined complex type
Nillable no
Abstract no
Documentation Definition of predicate or term constants.
XML Instance Representation
<DEFINITION
kind=" xs:string [1]"
arguments=" xs:NMTOKEN [1]">
<LATEXPATTERN> xs:string </LATEXPATTERN> [1]
<VARLIST> [1]
<VAR> ... </VAR> [1..*]
</VARLIST>
Start Sequence [0..1]
<FORMULA> ... </FORMULA> [1]
End Sequence
<DESCRIPTION> [0..1] ?
<LATEX> ... </LATEX> [1..*]
</DESCRIPTION>
</DEFINITION>
Schema Component Representation
<xs:element name="DEFINITION" substitutionGroup="NODETYPE">
<xs:complexType>
<xs:sequence>
<xs:element name="LATEXPATTERN" type=" xs:string "/>
<xs:element name="VARLIST">
<xs:complexType>
<xs:sequence>
<xs:element ref=" VAR " maxOccurs="unbounded"/>
</xs:sequence>
</xs:complexType>
</xs:element>
<xs:sequence minOccurs="0">
<xs:element ref=" FORMULA "/>
</xs:sequence>
<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="kind" type=" xs:string " use="required"/>
<xs:attribute name="arguments" type=" xs:NMTOKEN " 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 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 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 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 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
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
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
XML Instance Representation
<FUNCON
id=" xs:string [1]">
<TERMTYPE> ... </TERMTYPE> [1..*]
</FUNCON>
Schema Component Representation
<xs:element name="FUNCON" 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: FUNVAR

  • This element can be used wherever the following element is referenced:
Name FUNVAR
Type Locally-defined complex type
Nillable no
Abstract no
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 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
XML Instance Representation
<LATEX
language=" xs:language [0..1]"
level=" LEVELTYPE [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:attribute name="level" type=" LEVELTYPE "/>
</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 carries formulas.
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
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 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 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
XML Instance Representation
<PREDCON
ref=" xs:NMTOKEN [1]">
<TERMTYPE> ... </TERMTYPE> [1..*]
</PREDCON>
Schema Component Representation
<xs:element name="PREDCON" substitutionGroup="FORMULATYPE">
<xs:complexType>
<xs:sequence>
<xs:element ref=" TERMTYPE " 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
XML Instance Representation
<PREDVAR
id=" xs:string [1]">
<TERMTYPE> ... </TERMTYPE> [1..*]
</PREDVAR>
Schema Component Representation
<xs:element name="PREDVAR" substitutionGroup="FORMULATYPE">
<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: QEDEQ

Name QEDEQ
Type Locally-defined complex type
Nillable no
Abstract no
Documentation Root element.
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>
</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>
<xs:element name="AUTHOR">
<xs:complexType>
<xs:sequence>
<xs:element name="NAME">
<xs:complexType>
<xs:sequence>
<xs:element ref=" LATEX "/>
</xs:sequence>
</xs:complexType>
</xs:element>
<-- TODO mime <xs:element ref="LATEX"/> -->
</xs:sequence>
<xs:attribute name="email" type=" EMAILTYPE "/>
</xs:complexType>
</xs:element>
</xs:sequence>
</xs:complexType>
</xs:element>
<xs:element name="IMPORTS" minOccurs="0">
<xs:complexType>
<xs:sequence>
<xs:element name="IMPORT" maxOccurs="unbounded">
<xs:complexType>
<xs:sequence>
<xs:element ref=" SPECIFICATION "/>
</xs:sequence>
<xs:attribute name="label" type=" xs:NMTOKEN " use="required"/>
</xs:complexType>
</xs:element>
</xs:sequence>
</xs:complexType>
</xs:element>
<xs:element name="USEDBY" minOccurs="0">
<xs:complexType>
<xs:sequence>
<xs:element ref=" SPECIFICATION "/>
</xs:sequence>
</xs:complexType>
</xs:element>
</xs:sequence>
<xs:attribute name="email" type=" EMAILTYPE "/>
</xs:complexType>
</xs:element>
<xs:element name="CHAPTER" maxOccurs="unbounded">
<xs:complexType>
<xs:sequence>
<xs:element ref=" TITLE "/>
<xs:element name="INTRODUCTION">
<xs:complexType>
<xs:sequence>
<xs:element ref=" LATEX " minOccurs="1" maxOccurs="unbounded"/>
</xs:sequence>
</xs:complexType>
</xs:element>
<xs:element name="SECTION" minOccurs="0" maxOccurs="unbounded">
<xs:complexType>
<xs:sequence>
<xs:element ref=" TITLE "/>
<xs:element name="INTRODUCTION" minOccurs="0">
<xs:complexType>
<xs:sequence>
<xs:element ref=" LATEX " minOccurs="1" maxOccurs="unbounded"/>
</xs:sequence>
</xs:complexType>
</xs:element>
<xs:element name="SUBSECTIONS" minOccurs="0">
<xs:complexType>
<xs:sequence>
<xs:element ref=" SUBSECTIONTYPE " minOccurs="1" maxOccurs="unbounded"/>
</xs:sequence>
</xs:complexType>
</xs:element>
</xs:sequence>
<xs:attribute name="noNumber" type=" xs:boolean " use="optional"/>
</xs:complexType>
</xs:element>
</xs:sequence>
<xs:attribute name="noNumber" type=" xs:boolean " use="optional"/>
</xs:complexType>
</xs:element>
</xs:sequence>
</xs:complexType>
</xs:element>
top

Element: RULE

  • This element can be used wherever the following element is referenced:
Name RULE
Type Locally-defined complex type
Nillable no
Abstract no
Documentation A new meta rule.
XML Instance Representation
<RULE
name=" xs:string [1]">
<LINK
id=" xs:string [1]"/> [0..*] ?
<DESCRIPTION> [1] ?
<LATEX> ... </LATEX> [1..*]
</DESCRIPTION>
<PROOF
kind=" xs:NMTOKEN [1]"
level=" xs:string [1]"> [0..*]
<LATEX> ... </LATEX> [1..*]
</PROOF>
</RULE>
Schema Component Representation
<xs:element name="RULE" substitutionGroup="NODETYPE">
<xs:complexType>
<xs:sequence>
<xs:element name="LINK" minOccurs="0" maxOccurs="unbounded">
<xs:complexType>
<xs:attribute name="id" type=" xs:string " use="required"/>
</xs:complexType>
</xs:element>
<xs:element name="DESCRIPTION" minOccurs="1">
<xs:complexType>
<xs:sequence>
<xs:element ref=" LATEX " minOccurs="1" maxOccurs="unbounded"/>
</xs:sequence>
</xs:complexType>
</xs:element>
<xs:element name="PROOF" minOccurs="0" maxOccurs="unbounded">
<xs:complexType>
<xs:sequence>
<xs:element ref=" LATEX " minOccurs="1" maxOccurs="unbounded"/>
</xs:sequence>
<xs:attribute name="kind" type=" xs:NMTOKEN " use="required"/>
<xs:attribute name="level" type=" xs:string " use="required"/>
</xs:complexType>
</xs:element>
</xs:sequence>
<xs:attribute name="name" type=" xs:string " use="required<