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    ]>
  13
  14 <rdf:RDF xml:lang="en"
  15        xmlns:rdf="&rdfns;"
  16        xmlns:rdfs="&rdfsns;"
  17        xmlns:dc="&dcns;"
  18        xmlns:dcq="&dcqns;"
  19        xmlns:xs="&xschemans;">
  20
  21 <!-- RICORDA: aggiungi commento anche a proprieta' e istanze -->
  22 <!-- RICORDA: studiare tipi di dato (invece di Literal) -->
  23 <!-- RICORDA: specificare i contenuti dei dc elements -->
  24 <!-- RICORDA: verifica formato xml.helm.cic  -->
  25 <!-- RICORDA: aggiungi euler properties -->
  26
  27 <!-- Classes -->
  28
  29 <rdfs:Class rdf:ID="MathResource">
  30      <rdfs:comment>Mathematical resource</rdfs:comment>
  31      <rdfs:subClassOf rdf:resource="&rdfsns;Resource"/>
  32 </rdfs:Class>
  33
  34 <rdfs:Class rdf:ID="Theory">
  35      <rdfs:comment>Mathematical resource represented by a theory</rdfs:comment>
  36      <rdfs:subClassOf rdf:resource="#MathResource"/>
  37 </rdfs:Class>
  38
  39 <rdfs:Class rdf:ID="TheoryItem">
  40      <rdfs:comment>Theory item represented by: axiom, fact, definition, theorem, lemma, corollary, variable, specified by a XPath expression </rdfs:comment>
  41 </rdfs:Class>
  42
  43 <rdfs:Class rdf:ID="HelmFormat">
  44      <rdfs:comment>HELM File format of a mathematical resource (possible values of the Dublin Core property Format). Possible values of its rdf:about
  45 attribute can be XML.cic, XML.hol, XML.mizar. Each Helm format describes
  46 a logical framework. The class dcq:IMT contains values as text/xml, text/xhtml,
  47 text/mml, text/ps, text/tex, text/pdf.</rdfs:comment>
  48      <rdfs:subClassOf rdf:resource="&dcqns;FormatScheme"/>
  49 </rdfs:Class>
  50
  51 <rdfs:Class rdf:ID="HelmURI">
  52      <rdfs:comment>HELM URI of a mathematical resource</rdfs:comment>
  53 </rdfs:Class>
  54
  55 <rdfs:Class rdf:ID="HelmID">
  56      <rdfs:comment>HELM identifier</rdfs:comment>
  57 </rdfs:Class>
  58
  59 <rdfs:Class rdf:ID="Contact">
  60      <rdfs:comment>Creator contact information</rdfs:comment>
  61 </rdfs:Class>
  62
  63 <!-- Added subProperties of the Property dc:relation -->
  64
  65 <rdf:Property rdf:ID="isBasedOn">
  66     <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
  67     <rdfs:domain rdf:resource="#MathResource"/>
  68     <rdfs:range rdf:resource="&rdfsns;Literal"/>
  69     <rdfs:comment>A relation between mathematical resources</rdfs:comment>
  70 </rdf:Property>
  71
  72 <rdf:Property rdf:ID="isBasisFor">
  73     <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
  74     <rdfs:domain rdf:resource="#MathResource"/>
  75     <rdfs:range rdf:resource="&rdfsns;Literal"/>
  76     <rdfs:comment>A relation between mathematical resources</rdfs:comment>
  77 </rdf:Property>
  78
  79 <rdf:Property rdf:ID="isSourceFor">
  80     <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
  81     <rdfs:domain rdf:resource="#MathResource"/>
  82     <rdfs:range rdf:resource="&rdfsns;Literal"/>
  83     <rdfs:comment>A relation between mathematical resources</rdfs:comment>
  84 </rdf:Property>
  85
  86 <rdf:Property rdf:ID="hasSource">
  87     <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
  88     <rdfs:domain rdf:resource="#MathResource"/>
  89     <rdfs:range rdf:resource="&rdfsns;Literal"/>
  90     <rdfs:comment>A relation between mathematical resources</rdfs:comment>
  91 </rdf:Property>
  92
  93 <!--  subProperties of Property hth:dependence -->
  94
  95 <rdf:Property rdf:ID="uses">
  96     <rdfs:subPropertyOf rdf:resource="#dependence"/>
  97     <rdfs:comment>A dependence between theory items (for instance: between a theorem or anything else and a variable)</rdfs:comment>
  98 </rdf:Property>
  99
 100 <rdf:Property rdf:ID="isUsedBy">
 101     <rdfs:subPropertyOf rdf:resource="#dependence"/>
 102     <rdfs:comment>A dependence between theory items (for instance: between a variable and
 103 a theorem or anything else)</rdfs:comment>
 104 </rdf:Property>
 105
 106 <rdf:Property rdf:ID="hasConsequence">
 107     <rdfs:subPropertyOf rdf:resource="#dependence"/>
 108     <rdfs:comment>A dependence between theory items (for instance: between a theorem and
 109 a corollary)</rdfs:comment>
 110 </rdf:Property>
 111
 112 <rdf:Property rdf:ID="isConsequenceOf">
 113     <rdfs:subPropertyOf rdf:resource="#dependence"/>
 114     <rdfs:comment>A dependence between theory items (for instance: between a corollary
 115 and a theorem). Alternatively: IsResultOf</rdfs:comment>
 116 </rdf:Property>
 117
 118 <rdf:Property rdf:ID="hasPremise">
 119     <rdfs:subPropertyOf rdf:resource="#dependence"/>
 120     <rdfs:comment>A dependence between theory items (for instance: between a theorem
 121 and a lemma)</rdfs:comment>
 122 </rdf:Property>
 123
 124 <rdf:Property rdf:ID="isPremiseOf">
 125     <rdfs:subPropertyOf rdf:resource="#dependence"/>
 126     <rdfs:comment>A dependence between theory items (for instance: between a lemma
 127 and a theorem)</rdfs:comment>
 128 </rdf:Property>
 129
 130 <!-- Possible values of rdf:value of the dct:Text instance of dct:DCMIType,
 131 can be: Abstract, Paper, Bibliography, HomePage, LectureNotes, Monograph,
 132 PatentSpec, Preprints, Proceedings, Review, Separatum, Serial, TechReport,
 133 Thesis, Enclosure, General.                                               -->
 134 <!-- There are dct:Image and dct:Software. Possible values of rdf:value
 135 of the dct:Software can be: Exec, Source.                                 -->
 136 <!-- Text.general describes a document not of the following types.        -->
 137 <!-- A helm theory has no type per se                                     -->
 138
 139 <!-- Properties -->
 140
 141 <rdf:Property rdf:ID="theoryItem">
 142     <rdfs:domain rdf:resource="#Theory"/>
 143     <rdfs:range rdf:resource="#TheoryItem"/>
 144 </rdf:Property>
 145
 146 <rdf:Property rdf:ID="dependence">
 147     <rdfs:domain rdf:resource="#TheoryItem"/>
 148     <rdfs:range rdf:resource="#HelmURI"/>
 149 </rdf:Property>
 150
 151 <rdf:Property rdf:ID="itemType">
 152     <rdfs:comment>Axiom, Fact, Definition, Theorem, Lemma, Corollary,
 153 Variable. Redundant info: it is already captured by the corresponding xml data</rdfs:comment>
 154     <rdfs:domain rdf:resource="#TheoryItem"/>
 155     <rdfs:range rdf:resource="&xschemans;string"/>
 156 </rdf:Property>
 157
 158 <rdf:Property rdf:ID="label">
 159     <rdfs:comment>Description of the kind of objects: data type,
 160 algorithm, specification, theorem containing algorithm, verification (that the
 161 implementation satisfies the specification), predicate/relation, proposition</rdfs:comment>
 162     <rdfs:domain rdf:resource="#TheoryItem"/>
 163     <rdfs:range rdf:resource="&xschemans;string"/>
 164 </rdf:Property>
 165
 166 <!-- ex. f:N->Z => N>->Z and n:Nat => n:Z -->
 167 <rdf:Property rdf:ID="isCoercion">
 168     <rdfs:comment>A Definition item can be a coercion</rdfs:comment>
 169     <rdfs:domain rdf:resource="#TheoryItem"/>
 170     <rdfs:range rdf:resource="&xschemans;boolean"/>
 171 </rdf:Property>
 172
 173 <!-- The id info is no more contained in the theory xml doc, so there isn't
 174 redundant info between metadata and data -->
 175 <rdf:Property rdf:ID="ident">
 176     <rdfs:domain rdf:resource="#TheoryItem"/>
 177     <rdfs:range rdf:resource="#HelmID"/>
 178 </rdf:Property>
 179
 180 <!-- There are also dcq:created and dcq:modified -->
 181 <rdf:Property rdf:ID="institution">
 182     <rdfs:subPropertyOf rdf:resource="&dcns;creator"/>
 183     <rdfs:domain rdf:resource="#MathResource"/>
 184     <rdfs:range rdf:resource="&xschemans;string"/>
 185 </rdf:Property>
 186
 187 <rdf:Property rdf:ID="contact">
 188     <rdfs:subPropertyOf rdf:resource="&dcns;creator"/>
 189     <rdfs:domain rdf:resource="#MathResource"/>
 190     <rdfs:range rdf:resource="#Contact"/>
 191 </rdf:Property>
 192
 193 <rdf:Property rdf:ID="email">
 194     <rdfs:domain rdf:resource="#Contact"/>
 195     <rdfs:range rdf:resource="&xschemans;string"/>
 196 </rdf:Property>
 197
 198 <rdf:Property rdf:ID="address">
 199     <rdfs:domain rdf:resource="#Contact"/>
 200     <rdfs:range rdf:resource="&xschemans;string"/>
 201 </rdf:Property>
 202
 203 <!-- HELM: Here we want to constraint an external (dc) property to a
 204 particular range and domain (hth:MathResource). VRP gives a Warning when
 205 (extending or modifying) constraining the range of a property defined
 206 in another schema; the correct way is to specialize it with a subProperty. -->
 207 <!-- <rdf:Description rdf:about = "&dcns;type">
 208     <rdfs:domain rdf:resource="#MathResource"/>
 209 </rdf:Description> -->
 210
 211
 212 </rdf:RDF>
 213
 214
 215
 216
 217
 218
 219
 220