helm/schemas/schema-hth

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