<!-- Rdf Schema definition for theory files:
xmlns:hth="http://www.cs.unibo.it/~schena/schema-hth.rdf#" -->
+<!DOCTYPE rdf:RDF [
+ <!ENTITY rdfns 'http://www.w3.org/1999/02/22-rdf-syntax-ns#'>
+ <!ENTITY rdfsns 'http://www.w3.org/2000/01/rdf-schema#'>
+ <!ENTITY dcns 'http://www.cs.unibo.it/~schena/dces#'>
+ <!ENTITY dcqns 'http://www.cs.unibo.it/~schena/dcq#'>
+ <!ENTITY xschemans 'http://www.w3.org/1999/XMLSchema-datatypes#'>
+ ]>
+
<rdf:RDF xml:lang="en"
- xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
- xmlns:rdfs="http://www.w3.org/2000/01/rdf-schema#"
- xmlns:dc="http://www.cs.unibo.it/~schena/dublin_core.rdf#">
+ xmlns:rdf="&rdfns;"
+ xmlns:rdfs="&rdfsns;"
+ xmlns:dc="&dcns;"
+ xmlns:dcq="&dcqns;"
+ xmlns:xs="&xschemans;">
<!-- RICORDA: aggiungi commento anche a proprieta' e istanze -->
<!-- RICORDA: studiare tipi di dato (invece di Literal) -->
<rdfs:Class rdf:ID="MathResource">
<rdfs:comment>Mathematical resource</rdfs:comment>
- <rdfs:subClassOf rdf:resource="http://www.w3.org/2000/01/rdf-schema#Resource"/>
+ <rdfs:subClassOf rdf:resource="&rdfsns;Resource"/>
</rdfs:Class>
<rdfs:Class rdf:ID="Theory">
<rdfs:comment>Theory item represented by: axiom, fact, definition, theorem, lemma, corollary, variable, specified by a XPath expression </rdfs:comment>
</rdfs:Class>
-<rdfs:Class rdf:ID="ResourceFormat">
- <rdfs:comment>File format of a mathematical resource (possible values of the
-Dublin Core property Format)</rdfs:comment>
+<rdfs:Class rdf:ID="HelmFormat">
+ <rdfs:comment>HELM File format of a mathematical resource (possible values of the Dublin Core property Format). Possible values of its rdf:about
+attribute can be XML.cic, XML.hol, XML.mizar. Each Helm format describes
+a logical framework. The class dcq:IMT contains values as text/xml, text/xhtml,
+text/mml, text/ps, text/tex, text/pdf.</rdfs:comment>
+ <rdfs:subClassOf rdf:resource="&dcqns;FormatScheme"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="HelmURI">
+ <rdfs:comment>HELM URI of a mathematical resource</rdfs:comment>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="HelmID">
+ <rdfs:comment>HELM identifier</rdfs:comment>
</rdfs:Class>
-<rdfs:Class rdf:ID="ResourceType">
- <rdfs:comment>Type of mathematical resource (possible values of the Dublin Core
-property Type)</rdfs:comment>
+<rdfs:Class rdf:ID="Contact">
+ <rdfs:comment>Creator contact information</rdfs:comment>
</rdfs:Class>
<!-- Added subProperties of the Property dc:relation -->
<rdf:Property rdf:ID="isBasedOn">
- <rdfs:subPropertyOf rdf:resource="http://www.cs.unibo.it/~schena/dublin_core.rdf#relation"/>
+ <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
<rdfs:domain rdf:resource="#MathResource"/>
- <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+ <rdfs:range rdf:resource="&rdfsns;Literal"/>
<rdfs:comment>A relation between mathematical resources</rdfs:comment>
</rdf:Property>
<rdf:Property rdf:ID="isBasisFor">
- <rdfs:subPropertyOf rdf:resource="http://www.cs.unibo.it/~schena/dublin_core.rdf#relation"/>
+ <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
<rdfs:domain rdf:resource="#MathResource"/>
- <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+ <rdfs:range rdf:resource="&rdfsns;Literal"/>
<rdfs:comment>A relation between mathematical resources</rdfs:comment>
</rdf:Property>
<rdf:Property rdf:ID="isSourceFor">
- <rdfs:subPropertyOf rdf:resource="http://www.cs.unibo.it/~schena/dublin_core.rdf#relation"/>
+ <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
<rdfs:domain rdf:resource="#MathResource"/>
- <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+ <rdfs:range rdf:resource="&rdfsns;Literal"/>
<rdfs:comment>A relation between mathematical resources</rdfs:comment>
</rdf:Property>
<rdf:Property rdf:ID="hasSource">
- <rdfs:subPropertyOf rdf:resource="http://www.cs.unibo.it/~schena/dublin_core.rdf#relation"/>
+ <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
<rdfs:domain rdf:resource="#MathResource"/>
- <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+ <rdfs:range rdf:resource="&rdfsns;Literal"/>
<rdfs:comment>A relation between mathematical resources</rdfs:comment>
</rdf:Property>
and a theorem)</rdfs:comment>
</rdf:Property>
-<!-- Text.general describes a document not of the following types. -->
-<!-- A helm theory has no type per se -->
-<!-- Instances of hth:ResourceType -->
-
-<rdfs:Class rdf:ID="Text.Abstract">
- <rdf:type rdf:resource="#ResourceType"/>
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Text.Paper">
- <rdf:type rdf:resource="#ResourceType"/>
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Text.Bibliography">
- <rdf:type rdf:resource="#ResourceType"/>
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Text.HomePage">
- <rdf:type rdf:resource="#ResourceType"/>
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Text.LectureNotes">
- <rdf:type rdf:resource="#ResourceType"/>
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Text.Monograph">
- <rdf:type rdf:resource="#ResourceType"/>
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Text.PatentSpec">
- <rdf:type rdf:resource="#ResourceType"/>
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Text.Preprints">
- <rdf:type rdf:resource="#ResourceType"/>
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Text.Proceedings">
- <rdf:type rdf:resource="#ResourceType"/>
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Text.Review">
- <rdf:type rdf:resource="#ResourceType"/>
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Text.Separatum">
- <rdf:type rdf:resource="#ResourceType"/>
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Text.Serial">
- <rdf:type rdf:resource="#ResourceType"/>
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Text.TechReport">
- <rdf:type rdf:resource="#ResourceType"/>
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Text.Thesis">
- <rdf:type rdf:resource="#ResourceType"/>
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Text.Enclosure">
- <rdf:type rdf:resource="#ResourceType"/>
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Text.General">
- <rdf:type rdf:resource="#ResourceType"/>
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Image">
- <rdf:type rdf:resource="#ResourceType"/>
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Software.Exec">
- <rdf:type rdf:resource="#ResourceType"/>
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Software.Source">
- <rdf:type rdf:resource="#ResourceType"/>
-</rdfs:Class>
-
-<!-- NOTE: each helm format describes a logical framework -->
-<!-- Instances of hth:ResourceFormat -->
-
-<rdfs:Class rdf:ID="Text.xml">
- <rdf:type rdf:resource="#ResourceFormat"/>
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Text.xhtml">
- <rdf:type rdf:resource="#ResourceFormat"/>
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Text.mml">
- <rdf:type rdf:resource="#ResourceFormat"/>
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Text.ps">
- <rdf:type rdf:resource="#ResourceFormat"/>
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Text.pdf">
- <rdf:type rdf:resource="#ResourceFormat"/>
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="Text.tex">
- <rdf:type rdf:resource="#ResourceFormat"/>
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="XML.helm.cic">
- <rdf:type rdf:resource="#ResourceFormat"/>
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="XML.helm.mizar">
- <rdf:type rdf:resource="#ResourceFormat"/>
-</rdfs:Class>
-
-<rdfs:Class rdf:ID="XML.helm.hol">
- <rdf:type rdf:resource="#ResourceFormat"/>
-</rdfs:Class>
+<!-- Possible values of rdf:value of the dct:Text instance of dct:DCMIType,
+can be: Abstract, Paper, Bibliography, HomePage, LectureNotes, Monograph,
+PatentSpec, Preprints, Proceedings, Review, Separatum, Serial, TechReport,
+Thesis, Enclosure, General. -->
+<!-- There are dct:Image and dct:Software. Possible values of rdf:value
+of the dct:Software can be: Exec, Source. -->
+<!-- Text.general describes a document not of the following types. -->
+<!-- A helm theory has no type per se -->
<!-- Properties -->
<rdf:Property rdf:ID="dependence">
<rdfs:domain rdf:resource="#TheoryItem"/>
- <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+ <rdfs:range rdf:resource="#HelmURI"/>
</rdf:Property>
<rdf:Property rdf:ID="itemType">
<rdfs:comment>Axiom, Fact, Definition, Theorem, Lemma, Corollary,
Variable. Redundant info: it is already captured by the corresponding xml data</rdfs:comment>
<rdfs:domain rdf:resource="#TheoryItem"/>
- <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+ <rdfs:range rdf:resource="&xschemans;string"/>
</rdf:Property>
<rdf:Property rdf:ID="label">
algorithm, specification, theorem containing algorithm, verification (that the
implementation satisfies the specification), predicate/relation, proposition</rdfs:comment>
<rdfs:domain rdf:resource="#TheoryItem"/>
- <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+ <rdfs:range rdf:resource="&xschemans;string"/>
</rdf:Property>
<!-- ex. f:N->Z => N>->Z and n:Nat => n:Z -->
<rdf:Property rdf:ID="isCoercion">
<rdfs:comment>A Definition item can be a coercion</rdfs:comment>
<rdfs:domain rdf:resource="#TheoryItem"/>
- <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+ <rdfs:range rdf:resource="&xschemans;boolean"/>
</rdf:Property>
<!-- The id info is no more contained in the theory xml doc, so there isn't
redundant info between metadata and data -->
<rdf:Property rdf:ID="ident">
<rdfs:domain rdf:resource="#TheoryItem"/>
- <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+ <rdfs:range rdf:resource="#HelmID"/>
</rdf:Property>
+<!-- There are also dcq:created and dcq:modified -->
<rdf:Property rdf:ID="institution">
+ <rdfs:subPropertyOf rdf:resource="&dcns;creator"/>
<rdfs:domain rdf:resource="#MathResource"/>
- <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+ <rdfs:range rdf:resource="&xschemans;string"/>
</rdf:Property>
<rdf:Property rdf:ID="contact">
+ <rdfs:subPropertyOf rdf:resource="&dcns;creator"/>
<rdfs:domain rdf:resource="#MathResource"/>
- <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+ <rdfs:range rdf:resource="#Contact"/>
</rdf:Property>
-<rdf:Property rdf:ID="firstVersion">
- <rdfs:domain rdf:resource="#MathResource"/>
- <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+<rdf:Property rdf:ID="email">
+ <rdfs:domain rdf:resource="#Contact"/>
+ <rdfs:range rdf:resource="&xschemans;string"/>
</rdf:Property>
-<rdf:Property rdf:ID="modified">
- <rdfs:domain rdf:resource="#MathResource"/>
- <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+<rdf:Property rdf:ID="address">
+ <rdfs:domain rdf:resource="#Contact"/>
+ <rdfs:range rdf:resource="&xschemans;string"/>
</rdf:Property>
-<!-- ATTENZIONE: si dovrebbero generare constraint che il dominio delle
-dc properties sia hth:MathResource e che il range sia strutturato. Ma per
-fare questo e' necessario definire NUOVE proprieta' (nuovo namespace) -->
-
-<rdf:Property rdf:ID="type">
- <rdfs:subPropertyOf rdf:resource="http://www.cs.unibo.it/~schena/dublin_core.rdf#type"/>
+<!-- HELM: Here we want to constraint an external (dc) property to a
+particular range and domain (hth:MathResource). VRP gives a Warning when
+(extending or modifying) constraining the range of a property defined
+in another schema; the correct way is to specialize it with a subProperty. -->
+<!-- <rdf:Description rdf:about = "&dcns;type">
<rdfs:domain rdf:resource="#MathResource"/>
- <rdfs:range rdf:resource="#ResourceType"/>
-</rdf:Property>
+</rdf:Description> -->
-<rdf:Property rdf:ID="format">
- <rdfs:subPropertyOf rdf:resource="http://www.cs.unibo.it/~schena/dublin_core.rdf#format"/>
- <rdfs:domain rdf:resource="#MathResource"/>
- <rdfs:range rdf:resource="#ResourceFormat"/>
-</rdf:Property>
</rdf:RDF>
projects / helm.git / blobdiff