--- /dev/null
+<?xml version="1.0"?>
+
+<!-- Rdf Schema definition for CIC XML files:
+xmlns:h="http://www.cs.unibo.it/~schena/schema-h#" -->
+
+<!DOCTYPE rdf:RDF [
+ <!ENTITY rdfns 'http://www.w3.org/1999/02/22-rdf-syntax-ns#'>
+ <!ENTITY rdfsns 'http://www.w3.org/2000/01/rdf-schema#'>
+ <!ENTITY hthns 'http://www.cs.unibo.it/~schena/schema-hth#'>
+ <!ENTITY hns 'http://www.cs.unibo.it/~schena/schema-h#'>
+ <!ENTITY xschemans 'http://www.w3.org/1999/XMLSchema-datatypes#'>
+ <!ENTITY dcns 'http://www.cs.unibo.it/~schena/dces#'>
+ <!ENTITY dcqns 'http://www.cs.unibo.it/~schena/dcq#'>
+ ]>
+
+<rdf:RDF xml:lang="en"
+ xmlns:rdf="&rdfns;"
+ xmlns:rdfs="&rdfsns;"
+ xmlns:hth="&hthns;"
+ xmlns:h="&hns;"
+ xmlns:xs="&xschemans;"
+ xmlns:dc="&dcns;"
+ xmlns:dcq="&dcqns;">
+
+<!-- RICORDA: metadati solo su oggetto (come teoria ma piu' specifici) (non
+distinzione tipi di body) e non ridondanze se non riducono il numero di doc
+da parsare -->
+
+<!-- Description of Schema -->
+
+<rdf:Description rdf:about="&hns;">
+ <rdfs:label>The HELM Element Set v0.1</rdfs:label>
+ <dc:title>The HELM Object Element Set v0.1</dc:title>
+ <dc:publisher>The HELM Project</dc:publisher>
+ <dc:description>The HELM metadata vocabulary is a simple vocabulary
+ intended to facilitate discovery of mathematical resources.
+ </dc:description>
+ <dc:language>English</dc:language>
+ <dc:relation rdf:resource="http://ww.cs.unibo.it/helm/"/>
+ <dcq:isRequiredBy rdf:resource="&hns;"/>
+ <dcq:conformsTo rdf:resource="http://www.w3.org/RDF/"/>
+ <dcq:issued>2000-6-3</dcq:issued>
+ <dcq:modified>2002-9-6</dcq:modified>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdf:Description>
+
+
+<!-- Classes -->
+
+<rdfs:Class rdf:about="&hns;Object">
+ <rdfs:comment>Mathematical objects represented by a CIC XML
+file</rdfs:comment>
+ <rdfs:subClassOf rdf:resource="&hthns;MathResource"/>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdfs:Class>
+
+<!-- Objects can inherit its dc properties -->
+<rdfs:Class rdf:about="&hns;DirectoryOfObjects">
+ <rdfs:comment>Mathematical resources (directories) represented by sets
+of CIC XML files, contained in the tree that has the dir as root </rdfs:comment>
+ <rdfs:subClassOf rdf:resource="&hthns;MathResource"/>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdfs:Class>
+
+<rdfs:Class rdf:about="&hns;Statement">
+ <rdfs:comment>Types of objects</rdfs:comment>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdfs:Class>
+
+<rdfs:Class rdf:about="&hns;Body">
+ <rdfs:comment>Terms of objects</rdfs:comment>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdfs:Class>
+
+<rdfs:Class rdf:about="&hns;Occurrence">
+ <rdfs:comment>Occurrences of an object inside an object</rdfs:comment>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdfs:Class>
+
+<rdfs:Class rdf:about="&hns;Position">
+ <rdfs:comment>Positions of occurrences of an object inside an object</rdfs:comment>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdfs:Class>
+
+<rdfs:Class rdf:about="&hns;Postit">
+ <rdfs:comment>Additional information associated to fragments of the objects</rdfs:comment>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdfs:Class>
+
+<rdfs:Class rdf:about="&hns;Const">
+ <rdfs:comment>Constants in the body of an object</rdfs:comment>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdfs:Class>
+
+<rdfs:Class rdf:about="&hns;StatementId">
+ <rdfs:comment>Identifiers in the statement</rdfs:comment>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdfs:Class>
+
+<rdfs:Class rdf:about="&hns;BodyId">
+ <rdfs:comment>Identifiers in the body</rdfs:comment>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdfs:Class>
+
+<rdfs:Class rdf:about="&hns;ImplArg">
+ <rdfs:comment>Implicit arguments</rdfs:comment>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdfs:Class>
+
+<!-- Instances of the class h:Position -->
+
+<h:Position rdf:about="&hns;MainHypothesis">
+ <rdfs:comment>Occurrences of an object in head position of some hypothesis
+ of an object statement</rdfs:comment>
+ <rdf:type rdf:resource="&rdfsns;Class"/>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</h:Position>
+
+<h:Position rdf:about="InHypothesis">
+ <rdfs:comment>Occurrences of an object in the hypotheses of an object
+ statement</rdfs:comment>
+ <rdf:type rdf:resource="&rdfsns;Class"/>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</h:Position>
+
+<h:Position rdf:about="&hns;MainConclusion">
+ <rdfs:comment>Occurrences of an object in head position of the
+ conclusion of an object statement</rdfs:comment>
+ <rdf:type rdf:resource="&rdfsns;Class"/>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</h:Position>
+
+<h:Position rdf:about="&hns;InConclusion">
+ <rdfs:comment>Occurrences of an object in the conclusion of an object
+ statement</rdfs:comment>
+ <rdf:type rdf:resource="&rdfsns;Class"/>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</h:Position>
+
+<h:Position rdf:about="&hns;InBody">
+ <rdfs:comment>Occurrences of an object only in an object body (not in the
+ statement)</rdfs:comment>
+ <rdf:type rdf:resource="&rdfsns;Class"/>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</h:Position>
+
+<!-- Properties -->
+
+<rdf:Property rdf:about="&hns;statement">
+ <rdfs:comment>Statement</rdfs:comment>
+ <rdfs:domain rdf:resource="&hns;Object"/>
+ <rdfs:range rdf:resource="&hns;Statement"/>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hns;body">
+ <rdfs:comment>Body</rdfs:comment>
+ <rdfs:domain rdf:resource="&hns;Object"/>
+ <rdfs:range rdf:resource="&hns;Body"/>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hns;statementId">
+ <rdfs:comment>Statement identifier</rdfs:comment>
+ <rdfs:domain rdf:resource="&hns;Statement"/>
+ <rdfs:range rdf:resource="&hns;StatementId"/>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hns;constrId">
+ <rdfs:comment>Constructor identifier of the statement conclusion</rdfs:comment>
+ <rdfs:domain rdf:resource="&hns;StatementId"/>
+ <rdfs:range rdf:resource="&hthns;HelmID"/>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hns;listId">
+ <rdfs:comment>List of all ids in the domain</rdfs:comment>
+ <rdfs:domain rdf:resource="&hns;StatementId"/>
+ <rdfs:domain rdf:resource="&hns;BodyId"/>
+ <rdfs:range rdf:resource="&rdfns;Seq"/>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hns;bodyId">
+ <rdfs:comment>Body identifier</rdfs:comment>
+ <rdfs:domain rdf:resource="&hns;Body"/>
+ <rdfs:range rdf:resource="&hns;BodyId"/>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hns;refObj">
+ <rdfs:comment>Reference to an object</rdfs:comment>
+ <rdfs:domain rdf:resource="&hns;Object"/>
+ <rdfs:range rdf:resource="&hns;Occurrence"/>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hns;constrImplArg">
+ <rdfs:comment>Implicit arguments of constructors</rdfs:comment>
+ <rdfs:domain rdf:resource="&hns;Statement"/>
+ <rdfs:range rdf:resource="&hns;ImplArg"/>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hns;objImplArg">
+ <rdfs:comment>Implicit arguments of objects</rdfs:comment>
+ <rdfs:domain rdf:resource="&hns;Object"/>
+ <rdfs:range rdf:resource="&hns;ImplArg"/>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hns;listImplArg">
+ <rdfs:comment>List of implicit arguments</rdfs:comment>
+ <rdfs:domain rdf:resource="&hns;ImplArg"/>
+ <rdfs:range rdf:resource="&rdfns;Seq"/>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hns;backPointer">
+ <rdfs:comment>Backwards pointer: who points the object</rdfs:comment>
+ <rdfs:domain rdf:resource="&hns;Object"/>
+ <rdfs:range rdf:resource="&hns;Occurrence"/>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hns;occurrence">
+ <rdfs:comment>URI of an object</rdfs:comment>
+ <rdfs:domain rdf:resource="&hns;Occurrence"/>
+ <rdfs:range rdf:resource="&hthns;HelmURI"/>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hns;position">
+ <rdfs:comment>Position of an occurrence</rdfs:comment>
+ <rdfs:domain rdf:resource="&hns;Occurrence"/>
+ <rdfs:range rdf:resource="&hns;Position"/>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdf:Property>
+
+
+<rdf:Property rdf:about="&hns;postit">
+ <rdfs:comment>Postit</rdfs:comment>
+ <rdfs:domain rdf:resource="&hns;Object"/>
+ <rdfs:range rdf:resource="&hns;Postit"/>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hns;content">
+ <rdfs:comment>Content of a Postit</rdfs:comment>
+ <rdfs:domain rdf:resource="#Postit"/>
+ <rdfs:range rdf:resource="&xschemans;string"/>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hns;refersTo">
+ <rdfs:comment>Identifies the object fragment (Xpointer) which Postit
+refers to</rdfs:comment>
+ <rdfs:domain rdf:resource="&hns;Postit"/>
+ <rdfs:range rdf:resource="&hthns;HelmURI"/>
+ <rdfs:isDefinedBy rdf:resource = "&hns;" />
+</rdf:Property>
+
+</rdf:RDF>
\ No newline at end of file
+++ /dev/null
-<?xml version="1.0"?>
-
-<!-- Rdf Schema definition for CIC XML files:
-xmlns:h="http://www.cs.unibo.it/~schena/schema-h.rdf#" -->
-
-<!DOCTYPE rdf:RDF [
- <!ENTITY rdfns 'http://www.w3.org/1999/02/22-rdf-syntax-ns#'>
- <!ENTITY rdfsns 'http://www.w3.org/2000/01/rdf-schema#'>
- <!ENTITY hthns 'http://www.cs.unibo.it/~schena/schema-hth.rdf#'>
- <!ENTITY xschemans 'http://www.w3.org/1999/XMLSchema-datatypes#'>
- <!ENTITY hns 'http://www.cs.unibo.it/~schena/schema-h.rdf#'>
- <!ENTITY dcns 'http://www.cs.unibo.it/~schena/dces#'>
- ]>
-
-<rdf:RDF xml:lang="en"
- xmlns:rdf="&rdfns;"
- xmlns:rdfs="&rdfsns;"
- xmlns:hth="&hthns;"
- xmlns:xs="&xschemans;"
- xmlns:dc="&dcns;">
-
-<!-- RICORDA: metadati solo su oggetto (come teoria ma piu' specifici) (non
-distinzione tipi di body) e non ridondanze se non riducono il numero di doc
-da parsare -->
-
-<!-- Description of Schema -->
-
-<rdf:Description rdf:about="&hns;">
- <rdf:value>The HELM Element Set v0.1</rdf:value>
- <dc:title>The HELM Object Element Set v0.1</dc:title>
- <dc:publisher>The HELM Project</dc:publisher>
- <dc:description>The HELM metadata vocabulary is a simple vocabulary
- intended to facilitate discovery of mathematical resources.
- </dc:description>
- <dc:language>English</dc:language>
- <dc:relation rdf:resource="http://ww.cs.unibo.it/helm/"/>
- <dc:date>2001-12-12</dc:date>
-</rdf:Description>
-
-
-<!-- Classes -->
-
-<rdfs:Class rdf:ID="Object">
- <rdfs:comment>Mathematical objects represented by a CIC XML
-file</rdfs:comment>
- <rdfs:subClassOf rdf:resource="&hthns;MathResource"/>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdfs:Class>
-
-<!-- Objects can inherit its dc properties -->
-<rdfs:Class rdf:ID="DirectoryOfObjects">
- <rdfs:comment>Mathematical resources (directories) represented by sets
-of CIC XML files, contained in the tree that has the dir as root </rdfs:comment>
- <rdfs:subClassOf rdf:resource="&hthns;MathResource"/>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Statement">
- <rdfs:comment>Types of objects</rdfs:comment>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Body">
- <rdfs:comment>Terms of objects</rdfs:comment>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Occurrence">
- <rdfs:comment>Occurrences of an object inside an object</rdfs:comment>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Position">
- <rdfs:comment>Positions of occurrences of an object inside an object</rdfs:comment>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Postit">
- <rdfs:comment>Additional information associated to fragments of the objects</rdfs:comment>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Const">
- <rdfs:comment>Constants in the body of an object</rdfs:comment>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="StatementId">
- <rdfs:comment>Identifiers in the statement</rdfs:comment>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="BodyId">
- <rdfs:comment>Identifiers in the body</rdfs:comment>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="ImplArg">
- <rdfs:comment>Implicit arguments</rdfs:comment>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdfs:Class>
-
-<!-- Instances of the class h:Position -->
-
-<rdfs:Class rdf:ID="MainHypothesis">
- <rdfs:comment>Occurrences of an object in head position of some hypothesis
- of an object statement</rdfs:comment>
- <rdf:type rdf:resource="#Position"/>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="InHypothesis">
- <rdfs:comment>Occurrences of an object in the hypotheses of an object
- statement</rdfs:comment>
- <rdf:type rdf:resource="#Position"/>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="MainConclusion">
- <rdfs:comment>Occurrences of an object in head position of the
- conclusion of an object statement</rdfs:comment>
- <rdf:type rdf:resource="#Position"/>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="InConclusion">
- <rdfs:comment>Occurrences of an object in the conclusion of an object
- statement</rdfs:comment>
- <rdf:type rdf:resource="#Position"/>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="InBody">
- <rdfs:comment>Occurrences of an object only in an object body (not in the
- statement)</rdfs:comment>
- <rdf:type rdf:resource="#Position"/>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdfs:Class>
-
-<!-- Properties -->
-
-<rdf:Property rdf:ID="statement">
- <rdfs:comment>Statement</rdfs:comment>
- <rdfs:domain rdf:resource="#Object"/>
- <rdfs:range rdf:resource="#Statement"/>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="body">
- <rdfs:comment>Body</rdfs:comment>
- <rdfs:domain rdf:resource="#Object"/>
- <rdfs:range rdf:resource="#Body"/>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="statementId">
- <rdfs:comment>Statement identifier</rdfs:comment>
- <rdfs:domain rdf:resource="#Statement"/>
- <rdfs:range rdf:resource="#StatementId"/>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="constrId">
- <rdfs:comment>Constructor identifier of the statement conclusion</rdfs:comment>
- <rdfs:domain rdf:resource="#StatementId"/>
- <rdfs:range rdf:resource="&hthns;HelmID"/>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="listId">
- <rdfs:comment>List of all ids in the domain</rdfs:comment>
- <rdfs:domain rdf:resource="#StatementId"/>
- <rdfs:domain rdf:resource="#BodyId"/>
- <rdfs:range rdf:resource="&rdfns;Seq"/>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="bodyId">
- <rdfs:comment>Body identifier</rdfs:comment>
- <rdfs:domain rdf:resource="#Body"/>
- <rdfs:range rdf:resource="#BodyId"/>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="refObj">
- <rdfs:comment>Reference to an object</rdfs:comment>
- <rdfs:domain rdf:resource="#Object"/>
- <rdfs:range rdf:resource="#Occurrence"/>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="constrImplArg">
- <rdfs:comment>Implicit arguments of constructors</rdfs:comment>
- <rdfs:domain rdf:resource="#Statement"/>
- <rdfs:range rdf:resource="#ImplArg"/>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="objImplArg">
- <rdfs:comment>Implicit arguments of objects</rdfs:comment>
- <rdfs:domain rdf:resource="#Object"/>
- <rdfs:range rdf:resource="#ImplArg"/>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="listImplArg">
- <rdfs:comment>List of implicit arguments</rdfs:comment>
- <rdfs:domain rdf:resource="#ImplArg"/>
- <rdfs:range rdf:resource="&rdfns;Seq"/>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="backPointer">
- <rdfs:comment>Backwards pointer: who points the object</rdfs:comment>
- <rdfs:domain rdf:resource="#Object"/>
- <rdfs:range rdf:resource="#Occurrence"/>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="occurrence">
- <rdfs:comment>URI of an object</rdfs:comment>
- <rdfs:domain rdf:resource="#Occurrence"/>
- <rdfs:range rdf:resource="&hthns;HelmURI"/>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="position">
- <rdfs:comment>Position of an occurrence</rdfs:comment>
- <rdfs:domain rdf:resource="#Occurrence"/>
- <rdfs:range rdf:resource="#Position"/>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdf:Property>
-
-
-<rdf:Property rdf:ID="postit">
- <rdfs:comment>Postit</rdfs:comment>
- <rdfs:domain rdf:resource="#Object"/>
- <rdfs:range rdf:resource="#Postit"/>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="content">
- <rdfs:comment>Content of a Postit</rdfs:comment>
- <rdfs:domain rdf:resource="#Postit"/>
- <rdfs:range rdf:resource="&xschemans;string"/>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="refersTo">
- <rdfs:comment>Identifies the object fragment (Xpointer) which Postit
-refers to</rdfs:comment>
- <rdfs:domain rdf:resource="#Postit"/>
- <rdfs:range rdf:resource="&hthns;HelmURI"/>
- <rdfs:isDefinedBy rdf:resource = "&hns;" />
-</rdf:Property>
-
-</rdf:RDF>
\ No newline at end of file
--- /dev/null
+<?xml version="1.0"?>
+
+<!-- Rdf Schema definition for theory files:
+xmlns:hth="http://www.cs.unibo.it/~schena/schema-hth#" -->
+
+<!DOCTYPE rdf:RDF [
+ <!ENTITY rdfns 'http://www.w3.org/1999/02/22-rdf-syntax-ns#'>
+ <!ENTITY rdfsns 'http://www.w3.org/2000/01/rdf-schema#'>
+ <!ENTITY dcns 'http://www.cs.unibo.it/~schena/dces#'>
+ <!ENTITY dcqns 'http://www.cs.unibo.it/~schena/dcq#'>
+ <!ENTITY dctns 'http://www.cs.unibo.it/~schena/dctype#'>
+ <!ENTITY xschemans 'http://www.w3.org/1999/XMLSchema-datatypes#'>
+ <!ENTITY hthns 'http://www.cs.unibo.it/~schena/schema-hth#'>
+ <!ENTITY hns 'http://www.cs.unibo.it/~schena/schema-h#'>
+ ]>
+
+<rdf:RDF xml:lang="en"
+ xmlns:rdf="&rdfns;"
+ xmlns:rdfs="&rdfsns;"
+ xmlns:dc="&dcns;"
+ xmlns:dcq="&dcqns;"
+ xmlns:dct="&dctns;"
+ xmlns:xs="&xschemans;">
+
+<!-- RICORDA: specificare i contenuti dei dc elements: problemi con RSSDB -->
+<!-- RICORDA: aggiungi euler properties -->
+
+<!-- Description of Schema -->
+
+<rdf:Description rdf:about="&hthns;">
+ <rdfs:label>The HELM Element Set v0.1</rdfs:label>
+ <dc:title>The HELM Theory Element Set v0.1</dc:title>
+ <dc:publisher>The HELM Project</dc:publisher>
+ <dc:description>The HELM metadata vocabulary is a simple vocabulary
+ intended to facilitate discovery of mathematical resources.
+ </dc:description>
+ <dc:language>English</dc:language>
+ <dc:relation rdf:resource="http://ww.cs.unibo.it/helm/"/>
+ <dcq:isRequiredBy rdf:resource="&hns;"/>
+ <dcq:conformsTo rdf:resource="http://www.w3.org/RDF/"/>
+ <dcq:issued>2000-6-3</dcq:issued>
+ <dcq:modified>2002-9-6</dcq:modified>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdf:Description>
+
+
+<!-- Classes -->
+
+<rdfs:Class rdf:about="&hthns;MathResource">
+ <rdfs:comment>Mathematical resources</rdfs:comment>
+ <rdfs:subClassOf rdf:resource="&rdfsns;Resource"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdfs:Class>
+
+<rdfs:Class rdf:about="&hthns;Theory">
+ <rdfs:comment>Mathematical resources represented by theories</rdfs:comment>
+ <rdfs:subClassOf rdf:resource="&hthns;MathResource"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdfs:Class>
+
+<rdfs:Class rdf:about="&hthns;TheoryItem">
+ <rdfs:comment>Theory items represented by: axiom, fact, definition, theorem, lemma, corollary, variable, specified by a XPath expression</rdfs:comment>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdfs:Class>
+
+<rdfs:Class rdf:about="&hthns;Contact">
+ <rdfs:comment>Creator contact information</rdfs:comment>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdfs:Class>
+
+<!-- Subclass of dcq:URI, dct:Text and dct:Software -->
+
+<rdfs:Class rdf:about="&hthns;HelmURI">
+ <rdfs:comment>HELM URIs of a mathematical resource. Subclass of dcq:URI
+which is an instance of the IdentifierScheme class</rdfs:comment>
+ <rdfs:subClassOf rdf:resource="&dcqns;URI"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdfs:Class>
+
+<rdfs:Class rdf:about="&hthns;HELMText">
+ <rdfs:comment>HELM File text types of a mathematical resource (possible
+values of the Dublin Core property type). Possible values of the rdf:about
+attribute can be: Abstract, Paper, Bibliography, HomePage, LectureNotes,
+Monograph, PatentSpec, Preprints, Proceedings, Review, Separatum, Serial,
+TechReport, Thesis, Enclosure, General. General describes a document not of
+the previous types. A helm theory has no type per se. Subclass of dcq:Text
+which is an instance of the TypeScheme class</rdfs:comment>
+ <rdfs:subClassOf rdf:resource="&dctns;Text"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdfs:Class>
+
+<rdfs:Class rdf:about="&hthns;HELMSoftware">
+ <rdfs:comment>HELM File software types of a mathematical resource
+(possible values of the Dublin Core property type). Possible values of the
+rdf:about attribute can be: Exec, Source. Subclass of dcq:Software
+which is an instance of the TypeScheme class</rdfs:comment>
+ <rdfs:subClassOf rdf:resource="&dctns;Software"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdfs:Class>
+
+<!-- Instances of dcq:FormatScheme and dcq:IdentifierScheme -->
+<!-- Instances are only for typing classes not for using. -->
+
+<dcq:FormatScheme rdf:about="&hthns;HelmFormat">
+ <rdfs:comment>Instance of the class FormatScheme to describe HELM File
+formats of a mathematical resource (possible values of the Dublin Core property
+format). Possible values of the rdf:about
+attribute can be XML.cic, XML.hol, XML.mizar. Each Helm format describes
+a logical framework. The class dcq:IMT contains values as text/xml, text/xhtml,
+text/mml, text/ps, text/tex, text/pdf.</rdfs:comment>
+ <rdf:type rdf:resource="&rdfsns;Class"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</dcq:FormatScheme>
+
+<dcq:IdentifierScheme rdf:about="&hthns;HelmID">
+ <rdfs:comment>Instance of the class IdentifierScheme to describe HELM
+identifiers</rdfs:comment>
+ <rdf:type rdf:resource="&rdfsns;Class"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</dcq:IdentifierScheme>
+
+<!-- SubProperties of dc:description, dc:creator, dc:relation and
+ hth:dependence -->
+
+<!-- There are also dcq:created and dcq:modified dc:date subProperties -->
+<rdf:Property rdf:ID="firstVersion">
+ <rdfs:comment>Any additional information about the first version of the
+mathematical resource</rdfs:comment>
+ <rdfs:subPropertyOf rdf:resource="&dcns;description"/>
+ <rdfs:domain rdf:resource="#MathResource"/>
+ <rdfs:range rdf:resource="&xschemans;string"/>
+</rdf:Property>
+
+<rdf:Property rdf:ID="modified">
+ <rdfs:comment>Any additional information about the modified version of the
+mathematical resource</rdfs:comment>
+ <rdfs:subPropertyOf rdf:resource="&dcns;description"/>
+ <rdfs:domain rdf:resource="#MathResource"/>
+ <rdfs:range rdf:resource="&xschemans;string"/>
+</rdf:Property>
+
+<rdf:Property rdf:about="&hthns;institution">
+ <rdfs:comment>Affiliated institution of the creator of the mathematical
+resource</rdfs:comment>
+ <rdfs:subPropertyOf rdf:resource="&dcns;creator"/>
+ <rdfs:domain rdf:resource="&hthns;MathResource"/>
+ <rdfs:range rdf:resource="&xschemans;string"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hthns;contact">
+ <rdfs:comment>Contact of the creator of the mathematical
+resource</rdfs:comment>
+ <rdfs:subPropertyOf rdf:resource="&dcns;creator"/>
+ <rdfs:domain rdf:resource="&hthns;MathResource"/>
+ <rdfs:range rdf:resource="#Contact"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hthns;isBasedOn">
+ <rdfs:comment>A relation between mathematical resources</rdfs:comment>
+ <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
+ <rdfs:domain rdf:resource="&hthns;MathResource"/>
+ <rdfs:range rdf:resource="&hthns;HelmURI"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hthns;isBasisFor">
+ <rdfs:comment>A relation between mathematical resources</rdfs:comment>
+ <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
+ <rdfs:domain rdf:resource="&hthns;MathResource"/>
+ <rdfs:range rdf:resource="&hthns;HelmURI"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hthns;isSourceFor">
+ <rdfs:comment>A relation between mathematical resources</rdfs:comment>
+ <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
+ <rdfs:domain rdf:resource="&hthns;MathResource"/>
+ <rdfs:range rdf:resource="&hthns;HelmURI"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hthns;hasSource">
+ <rdfs:comment>A relation between mathematical resources</rdfs:comment>
+ <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
+ <rdfs:domain rdf:resource="&hthns;MathResource"/>
+ <rdfs:range rdf:resource="&hthns;HelmURI"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hthns;uses">
+ <rdfs:comment>A dependence between theory items (for instance: between a theorem or anything else and a variable)</rdfs:comment>
+ <rdfs:subPropertyOf rdf:resource="&hthns;dependence"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hthns;isUsedBy">
+ <rdfs:comment>A dependence between theory items (for instance: between a variable and
+a theorem or anything else)</rdfs:comment>
+ <rdfs:subPropertyOf rdf:resource="&hthns;dependence"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hthns;hasConsequence">
+ <rdfs:comment>A dependence between theory items (for instance: between a theorem and
+a corollary)</rdfs:comment>
+ <rdfs:subPropertyOf rdf:resource="&hthns;dependence"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hthns;isConsequenceOf">
+ <rdfs:comment>A dependence between theory items (for instance: between a corollary
+and a theorem). Alternatively: IsResultOf</rdfs:comment>
+ <rdfs:subPropertyOf rdf:resource="&hthns;dependence"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hthns;hasPremise">
+ <rdfs:comment>A dependence between theory items (for instance: between a theorem
+and a lemma)</rdfs:comment>
+ <rdfs:subPropertyOf rdf:resource="&hthns;dependence"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hthns;isPremiseOf">
+ <rdfs:comment>A dependence between theory items (for instance: between a lemma
+and a theorem)</rdfs:comment>
+ <rdfs:subPropertyOf rdf:resource="&hthns;dependence"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdf:Property>
+
+<!-- Properties -->
+
+<rdf:Property rdf:about="&hthns;theoryItem">
+ <rdfs:comment>Theory item</rdfs:comment>
+ <rdfs:domain rdf:resource="&hthns;Theory"/>
+ <rdfs:range rdf:resource="&hthns;TheoryItem"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hthns;dependence">
+ <rdfs:comment>Dependence between theory items</rdfs:comment>
+ <rdfs:domain rdf:resource="&hthns;TheoryItem"/>
+ <rdfs:range rdf:resource="&hthns;HelmID"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hthns;itemType">
+ <rdfs:comment>Axiom, Fact, Definition, Theorem, Lemma, Corollary,
+Variable. Redundant info: it is already captured by the corresponding xml data</rdfs:comment>
+ <rdfs:domain rdf:resource="&hthns;TheoryItem"/>
+ <rdfs:range rdf:resource="&xschemans;string"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hthns;label">
+ <rdfs:comment>Description of the kind of objects: data type,
+algorithm, specification, theorem containing algorithm, verification (that the
+implementation satisfies the specification), predicate/relation, proposition</rdfs:comment>
+ <rdfs:domain rdf:resource="&hthns;TheoryItem"/>
+ <rdfs:range rdf:resource="&xschemans;string"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdf:Property>
+
+<!-- ex. f:N->Z => N>->Z and n:Nat => n:Z -->
+<rdf:Property rdf:about="&hthns;isCoercion">
+ <rdfs:comment>A Definition item can be a coercion</rdfs:comment>
+ <rdfs:domain rdf:resource="&hthns;TheoryItem"/>
+ <rdfs:range rdf:resource="&xschemans;boolean"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdf:Property>
+
+<!-- The id info is no more contained in the theory xml doc, so there isn't
+redundant info between metadata and data -->
+<rdf:Property rdf:about="&hthns;ident">
+ <rdfs:comment>Identifier of a theory item</rdfs:comment>
+ <rdfs:domain rdf:resource="&hthns;TheoryItem"/>
+ <rdfs:range rdf:resource="&hthns;HelmID"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hthns;email">
+ <rdfs:comment>E-mail of the creator of the mathematical
+resource</rdfs:comment>
+ <rdfs:domain rdf:resource="&hthns;Contact"/>
+ <rdfs:range rdf:resource="&xschemans;string"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdf:Property>
+
+<rdf:Property rdf:about="&hthns;address">
+ <rdfs:comment>Address of the creator of the mathematical
+resource</rdfs:comment>
+ <rdfs:domain rdf:resource="&hthns;Contact"/>
+ <rdfs:range rdf:resource="&xschemans;string"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
+</rdf:Property>
+
+<!-- HELM: Constraining an external (dc) property to a particular range and
+domain (hth:MathResource) should be possible. VRP gives a Warning when
+constraining (extending, adding constraints to) the range of a property
+defined in another schema (Consistency problems?No because it's an error
+modifying the original constraints): but where is the extensibility and
+reusability of RDF schemas? It's ok specializing a property with a
+subProperty. Anyway if the range of a property is not defined, VRP validates
+both if the property value is a resource, a class or a Literal.
+<rdf:Description rdf:about = "&dcns;type">
+ <rdfs:domain rdf:resource="&hthns;MathResource"/>
+</rdf:Description> -->
+
+</rdf:RDF>
+++ /dev/null
-<?xml version="1.0"?>
-
-<!-- Rdf Schema definition for theory files:
-xmlns:hth="http://www.cs.unibo.it/~schena/schema-hth.rdf#" -->
-
-<!DOCTYPE rdf:RDF [
- <!ENTITY rdfns 'http://www.w3.org/1999/02/22-rdf-syntax-ns#'>
- <!ENTITY rdfsns 'http://www.w3.org/2000/01/rdf-schema#'>
- <!ENTITY dcns 'http://www.cs.unibo.it/~schena/dces#'>
- <!ENTITY dcqns 'http://www.cs.unibo.it/~schena/dcq#'>
- <!ENTITY xschemans 'http://www.w3.org/1999/XMLSchema-datatypes#'>
- <!ENTITY hthns 'http://www.cs.unibo.it/~schena/schema-hth.rdf#'>
- ]>
-
-<rdf:RDF xml:lang="en"
- xmlns:rdf="&rdfns;"
- xmlns:rdfs="&rdfsns;"
- xmlns:dc="&dcns;"
- xmlns:dcq="&dcqns;"
- xmlns:xs="&xschemans;">
-
-<!-- RICORDA: specificare i contenuti dei dc elements: problemi con RSSDB -->
-<!-- RICORDA: aggiungi euler properties -->
-
-<!-- Description of Schema -->
-
-<rdf:Description rdf:about="&hthns;">
- <rdf:value>The HELM Element Set v0.1</rdf:value>
- <dc:title>The HELM Theory Element Set v0.1</dc:title>
- <dc:publisher>The HELM Project</dc:publisher>
- <dc:description>The HELM metadata vocabulary is a simple vocabulary
- intended to facilitate discovery of mathematical resources.
- </dc:description>
- <dc:language>English</dc:language>
- <dc:relation rdf:resource="http://ww.cs.unibo.it/helm/"/>
- <dc:date>2001-12-12</dc:date>
-</rdf:Description>
-
-
-<!-- Classes -->
-
-<rdfs:Class rdf:ID="MathResource">
- <rdfs:comment>Mathematical resources</rdfs:comment>
- <rdfs:subClassOf rdf:resource="&rdfsns;Resource"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Theory">
- <rdfs:comment>Mathematical resources represented by theories</rdfs:comment>
- <rdfs:subClassOf rdf:resource="#MathResource"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="TheoryItem">
- <rdfs:comment>Theory items represented by: axiom, fact, definition, theorem, lemma, corollary, variable, specified by a XPath expression</rdfs:comment>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="HelmFormat">
- <rdfs:comment>HELM File formats of a mathematical resource (possible values of the Dublin Core property Format). Possible values of the rdf:about
-attribute can be XML.cic, XML.hol, XML.mizar. Each Helm format describes
-a logical framework. The class dcq:IMT contains values as text/xml, text/xhtml,
-text/mml, text/ps, text/tex, text/pdf.</rdfs:comment>
- <rdfs:subClassOf rdf:resource="&dcqns;FormatScheme"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="HelmURI">
- <rdfs:comment>HELM URIs of a mathematical resource</rdfs:comment>
- <rdfs:subClassOf rdf:resource="&dcqns;URI"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="HelmID">
- <rdfs:comment>HELM identifiers</rdfs:comment>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Contact">
- <rdfs:comment>Creator contact information</rdfs:comment>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdfs:Class>
-
-<!-- Added subProperties of the Property dc:relation -->
-
-<rdf:Property rdf:ID="isBasedOn">
- <rdfs:comment>A relation between mathematical resources</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
- <rdfs:domain rdf:resource="#MathResource"/>
- <rdfs:range rdf:resource="#HelmURI"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="isBasisFor">
- <rdfs:comment>A relation between mathematical resources</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
- <rdfs:domain rdf:resource="#MathResource"/>
- <rdfs:range rdf:resource="#HelmURI"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="isSourceFor">
- <rdfs:comment>A relation between mathematical resources</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
- <rdfs:domain rdf:resource="#MathResource"/>
- <rdfs:range rdf:resource="#HelmURI"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="hasSource">
- <rdfs:comment>A relation between mathematical resources</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
- <rdfs:domain rdf:resource="#MathResource"/>
- <rdfs:range rdf:resource="#HelmURI"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<!-- subProperties of Property hth:dependence -->
-
-<rdf:Property rdf:ID="uses">
- <rdfs:comment>A dependence between theory items (for instance: between a theorem or anything else and a variable)</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="#dependence"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="isUsedBy">
- <rdfs:comment>A dependence between theory items (for instance: between a variable and
-a theorem or anything else)</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="#dependence"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="hasConsequence">
- <rdfs:comment>A dependence between theory items (for instance: between a theorem and
-a corollary)</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="#dependence"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="isConsequenceOf">
- <rdfs:comment>A dependence between theory items (for instance: between a corollary
-and a theorem). Alternatively: IsResultOf</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="#dependence"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="hasPremise">
- <rdfs:comment>A dependence between theory items (for instance: between a theorem
-and a lemma)</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="#dependence"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="isPremiseOf">
- <rdfs:comment>A dependence between theory items (for instance: between a lemma
-and a theorem)</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="#dependence"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<!-- Possible values of rdf:value of the dct:Text instance of dct:DCMIType,
-can be: Abstract, Paper, Bibliography, HomePage, LectureNotes, Monograph,
-PatentSpec, Preprints, Proceedings, Review, Separatum, Serial, TechReport,
-Thesis, Enclosure, General. -->
-<!-- There are dct:Image and dct:Software. Possible values of rdf:value
-of the dct:Software can be: Exec, Source. -->
-<!-- Text.general describes a document not of the following types. -->
-<!-- A helm theory has no type per se -->
-
-<!-- Properties -->
-
-<rdf:Property rdf:ID="theoryItem">
- <rdfs:comment>Theory item</rdfs:comment>
- <rdfs:domain rdf:resource="#Theory"/>
- <rdfs:range rdf:resource="#TheoryItem"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="dependence">
- <rdfs:comment>Dependence between theory items</rdfs:comment>
- <rdfs:domain rdf:resource="#TheoryItem"/>
- <rdfs:range rdf:resource="#HelmID"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="itemType">
- <rdfs:comment>Axiom, Fact, Definition, Theorem, Lemma, Corollary,
-Variable. Redundant info: it is already captured by the corresponding xml data</rdfs:comment>
- <rdfs:domain rdf:resource="#TheoryItem"/>
- <rdfs:range rdf:resource="&xschemans;string"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="label">
- <rdfs:comment>Description of the kind of objects: data type,
-algorithm, specification, theorem containing algorithm, verification (that the
-implementation satisfies the specification), predicate/relation, proposition</rdfs:comment>
- <rdfs:domain rdf:resource="#TheoryItem"/>
- <rdfs:range rdf:resource="&xschemans;string"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<!-- ex. f:N->Z => N>->Z and n:Nat => n:Z -->
-<rdf:Property rdf:ID="isCoercion">
- <rdfs:comment>A Definition item can be a coercion</rdfs:comment>
- <rdfs:domain rdf:resource="#TheoryItem"/>
- <rdfs:range rdf:resource="&xschemans;boolean"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<!-- The id info is no more contained in the theory xml doc, so there isn't
-redundant info between metadata and data -->
-<rdf:Property rdf:ID="ident">
- <rdfs:comment>Identifier of a theory item</rdfs:comment>
- <rdfs:domain rdf:resource="#TheoryItem"/>
- <rdfs:range rdf:resource="#HelmID"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<!-- There are also dcq:created and dcq:modified dc:date subProperties -->
-<rdf:Property rdf:ID="firstVersion">
- <rdfs:comment>Any additional information about the first version of the
-mathematical resource</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="&dcns;description"/>
- <rdfs:domain rdf:resource="#MathResource"/>
- <rdfs:range rdf:resource="&xschemans;string"/>
-</rdf:Property>
-
-<rdf:Property rdf:ID="modified">
- <rdfs:comment>Any additional information about the modified version of the
-mathematical resource</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="&dcns;description"/>
- <rdfs:domain rdf:resource="#MathResource"/>
- <rdfs:range rdf:resource="&xschemans;string"/>
-</rdf:Property>
-
-<rdf:Property rdf:ID="institution">
- <rdfs:comment>Affiliated institution of the creator of the mathematical
-resource</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="&dcns;creator"/>
- <rdfs:domain rdf:resource="#MathResource"/>
- <rdfs:range rdf:resource="&xschemans;string"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="contact">
- <rdfs:comment>Contact of the creator of the mathematical
-resource</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="&dcns;creator"/>
- <rdfs:domain rdf:resource="#MathResource"/>
- <rdfs:range rdf:resource="#Contact"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="email">
- <rdfs:comment>E-mail of the creator of the mathematical
-resource</rdfs:comment>
- <rdfs:domain rdf:resource="#Contact"/>
- <rdfs:range rdf:resource="&xschemans;string"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:ID="address">
- <rdfs:comment>Address of the creator of the mathematical
-resource</rdfs:comment>
- <rdfs:domain rdf:resource="#Contact"/>
- <rdfs:range rdf:resource="&xschemans;string"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<!-- HELM: Here we want to constraint an external (dc) property to a
-particular range and domain (hth:MathResource). VRP gives a Warning when
-(extending or modifying) constraining the range of a property defined
-in another schema; the correct way is to specialize it with a subProperty. -->
-<!-- <rdf:Description rdf:about = "&dcns;type">
- <rdfs:domain rdf:resource="#MathResource"/>
-</rdf:Description> -->
-
-
-</rdf:RDF>