X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fschemas%2Fschema-hth.rdf;h=6c54ff9163691df2fe017470b51f8e3d07fde4cd;hb=09aa799947c84148221af82e94e911adea8fd1e6;hp=110bf62fd5ab4f8a8403e087cbdfc31c0176f379;hpb=b585030cb67e164ec9a043abcd938be756d9ad1f;p=helm.git

diff --git a/helm/schemas/schema-hth.rdf b/helm/schemas/schema-hth.rdf
index 110bf62fd..6c54ff916 100644
--- a/helm/schemas/schema-hth.rdf
+++ b/helm/schemas/schema-hth.rdf
@@ -9,6 +9,7 @@ xmlns:hth="http://www.cs.unibo.it/~schena/schema-hth.rdf#" -->
         <!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"
@@ -18,113 +19,143 @@ xmlns:hth="http://www.cs.unibo.it/~schena/schema-hth.rdf#" -->
        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="#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="&rdfsns;Literal"/>
-    <rdfs:comment>A relation between mathematical resources</rdfs:comment>
+    <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="&rdfsns;Literal"/>
-    <rdfs:comment>A relation between mathematical resources</rdfs:comment>
+    <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="&rdfsns;Literal"/>
-    <rdfs:comment>A relation between mathematical resources</rdfs:comment>
+    <rdfs:range rdf:resource="#HelmURI"/>
+    <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,
@@ -139,13 +170,17 @@ of the dct:Software can be: Exec, Source.                                 -->
 <!-- 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:range rdf:resource="#HelmID"/>
+    <rdfs:isDefinedBy rdf:resource = "&hthns;" /> 
 </rdf:Property>
 
 <rdf:Property rdf:ID="itemType">
@@ -153,6 +188,7 @@ of the dct:Software can be: Exec, Source.                                 -->
 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">
@@ -161,6 +197,7 @@ 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 -->
@@ -168,36 +205,67 @@ implementation satisfies the specification), predicate/relation, proposition</rd
     <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>
 
-<!-- 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 
@@ -210,11 +278,3 @@ in another schema; the correct way is to specialize it with a subProperty. -->
 
 
 </rdf:RDF>
-
-
-
-
-
-
-
-