]> matita.cs.unibo.it Git - helm.git/blob - helm/schemas/schema-hth
Added aliases and notation.
[helm.git] / 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>