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 <rdf:RDF xml:lang="en"
   7        xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
   8        xmlns:rdfs="http://www.w3.org/2000/01/rdf-schema#"
   9        xmlns:dc="http://www.cs.unibo.it/~schena/dublin_core.rdf#">
  10
  11 <!-- RICORDA: aggiungi commento anche a proprieta' e istanze -->
  12 <!-- RICORDA: studiare tipi di dato (invece di Literal) -->
  13 <!-- RICORDA: specificare i contenuti dei dc elements -->
  14 <!-- RICORDA: verifica formato xml.helm.cic  -->
  15 <!-- RICORDA: aggiungi euler properties -->
  16
  17 <!-- Classes -->
  18
  19 <rdfs:Class rdf:ID="MathResource">
  20      <rdfs:comment>Mathematical resource</rdfs:comment>
  21      <rdfs:subClassOf rdf:resource="http://www.w3.org/2000/01/rdf-schema#Resource"/>
  22 </rdfs:Class>
  23
  24 <rdfs:Class rdf:ID="Theory">
  25      <rdfs:comment>Mathematical resource represented by a theory</rdfs:comment>
  26      <rdfs:subClassOf rdf:resource="#MathResource"/>
  27 </rdfs:Class>
  28
  29 <rdfs:Class rdf:ID="TheoryItem">
  30      <rdfs:comment>Theory item represented by: axiom, fact, definition, theorem, lemma, corollary, variable, specified by a XPath expression </rdfs:comment>
  31 </rdfs:Class>
  32
  33 <rdfs:Class rdf:ID="ResourceFormat">
  34      <rdfs:comment>File format of a mathematical resource (possible values of the
  35 Dublin Core property Format)</rdfs:comment>
  36 </rdfs:Class>
  37
  38 <rdfs:Class rdf:ID="ResourceType">
  39      <rdfs:comment>Type of mathematical resource (possible values of the Dublin Core
  40 property Type)</rdfs:comment>
  41 </rdfs:Class>
  42
  43 <!-- Added subProperties of the Property dc:relation -->
  44
  45 <rdf:Property rdf:ID="isBasedOn">
  46     <rdfs:subPropertyOf rdf:resource="http://www.cs.unibo.it/~schena/dublin_core.rdf#relation"/>
  47     <rdfs:domain rdf:resource="#MathResource"/>
  48     <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
  49     <rdfs:comment>A relation between mathematical resources</rdfs:comment>
  50 </rdf:Property>
  51
  52 <rdf:Property rdf:ID="isBasisFor">
  53     <rdfs:subPropertyOf rdf:resource="http://www.cs.unibo.it/~schena/dublin_core.rdf#relation"/>
  54     <rdfs:domain rdf:resource="#MathResource"/>
  55     <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
  56     <rdfs:comment>A relation between mathematical resources</rdfs:comment>
  57 </rdf:Property>
  58
  59 <rdf:Property rdf:ID="isSourceFor">
  60     <rdfs:subPropertyOf rdf:resource="http://www.cs.unibo.it/~schena/dublin_core.rdf#relation"/>
  61     <rdfs:domain rdf:resource="#MathResource"/>
  62     <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
  63     <rdfs:comment>A relation between mathematical resources</rdfs:comment>
  64 </rdf:Property>
  65
  66 <rdf:Property rdf:ID="hasSource">
  67     <rdfs:subPropertyOf rdf:resource="http://www.cs.unibo.it/~schena/dublin_core.rdf#relation"/>
  68     <rdfs:domain rdf:resource="#MathResource"/>
  69     <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
  70     <rdfs:comment>A relation between mathematical resources</rdfs:comment>
  71 </rdf:Property>
  72
  73 <!--  subProperties of Property hth:dependence -->
  74
  75 <rdf:Property rdf:ID="uses">
  76     <rdfs:subPropertyOf rdf:resource="#dependence"/>
  77     <rdfs:comment>A dependence between theory items (for instance: between a theorem or anything else and a variable)</rdfs:comment>
  78 </rdf:Property>
  79
  80 <rdf:Property rdf:ID="isUsedBy">
  81     <rdfs:subPropertyOf rdf:resource="#dependence"/>
  82     <rdfs:comment>A dependence between theory items (for instance: between a variable and
  83 a theorem or anything else)</rdfs:comment>
  84 </rdf:Property>
  85
  86 <rdf:Property rdf:ID="hasConsequence">
  87     <rdfs:subPropertyOf rdf:resource="#dependence"/>
  88     <rdfs:comment>A dependence between theory items (for instance: between a theorem and
  89 a corollary)</rdfs:comment>
  90 </rdf:Property>
  91
  92 <rdf:Property rdf:ID="isConsequenceOf">
  93     <rdfs:subPropertyOf rdf:resource="#dependence"/>
  94     <rdfs:comment>A dependence between theory items (for instance: between a corollary
  95 and a theorem). Alternatively: IsResultOf</rdfs:comment>
  96 </rdf:Property>
  97
  98 <rdf:Property rdf:ID="hasPremise">
  99     <rdfs:subPropertyOf rdf:resource="#dependence"/>
 100     <rdfs:comment>A dependence between theory items (for instance: between a theorem
 101 and a lemma)</rdfs:comment>
 102 </rdf:Property>
 103
 104 <rdf:Property rdf:ID="isPremiseOf">
 105     <rdfs:subPropertyOf rdf:resource="#dependence"/>
 106     <rdfs:comment>A dependence between theory items (for instance: between a lemma
 107 and a theorem)</rdfs:comment>
 108 </rdf:Property>
 109
 110 <!-- Text.general describes a document not of the following types. -->
 111 <!-- A helm theory has no type per se                              -->
 112 <!-- Instances of hth:ResourceType -->
 113
 114 <rdfs:Class rdf:ID="Text.Abstract">
 115     <rdf:type rdf:resource="#ResourceType"/>
 116 </rdfs:Class>
 117
 118 <rdfs:Class rdf:ID="Text.Paper">
 119     <rdf:type rdf:resource="#ResourceType"/>
 120 </rdfs:Class>
 121
 122 <rdfs:Class rdf:ID="Text.Bibliography">
 123     <rdf:type rdf:resource="#ResourceType"/>
 124 </rdfs:Class>
 125
 126 <rdfs:Class rdf:ID="Text.HomePage">
 127     <rdf:type rdf:resource="#ResourceType"/>
 128 </rdfs:Class>
 129
 130 <rdfs:Class rdf:ID="Text.LectureNotes">
 131     <rdf:type rdf:resource="#ResourceType"/>
 132 </rdfs:Class>
 133
 134 <rdfs:Class rdf:ID="Text.Monograph">
 135     <rdf:type rdf:resource="#ResourceType"/>
 136 </rdfs:Class>
 137
 138 <rdfs:Class rdf:ID="Text.PatentSpec">
 139     <rdf:type rdf:resource="#ResourceType"/>
 140 </rdfs:Class>
 141
 142 <rdfs:Class rdf:ID="Text.Preprints">
 143     <rdf:type rdf:resource="#ResourceType"/>
 144 </rdfs:Class>
 145
 146 <rdfs:Class rdf:ID="Text.Proceedings">
 147     <rdf:type rdf:resource="#ResourceType"/>
 148 </rdfs:Class>
 149
 150 <rdfs:Class rdf:ID="Text.Review">
 151     <rdf:type rdf:resource="#ResourceType"/>
 152 </rdfs:Class>
 153
 154 <rdfs:Class rdf:ID="Text.Separatum">
 155     <rdf:type rdf:resource="#ResourceType"/>
 156 </rdfs:Class>
 157
 158 <rdfs:Class rdf:ID="Text.Serial">
 159     <rdf:type rdf:resource="#ResourceType"/>
 160 </rdfs:Class>
 161
 162 <rdfs:Class rdf:ID="Text.TechReport">
 163     <rdf:type rdf:resource="#ResourceType"/>
 164 </rdfs:Class>
 165
 166 <rdfs:Class rdf:ID="Text.Thesis">
 167     <rdf:type rdf:resource="#ResourceType"/>
 168 </rdfs:Class>
 169
 170 <rdfs:Class rdf:ID="Text.Enclosure">
 171     <rdf:type rdf:resource="#ResourceType"/>
 172 </rdfs:Class>
 173
 174 <rdfs:Class rdf:ID="Text.General">
 175     <rdf:type rdf:resource="#ResourceType"/>
 176 </rdfs:Class>
 177
 178 <rdfs:Class rdf:ID="Image">
 179     <rdf:type rdf:resource="#ResourceType"/>
 180 </rdfs:Class>
 181
 182 <rdfs:Class rdf:ID="Software.Exec">
 183     <rdf:type rdf:resource="#ResourceType"/>
 184 </rdfs:Class>
 185
 186 <rdfs:Class rdf:ID="Software.Source">
 187     <rdf:type rdf:resource="#ResourceType"/>
 188 </rdfs:Class>
 189
 190 <!-- NOTE: each helm format describes a logical framework -->
 191 <!-- Instances of hth:ResourceFormat                      -->
 192
 193 <rdfs:Class rdf:ID="Text.xml">
 194     <rdf:type rdf:resource="#ResourceFormat"/>
 195 </rdfs:Class>
 196
 197 <rdfs:Class rdf:ID="Text.xhtml">
 198     <rdf:type rdf:resource="#ResourceFormat"/>
 199 </rdfs:Class>
 200
 201 <rdfs:Class rdf:ID="Text.mml">
 202     <rdf:type rdf:resource="#ResourceFormat"/>
 203 </rdfs:Class>
 204
 205 <rdfs:Class rdf:ID="Text.ps">
 206     <rdf:type rdf:resource="#ResourceFormat"/>
 207 </rdfs:Class>
 208
 209 <rdfs:Class rdf:ID="Text.pdf">
 210     <rdf:type rdf:resource="#ResourceFormat"/>
 211 </rdfs:Class>
 212
 213 <rdfs:Class rdf:ID="Text.tex">
 214     <rdf:type rdf:resource="#ResourceFormat"/>
 215 </rdfs:Class>
 216
 217 <rdfs:Class rdf:ID="XML.helm.cic">
 218     <rdf:type rdf:resource="#ResourceFormat"/>
 219 </rdfs:Class>
 220
 221 <rdfs:Class rdf:ID="XML.helm.mizar">
 222     <rdf:type rdf:resource="#ResourceFormat"/>
 223 </rdfs:Class>
 224
 225 <rdfs:Class rdf:ID="XML.helm.hol">
 226     <rdf:type rdf:resource="#ResourceFormat"/>
 227 </rdfs:Class>
 228
 229 <!-- Properties -->
 230
 231 <rdf:Property rdf:ID="theoryItem">
 232     <rdfs:domain rdf:resource="#Theory"/>
 233     <rdfs:range rdf:resource="#TheoryItem"/>
 234 </rdf:Property>
 235
 236 <rdf:Property rdf:ID="dependence">
 237     <rdfs:domain rdf:resource="#TheoryItem"/>
 238     <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
 239 </rdf:Property>
 240
 241 <rdf:Property rdf:ID="itemType">
 242     <rdfs:comment>Axiom, Fact, Definition, Theorem, Lemma, Corollary,
 243 Variable. Redundant info: it is already captured by the corresponding xml data</rdfs:comment>
 244     <rdfs:domain rdf:resource="#TheoryItem"/>
 245     <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
 246 </rdf:Property>
 247
 248 <rdf:Property rdf:ID="label">
 249     <rdfs:comment>Description of the kind of objects: data type,
 250 algorithm, specification, theorem containing algorithm, verification (that the
 251 implementation satisfies the specification), predicate/relation, proposition</rdfs:comment>
 252     <rdfs:domain rdf:resource="#TheoryItem"/>
 253     <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
 254 </rdf:Property>
 255
 256 <!-- ex. f:N->Z => N>->Z and n:Nat => n:Z -->
 257 <rdf:Property rdf:ID="isCoercion">
 258     <rdfs:comment>A Definition item can be a coercion</rdfs:comment>
 259     <rdfs:domain rdf:resource="#TheoryItem"/>
 260     <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
 261 </rdf:Property>
 262
 263 <!-- The id info is no more contained in the theory xml doc, so there isn't
 264 redundant info between metadata and data -->
 265 <rdf:Property rdf:ID="ident">
 266     <rdfs:domain rdf:resource="#TheoryItem"/>
 267     <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
 268 </rdf:Property>
 269
 270 <rdf:Property rdf:ID="institution">
 271     <rdfs:domain rdf:resource="#MathResource"/>
 272     <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
 273 </rdf:Property>
 274
 275 <rdf:Property rdf:ID="contact">
 276     <rdfs:domain rdf:resource="#MathResource"/>
 277     <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
 278 </rdf:Property>
 279
 280 <rdf:Property rdf:ID="firstVersion">
 281     <rdfs:domain rdf:resource="#MathResource"/>
 282     <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
 283 </rdf:Property>
 284
 285 <rdf:Property rdf:ID="modified">
 286     <rdfs:domain rdf:resource="#MathResource"/>
 287     <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
 288 </rdf:Property>
 289
 290 <!-- ATTENZIONE: si dovrebbero generare constraint che il dominio delle
 291 dc properties sia hth:MathResource e che il range sia strutturato. Ma per
 292 fare questo e' necessario definire NUOVE proprieta' (nuovo namespace) -->
 293
 294 <rdf:Property rdf:ID="type">
 295     <rdfs:subPropertyOf rdf:resource="http://www.cs.unibo.it/~schena/dublin_core.rdf#type"/>
 296     <rdfs:domain rdf:resource="#MathResource"/>
 297     <rdfs:range rdf:resource="#ResourceType"/>
 298 </rdf:Property>
 299
 300 <rdf:Property rdf:ID="format">
 301     <rdfs:subPropertyOf rdf:resource="http://www.cs.unibo.it/~schena/dublin_core.rdf#format"/>
 302     <rdfs:domain rdf:resource="#MathResource"/>
 303     <rdfs:range rdf:resource="#ResourceFormat"/>
 304 </rdf:Property>
 305
 306 </rdf:RDF>
 307
 308
 309
 310
 311
 312
 313
 314