+<?xml version="1.0"?>
+
+<!-- Rdf Schema definition for theory files:
+xmlns:hth="http://www.cs.unibo.it/~schena/schema-hth.rdf#" -->
+
+<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#">
+
+<!-- RICORDA: aggiungi commento anche a proprieta' e istanze -->
+<!-- RICORDA: studiare tipi di dato (invece di Literal) -->
+<!-- RICORDA: specificare i contenuti dei dc elements -->
+<!-- RICORDA: verifica formato xml.helm.cic -->
+<!-- RICORDA: aggiungi euler properties -->
+
+<!-- Classes -->
+
+<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:Class>
+
+<rdfs:Class rdf:ID="Theory">
+ <rdfs:comment>Mathematical resource represented by a theory</rdfs:comment>
+ <rdfs:subClassOf rdf:resource="#MathResource"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="TheoryItem">
+ <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>
+
+<rdfs:Class rdf:ID="ResourceType">
+ <rdfs:comment>Type of mathematical resource (possible values of the Dublin Core
+property Type)</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:domain rdf:resource="#MathResource"/>
+ <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#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:domain rdf:resource="#MathResource"/>
+ <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#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:domain rdf:resource="#MathResource"/>
+ <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#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:domain rdf:resource="#MathResource"/>
+ <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+ <rdfs:comment>A relation between mathematical resources</rdfs:comment>
+</rdf:Property>
+
+<!-- subProperties of Property hth:dependence -->
+
+<rdf:Property rdf:ID="uses">
+ <rdfs:subPropertyOf rdf:resource="#dependence"/>
+ <rdfs:comment>A dependence between theory items (for instance: between a theorem or anything else and a variable)</rdfs:comment>
+</rdf:Property>
+
+<rdf:Property rdf:ID="isUsedBy">
+ <rdfs:subPropertyOf rdf:resource="#dependence"/>
+ <rdfs:comment>A dependence between theory items (for instance: between a variable and
+a theorem or anything else)</rdfs:comment>
+</rdf:Property>
+
+<rdf:Property rdf:ID="hasConsequence">
+ <rdfs:subPropertyOf rdf:resource="#dependence"/>
+ <rdfs:comment>A dependence between theory items (for instance: between a theorem and
+a corollary)</rdfs:comment>
+</rdf:Property>
+
+<rdf:Property rdf:ID="isConsequenceOf">
+ <rdfs:subPropertyOf rdf:resource="#dependence"/>
+ <rdfs:comment>A dependence between theory items (for instance: between a corollary
+and a theorem). Alternatively: IsResultOf</rdfs:comment>
+</rdf:Property>
+
+<rdf:Property rdf:ID="hasPremise">
+ <rdfs:subPropertyOf rdf:resource="#dependence"/>
+ <rdfs:comment>A dependence between theory items (for instance: between a theorem
+and a lemma)</rdfs:comment>
+</rdf:Property>
+
+<rdf:Property rdf:ID="isPremiseOf">
+ <rdfs:subPropertyOf rdf:resource="#dependence"/>
+ <rdfs:comment>A dependence between theory items (for instance: between a lemma
+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>
+
+<!-- Properties -->
+
+<rdf:Property rdf:ID="theoryItem">
+ <rdfs:domain rdf:resource="#Theory"/>
+ <rdfs:range rdf:resource="#TheoryItem"/>
+</rdf:Property>
+
+<rdf:Property rdf:ID="dependence">
+ <rdfs:domain rdf:resource="#TheoryItem"/>
+ <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+</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"/>
+</rdf:Property>
+
+<rdf:Property rdf:ID="label">
+ <rdfs:comment>Description of the kind of objects: data type,
+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"/>
+</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"/>
+</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"/>
+</rdf:Property>
+
+<rdf:Property rdf:ID="institution">
+ <rdfs:domain rdf:resource="#MathResource"/>
+ <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+</rdf:Property>
+
+<rdf:Property rdf:ID="contact">
+ <rdfs:domain rdf:resource="#MathResource"/>
+ <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+</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:Property rdf:ID="modified">
+ <rdfs:domain rdf:resource="#MathResource"/>
+ <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+</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"/>
+ <rdfs:domain rdf:resource="#MathResource"/>
+ <rdfs:range rdf:resource="#ResourceType"/>
+</rdf:Property>
+
+<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>
+
+
+
+
+
+
+
+