3 <!-- Rdf Schema definition for theory files:
4 xmlns:hth="http://www.cs.unibo.it/~schena/schema-hth.rdf#" -->
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#">
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 -->
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"/>
24 <rdfs:Class rdf:ID="Theory">
25 <rdfs:comment>Mathematical resource represented by a theory</rdfs:comment>
26 <rdfs:subClassOf rdf:resource="#MathResource"/>
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>
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>
38 <rdfs:Class rdf:ID="ResourceType">
39 <rdfs:comment>Type of mathematical resource (possible values of the Dublin Core
40 property Type)</rdfs:comment>
43 <!-- Added subProperties of the Property dc:relation -->
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>
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>
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>
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>
73 <!-- subProperties of Property hth:dependence -->
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>
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>
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>
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>
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>
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>
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 -->
114 <rdfs:Class rdf:ID="Text.Abstract">
115 <rdf:type rdf:resource="#ResourceType"/>
118 <rdfs:Class rdf:ID="Text.Paper">
119 <rdf:type rdf:resource="#ResourceType"/>
122 <rdfs:Class rdf:ID="Text.Bibliography">
123 <rdf:type rdf:resource="#ResourceType"/>
126 <rdfs:Class rdf:ID="Text.HomePage">
127 <rdf:type rdf:resource="#ResourceType"/>
130 <rdfs:Class rdf:ID="Text.LectureNotes">
131 <rdf:type rdf:resource="#ResourceType"/>
134 <rdfs:Class rdf:ID="Text.Monograph">
135 <rdf:type rdf:resource="#ResourceType"/>
138 <rdfs:Class rdf:ID="Text.PatentSpec">
139 <rdf:type rdf:resource="#ResourceType"/>
142 <rdfs:Class rdf:ID="Text.Preprints">
143 <rdf:type rdf:resource="#ResourceType"/>
146 <rdfs:Class rdf:ID="Text.Proceedings">
147 <rdf:type rdf:resource="#ResourceType"/>
150 <rdfs:Class rdf:ID="Text.Review">
151 <rdf:type rdf:resource="#ResourceType"/>
154 <rdfs:Class rdf:ID="Text.Separatum">
155 <rdf:type rdf:resource="#ResourceType"/>
158 <rdfs:Class rdf:ID="Text.Serial">
159 <rdf:type rdf:resource="#ResourceType"/>
162 <rdfs:Class rdf:ID="Text.TechReport">
163 <rdf:type rdf:resource="#ResourceType"/>
166 <rdfs:Class rdf:ID="Text.Thesis">
167 <rdf:type rdf:resource="#ResourceType"/>
170 <rdfs:Class rdf:ID="Text.Enclosure">
171 <rdf:type rdf:resource="#ResourceType"/>
174 <rdfs:Class rdf:ID="Text.General">
175 <rdf:type rdf:resource="#ResourceType"/>
178 <rdfs:Class rdf:ID="Image">
179 <rdf:type rdf:resource="#ResourceType"/>
182 <rdfs:Class rdf:ID="Software.Exec">
183 <rdf:type rdf:resource="#ResourceType"/>
186 <rdfs:Class rdf:ID="Software.Source">
187 <rdf:type rdf:resource="#ResourceType"/>
190 <!-- NOTE: each helm format describes a logical framework -->
191 <!-- Instances of hth:ResourceFormat -->
193 <rdfs:Class rdf:ID="Text.xml">
194 <rdf:type rdf:resource="#ResourceFormat"/>
197 <rdfs:Class rdf:ID="Text.xhtml">
198 <rdf:type rdf:resource="#ResourceFormat"/>
201 <rdfs:Class rdf:ID="Text.mml">
202 <rdf:type rdf:resource="#ResourceFormat"/>
205 <rdfs:Class rdf:ID="Text.ps">
206 <rdf:type rdf:resource="#ResourceFormat"/>
209 <rdfs:Class rdf:ID="Text.pdf">
210 <rdf:type rdf:resource="#ResourceFormat"/>
213 <rdfs:Class rdf:ID="Text.tex">
214 <rdf:type rdf:resource="#ResourceFormat"/>
217 <rdfs:Class rdf:ID="XML.helm.cic">
218 <rdf:type rdf:resource="#ResourceFormat"/>
221 <rdfs:Class rdf:ID="XML.helm.mizar">
222 <rdf:type rdf:resource="#ResourceFormat"/>
225 <rdfs:Class rdf:ID="XML.helm.hol">
226 <rdf:type rdf:resource="#ResourceFormat"/>
231 <rdf:Property rdf:ID="theoryItem">
232 <rdfs:domain rdf:resource="#Theory"/>
233 <rdfs:range rdf:resource="#TheoryItem"/>
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"/>
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"/>
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"/>
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"/>
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"/>
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"/>
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"/>
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"/>
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"/>
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) -->
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"/>
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"/>