3 <!-- Rdf Schema definition for theory files:
4 xmlns:hth="http://www.cs.unibo.it/~schena/schema-hth.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 <!ENTITY hthns 'http://www.cs.unibo.it/~schena/schema-hth.rdf#'>
15 <rdf:RDF xml:lang="en"
20 xmlns:xs="&xschemans;">
22 <!-- RICORDA: specificare i contenuti dei dc elements: problemi con RSSDB -->
23 <!-- RICORDA: aggiungi euler properties -->
25 <!-- Description of Schema -->
27 <rdf:Description rdf:about="&hthns;">
28 <rdf:value>The HELM Element Set v0.1</rdf:value>
29 <dc:title>The HELM Theory Element Set v0.1</dc:title>
30 <dc:publisher>The HELM Project</dc:publisher>
31 <dc:description>The HELM metadata vocabulary is a simple vocabulary
32 intended to facilitate discovery of mathematical resources.
34 <dc:language>English</dc:language>
35 <dc:relation rdf:resource="http://ww.cs.unibo.it/helm/"/>
36 <dc:date>2001-12-12</dc:date>
42 <rdfs:Class rdf:ID="MathResource">
43 <rdfs:comment>Mathematical resources</rdfs:comment>
44 <rdfs:subClassOf rdf:resource="&rdfsns;Resource"/>
45 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
48 <rdfs:Class rdf:ID="Theory">
49 <rdfs:comment>Mathematical resources represented by theories</rdfs:comment>
50 <rdfs:subClassOf rdf:resource="#MathResource"/>
51 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
54 <rdfs:Class rdf:ID="TheoryItem">
55 <rdfs:comment>Theory items represented by: axiom, fact, definition, theorem, lemma, corollary, variable, specified by a XPath expression</rdfs:comment>
56 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
59 <rdfs:Class rdf:ID="HelmFormat">
60 <rdfs:comment>HELM File formats of a mathematical resource (possible values of the Dublin Core property Format). Possible values of the rdf:about
61 attribute can be XML.cic, XML.hol, XML.mizar. Each Helm format describes
62 a logical framework. The class dcq:IMT contains values as text/xml, text/xhtml,
63 text/mml, text/ps, text/tex, text/pdf.</rdfs:comment>
64 <rdfs:subClassOf rdf:resource="&dcqns;FormatScheme"/>
65 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
68 <rdfs:Class rdf:ID="HelmURI">
69 <rdfs:comment>HELM URIs of a mathematical resource</rdfs:comment>
70 <rdfs:subClassOf rdf:resource="&dcqns;URI"/>
71 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
74 <rdfs:Class rdf:ID="HelmID">
75 <rdfs:comment>HELM identifiers</rdfs:comment>
76 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
79 <rdfs:Class rdf:ID="Contact">
80 <rdfs:comment>Creator contact information</rdfs:comment>
81 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
84 <!-- Added subProperties of the Property dc:relation -->
86 <rdf:Property rdf:ID="isBasedOn">
87 <rdfs:comment>A relation between mathematical resources</rdfs:comment>
88 <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
89 <rdfs:domain rdf:resource="#MathResource"/>
90 <rdfs:range rdf:resource="#HelmURI"/>
91 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
94 <rdf:Property rdf:ID="isBasisFor">
95 <rdfs:comment>A relation between mathematical resources</rdfs:comment>
96 <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
97 <rdfs:domain rdf:resource="#MathResource"/>
98 <rdfs:range rdf:resource="#HelmURI"/>
99 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
102 <rdf:Property rdf:ID="isSourceFor">
103 <rdfs:comment>A relation between mathematical resources</rdfs:comment>
104 <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
105 <rdfs:domain rdf:resource="#MathResource"/>
106 <rdfs:range rdf:resource="#HelmURI"/>
107 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
110 <rdf:Property rdf:ID="hasSource">
111 <rdfs:comment>A relation between mathematical resources</rdfs:comment>
112 <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
113 <rdfs:domain rdf:resource="#MathResource"/>
114 <rdfs:range rdf:resource="#HelmURI"/>
115 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
118 <!-- subProperties of Property hth:dependence -->
120 <rdf:Property rdf:ID="uses">
121 <rdfs:comment>A dependence between theory items (for instance: between a theorem or anything else and a variable)</rdfs:comment>
122 <rdfs:subPropertyOf rdf:resource="#dependence"/>
123 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
126 <rdf:Property rdf:ID="isUsedBy">
127 <rdfs:comment>A dependence between theory items (for instance: between a variable and
128 a theorem or anything else)</rdfs:comment>
129 <rdfs:subPropertyOf rdf:resource="#dependence"/>
130 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
133 <rdf:Property rdf:ID="hasConsequence">
134 <rdfs:comment>A dependence between theory items (for instance: between a theorem and
135 a corollary)</rdfs:comment>
136 <rdfs:subPropertyOf rdf:resource="#dependence"/>
137 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
140 <rdf:Property rdf:ID="isConsequenceOf">
141 <rdfs:comment>A dependence between theory items (for instance: between a corollary
142 and a theorem). Alternatively: IsResultOf</rdfs:comment>
143 <rdfs:subPropertyOf rdf:resource="#dependence"/>
144 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
147 <rdf:Property rdf:ID="hasPremise">
148 <rdfs:comment>A dependence between theory items (for instance: between a theorem
149 and a lemma)</rdfs:comment>
150 <rdfs:subPropertyOf rdf:resource="#dependence"/>
151 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
154 <rdf:Property rdf:ID="isPremiseOf">
155 <rdfs:comment>A dependence between theory items (for instance: between a lemma
156 and a theorem)</rdfs:comment>
157 <rdfs:subPropertyOf rdf:resource="#dependence"/>
158 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
161 <!-- Possible values of rdf:value of the dct:Text instance of dct:DCMIType,
162 can be: Abstract, Paper, Bibliography, HomePage, LectureNotes, Monograph,
163 PatentSpec, Preprints, Proceedings, Review, Separatum, Serial, TechReport,
164 Thesis, Enclosure, General. -->
165 <!-- There are dct:Image and dct:Software. Possible values of rdf:value
166 of the dct:Software can be: Exec, Source. -->
167 <!-- Text.general describes a document not of the following types. -->
168 <!-- A helm theory has no type per se -->
172 <rdf:Property rdf:ID="theoryItem">
173 <rdfs:comment>Theory item</rdfs:comment>
174 <rdfs:domain rdf:resource="#Theory"/>
175 <rdfs:range rdf:resource="#TheoryItem"/>
176 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
179 <rdf:Property rdf:ID="dependence">
180 <rdfs:comment>Dependence between theory items</rdfs:comment>
181 <rdfs:domain rdf:resource="#TheoryItem"/>
182 <rdfs:range rdf:resource="#HelmID"/>
183 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
186 <rdf:Property rdf:ID="itemType">
187 <rdfs:comment>Axiom, Fact, Definition, Theorem, Lemma, Corollary,
188 Variable. Redundant info: it is already captured by the corresponding xml data</rdfs:comment>
189 <rdfs:domain rdf:resource="#TheoryItem"/>
190 <rdfs:range rdf:resource="&xschemans;string"/>
191 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
194 <rdf:Property rdf:ID="label">
195 <rdfs:comment>Description of the kind of objects: data type,
196 algorithm, specification, theorem containing algorithm, verification (that the
197 implementation satisfies the specification), predicate/relation, proposition</rdfs:comment>
198 <rdfs:domain rdf:resource="#TheoryItem"/>
199 <rdfs:range rdf:resource="&xschemans;string"/>
200 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
203 <!-- ex. f:N->Z => N>->Z and n:Nat => n:Z -->
204 <rdf:Property rdf:ID="isCoercion">
205 <rdfs:comment>A Definition item can be a coercion</rdfs:comment>
206 <rdfs:domain rdf:resource="#TheoryItem"/>
207 <rdfs:range rdf:resource="&xschemans;boolean"/>
208 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
211 <!-- The id info is no more contained in the theory xml doc, so there isn't
212 redundant info between metadata and data -->
213 <rdf:Property rdf:ID="ident">
214 <rdfs:comment>Identifier of a theory item</rdfs:comment>
215 <rdfs:domain rdf:resource="#TheoryItem"/>
216 <rdfs:range rdf:resource="#HelmID"/>
217 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
220 <!-- There are also dcq:created and dcq:modified dc:date subProperties -->
221 <rdf:Property rdf:ID="firstVersion">
222 <rdfs:comment>Any additional information about the first version of the
223 mathematical resource</rdfs:comment>
224 <rdfs:subPropertyOf rdf:resource="&dcns;description"/>
225 <rdfs:domain rdf:resource="#MathResource"/>
226 <rdfs:range rdf:resource="&xschemans;string"/>
229 <rdf:Property rdf:ID="modified">
230 <rdfs:comment>Any additional information about the modified version of the
231 mathematical resource</rdfs:comment>
232 <rdfs:subPropertyOf rdf:resource="&dcns;description"/>
233 <rdfs:domain rdf:resource="#MathResource"/>
234 <rdfs:range rdf:resource="&xschemans;string"/>
237 <rdf:Property rdf:ID="institution">
238 <rdfs:comment>Affiliated institution of the creator of the mathematical
239 resource</rdfs:comment>
240 <rdfs:subPropertyOf rdf:resource="&dcns;creator"/>
241 <rdfs:domain rdf:resource="#MathResource"/>
242 <rdfs:range rdf:resource="&xschemans;string"/>
243 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
246 <rdf:Property rdf:ID="contact">
247 <rdfs:comment>Contact of the creator of the mathematical
248 resource</rdfs:comment>
249 <rdfs:subPropertyOf rdf:resource="&dcns;creator"/>
250 <rdfs:domain rdf:resource="#MathResource"/>
251 <rdfs:range rdf:resource="#Contact"/>
252 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
255 <rdf:Property rdf:ID="email">
256 <rdfs:comment>E-mail of the creator of the mathematical
257 resource</rdfs:comment>
258 <rdfs:domain rdf:resource="#Contact"/>
259 <rdfs:range rdf:resource="&xschemans;string"/>
260 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
263 <rdf:Property rdf:ID="address">
264 <rdfs:comment>Address of the creator of the mathematical
265 resource</rdfs:comment>
266 <rdfs:domain rdf:resource="#Contact"/>
267 <rdfs:range rdf:resource="&xschemans;string"/>
268 <rdfs:isDefinedBy rdf:resource = "&hthns;" />
271 <!-- HELM: Here we want to constraint an external (dc) property to a
272 particular range and domain (hth:MathResource). VRP gives a Warning when
273 (extending or modifying) constraining the range of a property defined
274 in another schema; the correct way is to specialize it with a subProperty. -->
275 <!-- <rdf:Description rdf:about = "&dcns;type">
276 <rdfs:domain rdf:resource="#MathResource"/>
277 </rdf:Description> -->