+++ /dev/null
-<?xml version="1.0"?>
-
-<!-- Rdf Schema definition for theory files:
-xmlns:hth="http://www.cs.unibo.it/~schena/schema-hth#" -->
-
-<!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 dctns 'http://www.cs.unibo.it/~schena/dctype#'>
- <!ENTITY xschemans 'http://www.w3.org/1999/XMLSchema-datatypes#'>
- <!ENTITY hthns 'http://www.cs.unibo.it/~schena/schema-hth#'>
- <!ENTITY hns 'http://www.cs.unibo.it/~schena/schema-h#'>
- ]>
-
-<rdf:RDF xml:lang="en"
- xmlns:rdf="&rdfns;"
- xmlns:rdfs="&rdfsns;"
- xmlns:dc="&dcns;"
- xmlns:dcq="&dcqns;"
- xmlns:dct="&dctns;"
- xmlns:xs="&xschemans;">
-
-<!-- RICORDA: specificare i contenuti dei dc elements: problemi con RSSDB -->
-<!-- RICORDA: aggiungi euler properties -->
-
-<!-- Description of Schema -->
-
-<rdf:Description rdf:about="&hthns;">
- <rdfs:label>The HELM Element Set v0.1</rdfs:label>
- <dc:title>The HELM Theory Element Set v0.1</dc:title>
- <dc:publisher>The HELM Project</dc:publisher>
- <dc:description>The HELM metadata vocabulary is a simple vocabulary
- intended to facilitate discovery of mathematical resources.
- </dc:description>
- <dc:language>English</dc:language>
- <dc:relation rdf:resource="http://www.cs.unibo.it/helm/"/>
- <dcq:isRequiredBy rdf:resource="&hns;"/>
- <dcq:conformsTo rdf:resource="http://www.w3.org/RDF/"/>
- <dcq:issued>2000-6-3</dcq:issued>
- <dcq:modified>2002-9-6</dcq:modified>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Description>
-
-
-<!-- Classes -->
-
-<rdfs:Class rdf:about="&hthns;MathResource">
- <rdfs:comment>Mathematical resources</rdfs:comment>
- <rdfs:subClassOf rdf:resource="&rdfsns;Resource"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdfs:Class>
-
-<rdfs:Class rdf:about="&hthns;Theory">
- <rdfs:comment>Mathematical resources represented by theories</rdfs:comment>
- <rdfs:subClassOf rdf:resource="&hthns;MathResource"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdfs:Class>
-
-<rdfs:Class rdf:about="&hthns;TheoryItem">
- <rdfs:comment>Theory items represented by: axiom, fact, definition, theorem, lemma, corollary, variable, specified by a XPath expression</rdfs:comment>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdfs:Class>
-
-<rdfs:Class rdf:about="&hthns;Contact">
- <rdfs:comment>Creator contact information</rdfs:comment>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdfs:Class>
-
-<!-- Subclass of dct:Text and dct:Software -->
-
-<!-- Non necessario: uso direttamente la MathResource interessata per non
-intendere implicitamente le stesse entita' (introduco cicli espliciti). -->
-<!--<rdfs:Class rdf:about="&hthns;HelmURI">
- <rdfs:comment>HELM URIs of a mathematical resource. Subclass of dcq:URI
-which is an instance of the IdentifierScheme class</rdfs:comment>
- <rdfs:subClassOf rdf:resource="&dcqns;URI"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdfs:Class>-->
-
-<rdfs:Class rdf:about="&hthns;HELMText">
- <rdfs:comment>HELM File text types of a mathematical resource (possible
-values of the Dublin Core property type). Possible values of the rdf:about
-attribute can be: Abstract, Paper, Bibliography, HomePage, LectureNotes,
-Monograph, PatentSpec, Preprints, Proceedings, Review, Separatum, Serial,
-TechReport, Thesis, Enclosure, General. General describes a document not of
-the previous types. A helm theory has no type per se. Subclass of dcq:Text
-which is an instance of the TypeScheme class</rdfs:comment>
- <rdfs:subClassOf rdf:resource="&dctns;Text"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdfs:Class>
-
-<rdfs:Class rdf:about="&hthns;HELMSoftware">
- <rdfs:comment>HELM File software types of a mathematical resource
-(possible values of the Dublin Core property type). Possible values of the
-rdf:about attribute can be: Exec, Source. Subclass of dcq:Software
-which is an instance of the TypeScheme class</rdfs:comment>
- <rdfs:subClassOf rdf:resource="&dctns;Software"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdfs:Class>
-
-<!-- Instances of dcq:FormatScheme and dcq:IdentifierScheme -->
-<!-- Instances are only for typing classes not for using. -->
-
-<dcq:FormatScheme rdf:about="&hthns;HelmFormat">
- <rdfs:comment>Instance of the class FormatScheme to describe HELM File
-formats of a mathematical resource (possible values of the Dublin Core property
-format). Possible values of the 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>
- <rdf:type rdf:resource="&rdfsns;Class"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</dcq:FormatScheme>
-
-<dcq:IdentifierScheme rdf:about="&hthns;HelmID">
- <rdfs:comment>Instance of the class IdentifierScheme to describe HELM
-identifiers</rdfs:comment>
- <rdf:type rdf:resource="&rdfsns;Class"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</dcq:IdentifierScheme>
-
-<!-- SubProperties of dc:description, dc:creator, dc:relation and
- hth:dependence -->
-
-<!-- SubProperty of dc:title -->
-<rdf:Property rdf:about="&hthns;shortName">
- <rdfs:comment>Short name (alias) of the mathematical resource</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="&dcns;title"/>
- <rdfs:domain rdf:resource="&hthns;MathResource"/>
- <rdfs:range rdf:resource="&xschemans;string"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-
-<!-- There are also dcq:created and dcq:modified dc:date subProperties -->
-<rdf:Property rdf:ID="firstVersion">
- <rdfs:comment>Any additional information about the first version of the
-mathematical resource</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="&dcns;description"/>
- <rdfs:domain rdf:resource="#MathResource"/>
- <rdfs:range rdf:resource="&xschemans;string"/>
-</rdf:Property>
-
-<rdf:Property rdf:ID="modified">
- <rdfs:comment>Any additional information about the modified version of the
-mathematical resource</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="&dcns;description"/>
- <rdfs:domain rdf:resource="#MathResource"/>
- <rdfs:range rdf:resource="&xschemans;string"/>
-</rdf:Property>
-
-<rdf:Property rdf:about="&hthns;institution">
- <rdfs:comment>Affiliated institution of the creator of the mathematical
-resource</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="&dcns;creator"/>
- <rdfs:domain rdf:resource="&hthns;MathResource"/>
- <rdfs:range rdf:resource="&xschemans;string"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:about="&hthns;contact">
- <rdfs:comment>Contact of the creator of the mathematical
-resource</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="&dcns;creator"/>
- <rdfs:domain rdf:resource="&hthns;MathResource"/>
- <rdfs:range rdf:resource="#Contact"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:about="&hthns;isBasedOn">
- <rdfs:comment>A relation between mathematical resources</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
- <rdfs:domain rdf:resource="&hthns;MathResource"/>
- <rdfs:range rdf:resource="&hthns;MathResource"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:about="&hthns;isBasisFor">
- <rdfs:comment>A relation between mathematical resources</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
- <rdfs:domain rdf:resource="&hthns;MathResource"/>
- <rdfs:range rdf:resource="&hthns;MathResource"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:about="&hthns;isSourceFor">
- <rdfs:comment>A relation between mathematical resources</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
- <rdfs:domain rdf:resource="&hthns;MathResource"/>
- <rdfs:range rdf:resource="&hthns;MathResource"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:about="&hthns;hasSource">
- <rdfs:comment>A relation between mathematical resources</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="&dcns;relation"/>
- <rdfs:domain rdf:resource="&hthns;MathResource"/>
- <rdfs:range rdf:resource="&hthns;MathResource"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:about="&hthns;uses">
- <rdfs:comment>A dependence between theory items (for instance: between a theorem or anything else and a variable)</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="&hthns;dependence"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:about="&hthns;isUsedBy">
- <rdfs:comment>A dependence between theory items (for instance: between a variable and
-a theorem or anything else)</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="&hthns;dependence"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:about="&hthns;hasConsequence">
- <rdfs:comment>A dependence between theory items (for instance: between a theorem and
-a corollary)</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="&hthns;dependence"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:about="&hthns;isConsequenceOf">
- <rdfs:comment>A dependence between theory items (for instance: between a corollary
-and a theorem). Alternatively: IsResultOf</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="&hthns;dependence"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:about="&hthns;hasPremise">
- <rdfs:comment>A dependence between theory items (for instance: between a theorem
-and a lemma)</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="&hthns;dependence"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:about="&hthns;isPremiseOf">
- <rdfs:comment>A dependence between theory items (for instance: between a lemma
-and a theorem)</rdfs:comment>
- <rdfs:subPropertyOf rdf:resource="&hthns;dependence"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<!-- Properties -->
-
-<rdf:Property rdf:about="&hthns;theoryItem">
- <rdfs:comment>Theory item</rdfs:comment>
- <rdfs:domain rdf:resource="&hthns;Theory"/>
- <rdfs:range rdf:resource="&hthns;TheoryItem"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:about="&hthns;dependence">
- <rdfs:comment>Dependence between theory items</rdfs:comment>
- <rdfs:domain rdf:resource="&hthns;TheoryItem"/>
- <rdfs:range rdf:resource="&hthns;HelmID"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:about="&hthns;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="&hthns;TheoryItem"/>
- <rdfs:range rdf:resource="&xschemans;string"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:about="&hthns;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="&hthns;TheoryItem"/>
- <rdfs:range rdf:resource="&xschemans;string"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<!-- ex. f:N->Z => N>->Z and n:Nat => n:Z -->
-<rdf:Property rdf:about="&hthns;isCoercion">
- <rdfs:comment>A Definition item can be a coercion</rdfs:comment>
- <rdfs:domain rdf:resource="&hthns;TheoryItem"/>
- <rdfs:range rdf:resource="&xschemans;boolean"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</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:about="&hthns;ident">
- <rdfs:comment>Identifier of a theory item</rdfs:comment>
- <rdfs:domain rdf:resource="&hthns;TheoryItem"/>
- <rdfs:range rdf:resource="&hthns;HelmID"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:about="&hthns;email">
- <rdfs:comment>E-mail of the creator of the mathematical
-resource</rdfs:comment>
- <rdfs:domain rdf:resource="&hthns;Contact"/>
- <rdfs:range rdf:resource="&xschemans;string"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<rdf:Property rdf:about="&hthns;address">
- <rdfs:comment>Address of the creator of the mathematical
-resource</rdfs:comment>
- <rdfs:domain rdf:resource="&hthns;Contact"/>
- <rdfs:range rdf:resource="&xschemans;string"/>
- <rdfs:isDefinedBy rdf:resource = "&hthns;" />
-</rdf:Property>
-
-<!-- HELM: Constraining an external (dc) property to a particular range and
-domain (hth:MathResource) should be possible. VRP gives a Warning when
-constraining (extending, adding constraints to) the range of a property
-defined in another schema (Consistency problems?No because it's an error
-modifying the original constraints): but where is the extensibility and
-reusability of RDF schemas? It's ok specializing a property with a
-subProperty. Anyway if the range of a property is not defined, VRP validates
-both if the property value is a resource, a class or a Literal.
-<rdf:Description rdf:about = "&dcns;type">
- <rdfs:domain rdf:resource="&hthns;MathResource"/>
-</rdf:Description> -->
-
-</rdf:RDF>
projects / helm.git / blobdiff