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 dcq:URI, dct:Text and dct:Software -->
  72
  73 <rdfs:Class rdf:about="&hthns;HelmURI">
  74      <rdfs:comment>HELM URIs of a mathematical resource. Subclass of dcq:URI
  75 which is an instance of the IdentifierScheme class</rdfs:comment>
  76      <rdfs:subClassOf rdf:resource="&dcqns;URI"/>
  77      <rdfs:isDefinedBy rdf:resource = "&hthns;" />
  78 </rdfs:Class>
  79
  80 <rdfs:Class rdf:about="&hthns;HELMText">
  81      <rdfs:comment>HELM File text types of a mathematical resource (possible
  82 values of the Dublin Core property type). Possible values of the rdf:about
  83 attribute can be: Abstract, Paper, Bibliography, HomePage, LectureNotes,
  84 Monograph, PatentSpec, Preprints, Proceedings, Review, Separatum, Serial,
  85 TechReport, Thesis, Enclosure, General. General describes a document not of
  86 the previous types. A helm theory has no type per se. Subclass of dcq:Text
  87 which is an instance of the TypeScheme class</rdfs:comment>
  88      <rdfs:subClassOf rdf:resource="&dctns;Text"/>
  89      <rdfs:isDefinedBy rdf:resource = "&hthns;" />
  90 </rdfs:Class>
  91
  92 <rdfs:Class rdf:about="&hthns;HELMSoftware">
  93      <rdfs:comment>HELM File software types of a mathematical resource
  94 (possible values of the Dublin Core property type). Possible values of the
  95 rdf:about attribute can be: Exec, Source. Subclass of dcq:Software
  96 which is an instance of the TypeScheme class</rdfs:comment>
  97      <rdfs:subClassOf rdf:resource="&dctns;Software"/>
  98      <rdfs:isDefinedBy rdf:resource = "&hthns;" />
  99 </rdfs:Class>
 100
 101 <!-- Instances of dcq:FormatScheme and dcq:IdentifierScheme -->
 102 <!-- Instances are only for typing classes not for using.   -->
 103
 104 <dcq:FormatScheme rdf:about="&hthns;HelmFormat">
 105      <rdfs:comment>Instance of the class FormatScheme to describe HELM File
 106 formats of a mathematical resource (possible values of the Dublin Core property
 107 format). Possible values of the rdf:about
 108 attribute can be XML.cic, XML.hol, XML.mizar. Each Helm format describes
 109 a logical framework. The class dcq:IMT contains values as text/xml, text/xhtml,
 110 text/mml, text/ps, text/tex, text/pdf.</rdfs:comment>
 111      <rdf:type rdf:resource="&rdfsns;Class"/>
 112      <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 113 </dcq:FormatScheme>
 114
 115 <dcq:IdentifierScheme rdf:about="&hthns;HelmID">
 116      <rdfs:comment>Instance of the class IdentifierScheme to describe HELM
 117 identifiers</rdfs:comment>
 118      <rdf:type rdf:resource="&rdfsns;Class"/>
 119      <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 120 </dcq:IdentifierScheme>
 121
 122 <!--  SubProperties of dc:description, dc:creator, dc:relation and
 123       hth:dependence                                               -->
 124
 125 <!-- SubProperty of dc:title -->
 126 <rdf:Property rdf:about="&hthns;shortName">
 127     <rdfs:comment>Short name (alias) of the mathematical resource</rdfs:comment>
 128     <rdfs:subPropertyOf rdf:resource="&dcns;title"/>
 129     <rdfs:domain rdf:resource="&hthns;MathResource"/>
 130     <rdfs:range rdf:resource="&xschemans;string"/>
 131     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 132 </rdf:Property>
 133
 134
 135 <!-- There are also dcq:created and dcq:modified dc:date subProperties -->
 136 <rdf:Property rdf:ID="firstVersion">
 137     <rdfs:comment>Any additional information about the first version of the
 138 mathematical resource</rdfs:comment>
 139     <rdfs:subPropertyOf rdf:resource="&dcns;description"/>
 140     <rdfs:domain rdf:resource="#MathResource"/>
 141     <rdfs:range rdf:resource="&xschemans;string"/>
 142 </rdf:Property>
 143
 144 <rdf:Property rdf:ID="modified">
 145     <rdfs:comment>Any additional information about the modified version of the
 146 mathematical resource</rdfs:comment>
 147     <rdfs:subPropertyOf rdf:resource="&dcns;description"/>
 148     <rdfs:domain rdf:resource="#MathResource"/>
 149     <rdfs:range rdf:resource="&xschemans;string"/>
 150 </rdf:Property>
 151
 152 <rdf:Property rdf:about="&hthns;institution">
 153     <rdfs:comment>Affiliated institution of the creator of the mathematical
 154 resource</rdfs:comment>
 155     <rdfs:subPropertyOf rdf:resource="&dcns;creator"/>
 156     <rdfs:domain rdf:resource="&hthns;MathResource"/>
 157     <rdfs:range rdf:resource="&xschemans;string"/>
 158     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 159 </rdf:Property>
 160
 161 <rdf:Property rdf:about="&hthns;contact">
 162     <rdfs:comment>Contact of the creator of the mathematical
 163 resource</rdfs:comment>
 164     <rdfs:subPropertyOf rdf:resource="&dcns;creator"/>
 165     <rdfs:domain rdf:resource="&hthns;MathResource"/>
 166     <rdfs:range rdf:resource="#Contact"/>
 167     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 168 </rdf:Property>
 169
 170 <rdf:Property rdf:about="&hthns;isBasedOn">
 171     <rdfs:comment>A relation between mathematical resources</rdfs:comment>
 172     <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
 173     <rdfs:domain rdf:resource="&hthns;MathResource"/>
 174     <rdfs:range rdf:resource="&hthns;HelmURI"/>
 175     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 176 </rdf:Property>
 177
 178 <rdf:Property rdf:about="&hthns;isBasisFor">
 179     <rdfs:comment>A relation between mathematical resources</rdfs:comment>
 180     <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
 181     <rdfs:domain rdf:resource="&hthns;MathResource"/>
 182     <rdfs:range rdf:resource="&hthns;HelmURI"/>
 183     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 184 </rdf:Property>
 185
 186 <rdf:Property rdf:about="&hthns;isSourceFor">
 187     <rdfs:comment>A relation between mathematical resources</rdfs:comment>
 188     <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
 189     <rdfs:domain rdf:resource="&hthns;MathResource"/>
 190     <rdfs:range rdf:resource="&hthns;HelmURI"/>
 191     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 192 </rdf:Property>
 193
 194 <rdf:Property rdf:about="&hthns;hasSource">
 195     <rdfs:comment>A relation between mathematical resources</rdfs:comment>
 196     <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
 197     <rdfs:domain rdf:resource="&hthns;MathResource"/>
 198     <rdfs:range rdf:resource="&hthns;HelmURI"/>
 199     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 200 </rdf:Property>
 201
 202 <rdf:Property rdf:about="&hthns;uses">
 203     <rdfs:comment>A dependence between theory items (for instance: between a theorem or anything else and a variable)</rdfs:comment>
 204     <rdfs:subPropertyOf rdf:resource="&hthns;dependence"/>
 205     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 206 </rdf:Property>
 207
 208 <rdf:Property rdf:about="&hthns;isUsedBy">
 209     <rdfs:comment>A dependence between theory items (for instance: between a variable and
 210 a theorem or anything else)</rdfs:comment>
 211     <rdfs:subPropertyOf rdf:resource="&hthns;dependence"/>
 212     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 213 </rdf:Property>
 214
 215 <rdf:Property rdf:about="&hthns;hasConsequence">
 216     <rdfs:comment>A dependence between theory items (for instance: between a theorem and
 217 a corollary)</rdfs:comment>
 218     <rdfs:subPropertyOf rdf:resource="&hthns;dependence"/>
 219     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 220 </rdf:Property>
 221
 222 <rdf:Property rdf:about="&hthns;isConsequenceOf">
 223     <rdfs:comment>A dependence between theory items (for instance: between a corollary
 224 and a theorem). Alternatively: IsResultOf</rdfs:comment>
 225     <rdfs:subPropertyOf rdf:resource="&hthns;dependence"/>
 226     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 227 </rdf:Property>
 228
 229 <rdf:Property rdf:about="&hthns;hasPremise">
 230     <rdfs:comment>A dependence between theory items (for instance: between a theorem
 231 and a lemma)</rdfs:comment>
 232     <rdfs:subPropertyOf rdf:resource="&hthns;dependence"/>
 233     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 234 </rdf:Property>
 235
 236 <rdf:Property rdf:about="&hthns;isPremiseOf">
 237     <rdfs:comment>A dependence between theory items (for instance: between a lemma
 238 and a theorem)</rdfs:comment>
 239     <rdfs:subPropertyOf rdf:resource="&hthns;dependence"/>
 240     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 241 </rdf:Property>
 242
 243 <!-- Properties -->
 244
 245 <rdf:Property rdf:about="&hthns;theoryItem">
 246     <rdfs:comment>Theory item</rdfs:comment>
 247     <rdfs:domain rdf:resource="&hthns;Theory"/>
 248     <rdfs:range rdf:resource="&hthns;TheoryItem"/>
 249     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 250 </rdf:Property>
 251
 252 <rdf:Property rdf:about="&hthns;dependence">
 253     <rdfs:comment>Dependence between theory items</rdfs:comment>
 254     <rdfs:domain rdf:resource="&hthns;TheoryItem"/>
 255     <rdfs:range rdf:resource="&hthns;HelmID"/>
 256     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 257 </rdf:Property>
 258
 259 <rdf:Property rdf:about="&hthns;itemType">
 260     <rdfs:comment>Axiom, Fact, Definition, Theorem, Lemma, Corollary,
 261 Variable. Redundant info: it is already captured by the corresponding xml data</rdfs:comment>
 262     <rdfs:domain rdf:resource="&hthns;TheoryItem"/>
 263     <rdfs:range rdf:resource="&xschemans;string"/>
 264     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 265 </rdf:Property>
 266
 267 <rdf:Property rdf:about="&hthns;label">
 268     <rdfs:comment>Description of the kind of objects: data type,
 269 algorithm, specification, theorem containing algorithm, verification (that the
 270 implementation satisfies the specification), predicate/relation, proposition</rdfs:comment>
 271     <rdfs:domain rdf:resource="&hthns;TheoryItem"/>
 272     <rdfs:range rdf:resource="&xschemans;string"/>
 273     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 274 </rdf:Property>
 275
 276 <!-- ex. f:N->Z => N>->Z and n:Nat => n:Z -->
 277 <rdf:Property rdf:about="&hthns;isCoercion">
 278     <rdfs:comment>A Definition item can be a coercion</rdfs:comment>
 279     <rdfs:domain rdf:resource="&hthns;TheoryItem"/>
 280     <rdfs:range rdf:resource="&xschemans;boolean"/>
 281     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 282 </rdf:Property>
 283
 284 <!-- The id info is no more contained in the theory xml doc, so there isn't
 285 redundant info between metadata and data -->
 286 <rdf:Property rdf:about="&hthns;ident">
 287     <rdfs:comment>Identifier of a theory item</rdfs:comment>
 288     <rdfs:domain rdf:resource="&hthns;TheoryItem"/>
 289     <rdfs:range rdf:resource="&hthns;HelmID"/>
 290     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 291 </rdf:Property>
 292
 293 <rdf:Property rdf:about="&hthns;email">
 294     <rdfs:comment>E-mail of the creator of the mathematical
 295 resource</rdfs:comment>
 296     <rdfs:domain rdf:resource="&hthns;Contact"/>
 297     <rdfs:range rdf:resource="&xschemans;string"/>
 298     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 299 </rdf:Property>
 300
 301 <rdf:Property rdf:about="&hthns;address">
 302     <rdfs:comment>Address of the creator of the mathematical
 303 resource</rdfs:comment>
 304     <rdfs:domain rdf:resource="&hthns;Contact"/>
 305     <rdfs:range rdf:resource="&xschemans;string"/>
 306     <rdfs:isDefinedBy rdf:resource = "&hthns;" />
 307 </rdf:Property>
 308
 309 <!-- HELM: Constraining an external (dc) property to a particular range and
 310 domain (hth:MathResource) should be possible. VRP gives a Warning when
 311 constraining (extending, adding constraints to) the range of a property
 312 defined in another schema (Consistency problems?No because it's an error
 313 modifying the original constraints): but where is the extensibility and
 314 reusability of RDF schemas? It's ok specializing a property with a
 315 subProperty. Anyway if the range of a property is not defined, VRP validates
 316 both if the property value is a resource, a class or a Literal.
 317 <rdf:Description rdf:about = "&dcns;type">
 318     <rdfs:domain rdf:resource="&hthns;MathResource"/>
 319 </rdf:Description> -->
 320
 321 </rdf:RDF>