]> matita.cs.unibo.it Git - helm.git/blob - helm/schemas/schema-h
f26e003e1125b4694a192165937b8581e0a27748
[helm.git] / helm / schemas / schema-h
1 <?xml version="1.0"?>
2
3 <!-- Rdf Schema definition for CIC XML files:
4 xmlns:h="http://www.cs.unibo.it/~schena/schema-h#" -->
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 hthns 'http://www.cs.unibo.it/~schena/schema-hth#'>
10         <!ENTITY hns 'http://www.cs.unibo.it/~schena/schema-h#'>
11         <!ENTITY xschemans 'http://www.w3.org/1999/XMLSchema-datatypes#'>
12         <!ENTITY dcns 'http://www.cs.unibo.it/~schena/dces#'>
13         <!ENTITY dcqns 'http://www.cs.unibo.it/~schena/dcq#'>
14    ]>
15
16 <rdf:RDF xml:lang="en"
17        xmlns:rdf="&rdfns;"
18        xmlns:rdfs="&rdfsns;"
19        xmlns:hth="&hthns;"
20        xmlns:h="&hns;"
21        xmlns:xs="&xschemans;"
22        xmlns:dc="&dcns;"
23        xmlns:dcq="&dcqns;">
24
25 <!-- RICORDA: metadati solo su oggetto (come teoria ma piu' specifici) (non 
26 distinzione tipi di body) e non ridondanze se non riducono il numero di doc 
27 da parsare  -->
28
29 <!-- Description of Schema -->
30         
31 <rdf:Description rdf:about="&hns;">
32   <rdfs:label>The HELM Element Set v0.1</rdfs:label>
33   <dc:title>The HELM Object Element Set v0.1</dc:title>
34   <dc:publisher>The HELM Project</dc:publisher>
35   <dc:description>The HELM metadata vocabulary is a simple vocabulary
36       intended to facilitate discovery of mathematical resources. 
37   </dc:description>
38   <dc:language>English</dc:language>
39   <dc:relation rdf:resource="http://ww.cs.unibo.it/helm/"/>
40   <dcq:isRequiredBy rdf:resource="&hns;"/>
41   <dcq:conformsTo rdf:resource="http://www.w3.org/RDF/"/>
42   <dcq:issued>2000-6-3</dcq:issued>
43   <dcq:modified>2002-9-6</dcq:modified>
44   <rdfs:isDefinedBy rdf:resource = "&hthns;" />
45 </rdf:Description>
46
47
48 <!-- Classes -->
49
50 <rdfs:Class rdf:about="&hns;Object">
51      <rdfs:comment>Mathematical objects represented by a CIC XML 
52 file</rdfs:comment>
53      <rdfs:subClassOf rdf:resource="&hthns;MathResource"/>
54      <rdfs:isDefinedBy rdf:resource = "&hns;" />
55 </rdfs:Class>
56
57 <!-- Objects can inherit its dc properties -->
58 <rdfs:Class rdf:about="&hns;DirectoryOfObjects">
59      <rdfs:comment>Mathematical resources (directories) represented by sets 
60 of CIC XML files, contained in the tree that has the dir as root </rdfs:comment>
61      <rdfs:subClassOf rdf:resource="&hthns;MathResource"/>
62      <rdfs:isDefinedBy rdf:resource = "&hns;" />
63 </rdfs:Class>
64
65 <rdfs:Class rdf:about="&hns;Statement">
66      <rdfs:comment>Types of objects</rdfs:comment>
67      <rdfs:isDefinedBy rdf:resource = "&hns;" />
68 </rdfs:Class>
69
70 <rdfs:Class rdf:about="&hns;Body">
71      <rdfs:comment>Terms of objects</rdfs:comment>
72      <rdfs:isDefinedBy rdf:resource = "&hns;" />
73 </rdfs:Class>
74
75 <rdfs:Class rdf:about="&hns;Occurrence">
76      <rdfs:comment>Occurrences of an object inside an object</rdfs:comment>
77      <rdfs:isDefinedBy rdf:resource = "&hns;" />
78 </rdfs:Class>
79
80 <rdfs:Class rdf:about="&hns;Position">
81      <rdfs:comment>Positions of occurrences of an object inside an object</rdfs:comment>
82      <rdfs:isDefinedBy rdf:resource = "&hns;" />
83 </rdfs:Class>
84
85 <rdfs:Class rdf:about="&hns;Postit">
86      <rdfs:comment>Additional information associated to fragments of the objects</rdfs:comment>
87      <rdfs:isDefinedBy rdf:resource = "&hns;" />
88 </rdfs:Class>
89
90 <rdfs:Class rdf:about="&hns;Const">
91      <rdfs:comment>Constants in the body of an object</rdfs:comment>
92      <rdfs:isDefinedBy rdf:resource = "&hns;" />
93 </rdfs:Class>
94
95 <rdfs:Class rdf:about="&hns;StatementId">
96      <rdfs:comment>Identifiers in the statement</rdfs:comment>
97      <rdfs:isDefinedBy rdf:resource = "&hns;" />
98 </rdfs:Class>
99
100 <rdfs:Class rdf:about="&hns;BodyId">
101      <rdfs:comment>Identifiers in the body</rdfs:comment>
102      <rdfs:isDefinedBy rdf:resource = "&hns;" />
103 </rdfs:Class>
104
105 <rdfs:Class rdf:about="&hns;ImplArg">
106      <rdfs:comment>Implicit arguments</rdfs:comment>
107      <rdfs:isDefinedBy rdf:resource = "&hns;" /> 
108 </rdfs:Class>
109
110 <!-- Instances of the class h:Position -->
111
112 <h:Position rdf:about="&hns;MainHypothesis">
113     <rdfs:comment>Occurrences of an object in head position of some hypothesis 
114      of an object statement</rdfs:comment>
115     <rdf:type rdf:resource="&rdfsns;Class"/>
116     <rdfs:isDefinedBy rdf:resource = "&hns;" />
117 </h:Position>
118
119 <h:Position rdf:about="InHypothesis">
120     <rdfs:comment>Occurrences of an object in the hypotheses of an object 
121      statement</rdfs:comment>
122     <rdf:type rdf:resource="&rdfsns;Class"/>
123     <rdfs:isDefinedBy rdf:resource = "&hns;" />
124 </h:Position>
125
126 <h:Position rdf:about="&hns;MainConclusion">
127     <rdfs:comment>Occurrences of an object in head position of the 
128      conclusion of an object statement</rdfs:comment>
129     <rdf:type rdf:resource="&rdfsns;Class"/>
130     <rdfs:isDefinedBy rdf:resource = "&hns;" />
131 </h:Position>
132
133 <h:Position rdf:about="&hns;InConclusion">
134     <rdfs:comment>Occurrences of an object in the conclusion of an object
135      statement</rdfs:comment>  
136     <rdf:type rdf:resource="&rdfsns;Class"/>
137     <rdfs:isDefinedBy rdf:resource = "&hns;" />
138 </h:Position>
139
140 <h:Position rdf:about="&hns;InBody">
141     <rdfs:comment>Occurrences of an object only in an object body (not in the 
142      statement)</rdfs:comment>
143     <rdf:type rdf:resource="&rdfsns;Class"/>
144     <rdfs:isDefinedBy rdf:resource = "&hns;" />
145 </h:Position>
146
147 <!-- Properties -->
148
149 <rdf:Property rdf:about="&hns;statement">
150     <rdfs:comment>Statement</rdfs:comment>
151     <rdfs:domain rdf:resource="&hns;Object"/>
152     <rdfs:range rdf:resource="&hns;Statement"/>
153     <rdfs:isDefinedBy rdf:resource = "&hns;" />
154 </rdf:Property>
155
156 <rdf:Property rdf:about="&hns;body">
157     <rdfs:comment>Body</rdfs:comment>
158     <rdfs:domain rdf:resource="&hns;Object"/>
159     <rdfs:range rdf:resource="&hns;Body"/>
160     <rdfs:isDefinedBy rdf:resource = "&hns;" />
161 </rdf:Property>
162
163 <rdf:Property rdf:about="&hns;statementId">
164     <rdfs:comment>Statement identifier</rdfs:comment>
165     <rdfs:domain rdf:resource="&hns;Statement"/>
166     <rdfs:range rdf:resource="&hns;StatementId"/>
167     <rdfs:isDefinedBy rdf:resource = "&hns;" />
168 </rdf:Property>
169
170 <rdf:Property rdf:about="&hns;constrId">
171     <rdfs:comment>Constructor identifier of the statement conclusion</rdfs:comment>
172     <rdfs:domain rdf:resource="&hns;StatementId"/>
173     <rdfs:range rdf:resource="&hthns;HelmID"/>
174     <rdfs:isDefinedBy rdf:resource = "&hns;" />
175 </rdf:Property>
176
177 <rdf:Property rdf:about="&hns;listId">
178     <rdfs:comment>List of all ids in the domain</rdfs:comment>
179     <rdfs:domain rdf:resource="&hns;StatementId"/>
180     <rdfs:domain rdf:resource="&hns;BodyId"/>
181     <rdfs:range rdf:resource="&rdfns;Seq"/>
182     <rdfs:isDefinedBy rdf:resource = "&hns;" />
183 </rdf:Property>
184
185 <rdf:Property rdf:about="&hns;bodyId">
186     <rdfs:comment>Body identifier</rdfs:comment>
187     <rdfs:domain rdf:resource="&hns;Body"/>
188     <rdfs:range rdf:resource="&hns;BodyId"/>
189     <rdfs:isDefinedBy rdf:resource = "&hns;" />
190 </rdf:Property>
191
192 <rdf:Property rdf:about="&hns;refObj">
193     <rdfs:comment>Reference to an object</rdfs:comment>
194     <rdfs:domain rdf:resource="&hns;Object"/>
195     <rdfs:range rdf:resource="&hns;Occurrence"/>
196     <rdfs:isDefinedBy rdf:resource = "&hns;" />
197 </rdf:Property>
198
199 <rdf:Property rdf:about="&hns;constrImplArg">
200     <rdfs:comment>Implicit arguments of constructors</rdfs:comment>
201     <rdfs:domain rdf:resource="&hns;Statement"/>
202     <rdfs:range rdf:resource="&hns;ImplArg"/>
203     <rdfs:isDefinedBy rdf:resource = "&hns;" />
204 </rdf:Property>
205
206 <rdf:Property rdf:about="&hns;objImplArg">
207     <rdfs:comment>Implicit arguments of objects</rdfs:comment>
208     <rdfs:domain rdf:resource="&hns;Object"/>
209     <rdfs:range rdf:resource="&hns;ImplArg"/>
210     <rdfs:isDefinedBy rdf:resource = "&hns;" />
211 </rdf:Property>
212
213 <rdf:Property rdf:about="&hns;listImplArg">
214     <rdfs:comment>List of implicit arguments</rdfs:comment>
215     <rdfs:domain rdf:resource="&hns;ImplArg"/>
216     <rdfs:range rdf:resource="&rdfns;Seq"/>
217     <rdfs:isDefinedBy rdf:resource = "&hns;" />
218 </rdf:Property>
219
220 <rdf:Property rdf:about="&hns;backPointer">
221     <rdfs:comment>Backwards pointer: who points the object</rdfs:comment>
222     <rdfs:domain rdf:resource="&hns;Object"/>
223     <rdfs:range rdf:resource="&hns;Occurrence"/>
224     <rdfs:isDefinedBy rdf:resource = "&hns;" />
225 </rdf:Property>
226
227 <rdf:Property rdf:about="&hns;occurrence">
228     <rdfs:comment>URI of an object</rdfs:comment>
229     <rdfs:domain rdf:resource="&hns;Occurrence"/>
230     <rdfs:range rdf:resource="&hthns;HelmURI"/>
231     <rdfs:isDefinedBy rdf:resource = "&hns;" />
232 </rdf:Property>
233
234 <rdf:Property rdf:about="&hns;position">
235     <rdfs:comment>Position of an occurrence</rdfs:comment>
236     <rdfs:domain rdf:resource="&hns;Occurrence"/>
237     <rdfs:range rdf:resource="&hns;Position"/>
238     <rdfs:isDefinedBy rdf:resource = "&hns;" />
239 </rdf:Property>
240
241
242 <rdf:Property rdf:about="&hns;postit">
243     <rdfs:comment>Postit</rdfs:comment>
244     <rdfs:domain rdf:resource="&hns;Object"/>
245     <rdfs:range rdf:resource="&hns;Postit"/>
246     <rdfs:isDefinedBy rdf:resource = "&hns;" />
247 </rdf:Property>
248
249 <rdf:Property rdf:about="&hns;content">
250     <rdfs:comment>Content of a Postit</rdfs:comment>
251     <rdfs:domain rdf:resource="#Postit"/>
252     <rdfs:range rdf:resource="&xschemans;string"/>
253     <rdfs:isDefinedBy rdf:resource = "&hns;" />
254 </rdf:Property>
255
256 <rdf:Property rdf:about="&hns;refersTo">
257     <rdfs:comment>Identifies the object fragment (Xpointer) which Postit
258 refers to</rdfs:comment>
259     <rdfs:domain rdf:resource="&hns;Postit"/>
260     <rdfs:range rdf:resource="&hthns;HelmURI"/>
261     <rdfs:isDefinedBy rdf:resource = "&hns;" />
262 </rdf:Property>
263
264 <rdf:Property rdf:about="&hns;coercion">
265     <rdfs:comment>If the object can be a coercion</rdfs:comment>
266     <rdfs:domain rdf:resource="&hns;Object"/>
267     <rdfs:range rdf:resource="&xschemans;boolean"/>
268     <rdfs:isDefinedBy rdf:resource = "&hns;" /> 
269 </rdf:Property>
270
271 </rdf:RDF>