<!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:dcq="&dcqns;"
xmlns:xs="&xschemans;">
-<!-- RICORDA: aggiungi commento anche a proprieta' e istanze -->
-<!-- RICORDA: studiare tipi di dato (invece di Literal) -->
-<!-- RICORDA: specificare i contenuti dei dc elements -->
-<!-- RICORDA: verifica formato xml.helm.cic -->
+<!-- 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 resource</rdfs:comment>
+ <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 resource represented by a theory</rdfs:comment>
+ <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 item represented by: axiom, fact, definition, theorem, lemma, corollary, variable, specified by a XPath expression </rdfs:comment>
+ <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 format of a mathematical resource (possible values of the Dublin Core property Format). Possible values of its rdf:about
+ <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 URI of a mathematical resource</rdfs:comment>
+ <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 identifier</rdfs:comment>
+ <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="&rdfsns;Literal"/>
- <rdfs:comment>A relation between mathematical resources</rdfs:comment>
+ <rdfs:range rdf:resource="&rdfsns;Literal"/>
+ <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="&rdfsns;Literal"/>
- <rdfs:comment>A relation between mathematical resources</rdfs:comment>
+ <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="&rdfsns;Literal"/>
- <rdfs:comment>A relation between mathematical resources</rdfs:comment>
+ <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="&rdfsns;Literal"/>
- <rdfs:comment>A relation between mathematical resources</rdfs:comment>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
</rdf:Property>
<!-- subProperties of Property hth:dependence -->
-<rdf:Property rdf:ID="uses">
- <rdfs:subPropertyOf rdf:resource="#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:subPropertyOf rdf:resource="#dependence"/>
<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:subPropertyOf rdf:resource="#dependence"/>
<rdfs:comment>A dependence between theory items (for instance: between a theorem and
-a corollary)</rdfs:comment>
+a corollary)</rdfs:comment>
+ <rdfs:subPropertyOf rdf:resource="#dependence"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
</rdf:Property>
<rdf:Property rdf:ID="isConsequenceOf">
- <rdfs:subPropertyOf rdf:resource="#dependence"/>
<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:subPropertyOf rdf:resource="#dependence"/>
<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:subPropertyOf rdf:resource="#dependence"/>
<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,
<!-- 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="#HelmURI"/>
+ <rdfs:isDefinedBy rdf:resource = "&hthns;" />
</rdf:Property>
<rdf:Property rdf:ID="itemType">
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">
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 -->
<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 -->
<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
</rdf:RDF>
-
-
-
-
-
-
-
-
projects / helm.git / blobdiff