helm/schemas/schema-hth.rdf

   1 <?xml version="1.0"?>
   2
   3 <!-- Rdf Schema definition for theory files:
   4 xmlns:hth="http://www.cs.unibo.it/~schena/schema-hth.rdf#" -->
   5
   6 <!DOCTYPE rdf:RDF [
   7         <!ENTITY rdfns 'http://www.w3.org/1999/02/22-rdf-syntax-ns#'>
   8         <!ENTITY rdfsns 'http://www.w3.org/2000/01/rdf-schema#'>
   9         <!ENTITY dcns 'http://www.cs.unibo.it/~schena/dces#'>
  10         <!ENTITY dcqns 'http://www.cs.unibo.it/~schena/dcq#'>
  11         <!ENTITY xschemans 'http://www.w3.org/1999/XMLSchema-datatypes#'>
  12         <!ENTITY hthns 'http://www.cs.unibo.it/~schena/schema-hth.rdf#'>
  13    ]>
  14
  15 <rdf:RDF xml:lang="en"
  16        xmlns:rdf="&rdfns;"
  17        xmlns:rdfs="&rdfsns;"
  18        xmlns:dc="&dcns;"
  19        xmlns:dcq="&dcqns;"
  20        xmlns:xs="&xschemans;">
  21
  22 <!-- RICORDA: specificare i contenuti dei dc elements: problemi con RSSDB -->
  23 <!-- RICORDA: aggiungi euler properties -->
  24
  25 <!-- Description of Schema -->
  26
  27 <rdf:Description rdf:about="&hthns;">
  28   <rdf:value>The HELM Element Set v0.1</rdf:value>
  29   <dc:title>The HELM Theory Element Set v0.1</dc:title>
  30   <dc:publisher>The HELM Project</dc:publisher>
  31   <dc:description>The HELM metadata vocabulary is a simple vocabulary
  32       intended to facilitate discovery of mathematical resources.
  33   </dc:description>
  34   <dc:language>English</dc:language>
  35   <dc:relation rdf:resource="http://ww.cs.unibo.it/helm/"/>
  36   <dc:date>2001-12-12</dc:date>
  37 </rdf:Description>
  38
  39
  40 <!-- Classes -->
  41
  42 <rdfs:Class rdf:ID="MathResource">
  43      <rdfs:comment>Mathematical resources</rdfs:comment>
  44      <rdfs:subClassOf rdf:resource="&rdfsns;Resource"/>
  45      <rdfs:isDefinedBy rdf:resource = "&hthns;" />
  46 </rdfs:Class>
  47
  48 <rdfs:Class rdf:ID="Theory">
  49      <rdfs:comment>Mathematical resources represented by theories</rdfs:comment>
  50      <rdfs:subClassOf rdf:resource="#MathResource"/>
  51      <rdfs:isDefinedBy rdf:resource = "&hthns;" />
  52 </rdfs:Class>
  53
  54 <rdfs:Class rdf:ID="TheoryItem">
  55      <rdfs:comment>Theory items represented by: axiom, fact, definition, theorem, lemma, corollary, variable, specified by a XPath expression</rdfs:comment>
  56      <rdfs:isDefinedBy rdf:resource = "&hthns;" />
  57 </rdfs:Class>
  58
  59 <rdfs:Class rdf:ID="HelmFormat">
  60      <rdfs:comment>HELM File formats of a mathematical resource (possible values of the Dublin Core property Format). Possible values of the rdf:about
  61 attribute can be XML.cic, XML.hol, XML.mizar. Each Helm format describes
  62 a logical framework. The class dcq:IMT contains values as text/xml, text/xhtml,
  63 text/mml, text/ps, text/tex, text/pdf.</rdfs:comment>
  64      <rdfs:subClassOf rdf:resource="&dcqns;FormatScheme"/>
  65      <rdfs:isDefinedBy rdf:resource = "&hthns;" />
  66 </rdfs:Class>
  67
  68 <rdfs:Class rdf:ID="HelmURI">
  69      <rdfs:comment>HELM URIs of a mathematical resource</rdfs:comment>
  70      <rdfs:subClassOf rdf:resource="&dcqns;URI"/>
  71      <rdfs:isDefinedBy rdf:resource = "&hthns;" />
  72 </rdfs:Class>
  73
  74 <rdfs:Class rdf:ID="HelmID">
  75      <rdfs:comment>HELM identifiers</rdfs:comment>
  76      <rdfs:isDefinedBy rdf:resource = "&hthns;" />
  77 </rdfs:Class>
  78
  79 <rdfs:Class rdf:ID="Contact">
  80      <rdfs:comment>Creator contact information</rdfs:comment>
  81      <rdfs:isDefinedBy rdf:resource = "&hthns;" />
  82 </rdfs:Class>
  83
  84 <!-- Added subProperties of the Property dc:relation -->
  85
  86 <rdf:Property rdf:ID="isBasedOn">
  87     <rdfs:comment>A relation between mathematical resources</rdfs:comment>
  88     <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
  89     <rdfs:domain rdf:resource="#MathResource"/>
  90     <rdfs:range rdf:resource="#HelmURI"/>
  91     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
  92 </rdf:Property>
  93
  94 <rdf:Property rdf:ID="isBasisFor">
  95     <rdfs:comment>A relation between mathematical resources</rdfs:comment>
  96     <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
  97     <rdfs:domain rdf:resource="#MathResource"/>
  98     <rdfs:range rdf:resource="#HelmURI"/>
  99     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 100 </rdf:Property>
 101
 102 <rdf:Property rdf:ID="isSourceFor">
 103     <rdfs:comment>A relation between mathematical resources</rdfs:comment>
 104     <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
 105     <rdfs:domain rdf:resource="#MathResource"/>
 106     <rdfs:range rdf:resource="#HelmURI"/>
 107     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 108 </rdf:Property>
 109
 110 <rdf:Property rdf:ID="hasSource">
 111     <rdfs:comment>A relation between mathematical resources</rdfs:comment>
 112     <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
 113     <rdfs:domain rdf:resource="#MathResource"/>
 114     <rdfs:range rdf:resource="#HelmURI"/>
 115     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 116 </rdf:Property>
 117
 118 <!--  subProperties of Property hth:dependence -->
 119
 120 <rdf:Property rdf:ID="uses">
 121     <rdfs:comment>A dependence between theory items (for instance: between a theorem or anything else and a variable)</rdfs:comment>
 122     <rdfs:subPropertyOf rdf:resource="#dependence"/>
 123     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 124 </rdf:Property>
 125
 126 <rdf:Property rdf:ID="isUsedBy">
 127     <rdfs:comment>A dependence between theory items (for instance: between a variable and
 128 a theorem or anything else)</rdfs:comment>
 129     <rdfs:subPropertyOf rdf:resource="#dependence"/>
 130     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 131 </rdf:Property>
 132
 133 <rdf:Property rdf:ID="hasConsequence">
 134     <rdfs:comment>A dependence between theory items (for instance: between a theorem and
 135 a corollary)</rdfs:comment>
 136     <rdfs:subPropertyOf rdf:resource="#dependence"/>
 137     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 138 </rdf:Property>
 139
 140 <rdf:Property rdf:ID="isConsequenceOf">
 141     <rdfs:comment>A dependence between theory items (for instance: between a corollary
 142 and a theorem). Alternatively: IsResultOf</rdfs:comment>
 143     <rdfs:subPropertyOf rdf:resource="#dependence"/>
 144     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 145 </rdf:Property>
 146
 147 <rdf:Property rdf:ID="hasPremise">
 148     <rdfs:comment>A dependence between theory items (for instance: between a theorem
 149 and a lemma)</rdfs:comment>
 150     <rdfs:subPropertyOf rdf:resource="#dependence"/>
 151     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 152 </rdf:Property>
 153
 154 <rdf:Property rdf:ID="isPremiseOf">
 155     <rdfs:comment>A dependence between theory items (for instance: between a lemma
 156 and a theorem)</rdfs:comment>
 157     <rdfs:subPropertyOf rdf:resource="#dependence"/>
 158     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 159 </rdf:Property>
 160
 161 <!-- Possible values of rdf:value of the dct:Text instance of dct:DCMIType,
 162 can be: Abstract, Paper, Bibliography, HomePage, LectureNotes, Monograph,
 163 PatentSpec, Preprints, Proceedings, Review, Separatum, Serial, TechReport,
 164 Thesis, Enclosure, General.                                               -->
 165 <!-- There are dct:Image and dct:Software. Possible values of rdf:value
 166 of the dct:Software can be: Exec, Source.                                 -->
 167 <!-- Text.general describes a document not of the following types.        -->
 168 <!-- A helm theory has no type per se                                     -->
 169
 170 <!-- Properties -->
 171
 172 <rdf:Property rdf:ID="theoryItem">
 173     <rdfs:comment>Theory item</rdfs:comment>
 174     <rdfs:domain rdf:resource="#Theory"/>
 175     <rdfs:range rdf:resource="#TheoryItem"/>
 176     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 177 </rdf:Property>
 178
 179 <rdf:Property rdf:ID="dependence">
 180     <rdfs:comment>Dependence between theory items</rdfs:comment>
 181     <rdfs:domain rdf:resource="#TheoryItem"/>
 182     <rdfs:range rdf:resource="#HelmID"/>
 183     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 184 </rdf:Property>
 185
 186 <rdf:Property rdf:ID="itemType">
 187     <rdfs:comment>Axiom, Fact, Definition, Theorem, Lemma, Corollary,
 188 Variable. Redundant info: it is already captured by the corresponding xml data</rdfs:comment>
 189     <rdfs:domain rdf:resource="#TheoryItem"/>
 190     <rdfs:range rdf:resource="&xschemans;string"/>
 191     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 192 </rdf:Property>
 193
 194 <rdf:Property rdf:ID="label">
 195     <rdfs:comment>Description of the kind of objects: data type,
 196 algorithm, specification, theorem containing algorithm, verification (that the
 197 implementation satisfies the specification), predicate/relation, proposition</rdfs:comment>
 198     <rdfs:domain rdf:resource="#TheoryItem"/>
 199     <rdfs:range rdf:resource="&xschemans;string"/>
 200     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 201 </rdf:Property>
 202
 203 <!-- ex. f:N->Z => N>->Z and n:Nat => n:Z -->
 204 <rdf:Property rdf:ID="isCoercion">
 205     <rdfs:comment>A Definition item can be a coercion</rdfs:comment>
 206     <rdfs:domain rdf:resource="#TheoryItem"/>
 207     <rdfs:range rdf:resource="&xschemans;boolean"/>
 208     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 209 </rdf:Property>
 210
 211 <!-- The id info is no more contained in the theory xml doc, so there isn't
 212 redundant info between metadata and data -->
 213 <rdf:Property rdf:ID="ident">
 214     <rdfs:comment>Identifier of a theory item</rdfs:comment>
 215     <rdfs:domain rdf:resource="#TheoryItem"/>
 216     <rdfs:range rdf:resource="#HelmID"/>
 217     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 218 </rdf:Property>
 219
 220 <!-- There are also dcq:created and dcq:modified dc:date subProperties -->
 221 <rdf:Property rdf:ID="firstVersion">
 222     <rdfs:comment>Any additional information about the first version of the
 223 mathematical resource</rdfs:comment>
 224     <rdfs:subPropertyOf rdf:resource="&dcns;description"/>
 225     <rdfs:domain rdf:resource="#MathResource"/>
 226     <rdfs:range rdf:resource="&xschemans;string"/>
 227 </rdf:Property>
 228
 229 <rdf:Property rdf:ID="modified">
 230     <rdfs:comment>Any additional information about the modified version of the
 231 mathematical resource</rdfs:comment>
 232     <rdfs:subPropertyOf rdf:resource="&dcns;description"/>
 233     <rdfs:domain rdf:resource="#MathResource"/>
 234     <rdfs:range rdf:resource="&xschemans;string"/>
 235 </rdf:Property>
 236
 237 <rdf:Property rdf:ID="institution">
 238     <rdfs:comment>Affiliated institution of the creator of the mathematical
 239 resource</rdfs:comment>
 240     <rdfs:subPropertyOf rdf:resource="&dcns;creator"/>
 241     <rdfs:domain rdf:resource="#MathResource"/>
 242     <rdfs:range rdf:resource="&xschemans;string"/>
 243     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 244 </rdf:Property>
 245
 246 <rdf:Property rdf:ID="contact">
 247     <rdfs:comment>Contact of the creator of the mathematical
 248 resource</rdfs:comment>
 249     <rdfs:subPropertyOf rdf:resource="&dcns;creator"/>
 250     <rdfs:domain rdf:resource="#MathResource"/>
 251     <rdfs:range rdf:resource="#Contact"/>
 252     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 253 </rdf:Property>
 254
 255 <rdf:Property rdf:ID="email">
 256     <rdfs:comment>E-mail of the creator of the mathematical
 257 resource</rdfs:comment>
 258     <rdfs:domain rdf:resource="#Contact"/>
 259     <rdfs:range rdf:resource="&xschemans;string"/>
 260     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 261 </rdf:Property>
 262
 263 <rdf:Property rdf:ID="address">
 264     <rdfs:comment>Address of the creator of the mathematical
 265 resource</rdfs:comment>
 266     <rdfs:domain rdf:resource="#Contact"/>
 267     <rdfs:range rdf:resource="&xschemans;string"/>
 268     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 269 </rdf:Property>
 270
 271 <!-- HELM: Here we want to constraint an external (dc) property to a
 272 particular range and domain (hth:MathResource). VRP gives a Warning when
 273 (extending or modifying) constraining the range of a property defined
 274 in another schema; the correct way is to specialize it with a subProperty. -->
 275 <!-- <rdf:Description rdf:about = "&dcns;type">
 276     <rdfs:domain rdf:resource="#MathResource"/>
 277 </rdf:Description> -->
 278
 279
 280 </rdf:RDF>