From: Irene Schena Date: Fri, 6 Sep 2002 16:05:58 +0000 (+0000) Subject: Added Files: X-Git-Tag: BEFORE_METADATA_FOR_SORT_AND_REL~85 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=71c844edbf4d0c6eeafd10931aceb3f9f8ff5136;p=helm.git Added Files: 1)schema-h schema-hth: new versions Removed Files: 1)schema-h.rdf schema-hth.rdf: old versions --- diff --git a/helm/schemas/schema-h b/helm/schemas/schema-h new file mode 100644 index 000000000..151debbc1 --- /dev/null +++ b/helm/schemas/schema-h @@ -0,0 +1,264 @@ + + + + + + + + + + + + ]> + + + + + + + + + The HELM Element Set v0.1 + The HELM Object Element Set v0.1 + The HELM Project + The HELM metadata vocabulary is a simple vocabulary + intended to facilitate discovery of mathematical resources. + + English + + + + 2000-6-3 + 2002-9-6 + + + + + + + + Mathematical objects represented by a CIC XML +file + + + + + + + Mathematical resources (directories) represented by sets +of CIC XML files, contained in the tree that has the dir as root + + + + + + Types of objects + + + + + Terms of objects + + + + + Occurrences of an object inside an object + + + + + Positions of occurrences of an object inside an object + + + + + Additional information associated to fragments of the objects + + + + + Constants in the body of an object + + + + + Identifiers in the statement + + + + + Identifiers in the body + + + + + Implicit arguments + + + + + + + Occurrences of an object in head position of some hypothesis + of an object statement + + + + + + Occurrences of an object in the hypotheses of an object + statement + + + + + + Occurrences of an object in head position of the + conclusion of an object statement + + + + + + Occurrences of an object in the conclusion of an object + statement + + + + + + Occurrences of an object only in an object body (not in the + statement) + + + + + + + + Statement + + + + + + + Body + + + + + + + Statement identifier + + + + + + + Constructor identifier of the statement conclusion + + + + + + + List of all ids in the domain + + + + + + + + Body identifier + + + + + + + Reference to an object + + + + + + + Implicit arguments of constructors + + + + + + + Implicit arguments of objects + + + + + + + List of implicit arguments + + + + + + + Backwards pointer: who points the object + + + + + + + URI of an object + + + + + + + Position of an occurrence + + + + + + + + Postit + + + + + + + Content of a Postit + + + + + + + Identifies the object fragment (Xpointer) which Postit +refers to + + + + + + \ No newline at end of file diff --git a/helm/schemas/schema-h.rdf b/helm/schemas/schema-h.rdf deleted file mode 100644 index 395eb925c..000000000 --- a/helm/schemas/schema-h.rdf +++ /dev/null @@ -1,257 +0,0 @@ - - - - - - - - - - - ]> - - - - - - - - - The HELM Element Set v0.1 - The HELM Object Element Set v0.1 - The HELM Project - The HELM metadata vocabulary is a simple vocabulary - intended to facilitate discovery of mathematical resources. - - English - - 2001-12-12 - - - - - - - Mathematical objects represented by a CIC XML -file - - - - - - - Mathematical resources (directories) represented by sets -of CIC XML files, contained in the tree that has the dir as root - - - - - - Types of objects - - - - - Terms of objects - - - - - Occurrences of an object inside an object - - - - - Positions of occurrences of an object inside an object - - - - - Additional information associated to fragments of the objects - - - - - Constants in the body of an object - - - - - Identifiers in the statement - - - - - Identifiers in the body - - - - - Implicit arguments - - - - - - - Occurrences of an object in head position of some hypothesis - of an object statement - - - - - - Occurrences of an object in the hypotheses of an object - statement - - - - - - Occurrences of an object in head position of the - conclusion of an object statement - - - - - - Occurrences of an object in the conclusion of an object - statement - - - - - - Occurrences of an object only in an object body (not in the - statement) - - - - - - - - Statement - - - - - - - Body - - - - - - - Statement identifier - - - - - - - Constructor identifier of the statement conclusion - - - - - - - List of all ids in the domain - - - - - - - - Body identifier - - - - - - - Reference to an object - - - - - - - Implicit arguments of constructors - - - - - - - Implicit arguments of objects - - - - - - - List of implicit arguments - - - - - - - Backwards pointer: who points the object - - - - - - - URI of an object - - - - - - - Position of an occurrence - - - - - - - - Postit - - - - - - - Content of a Postit - - - - - - - Identifies the object fragment (Xpointer) which Postit -refers to - - - - - - \ No newline at end of file diff --git a/helm/schemas/schema-hth b/helm/schemas/schema-hth new file mode 100644 index 000000000..cd1e8fe28 --- /dev/null +++ b/helm/schemas/schema-hth @@ -0,0 +1,311 @@ + + + + + + + + + + + + + ]> + + + + + + + + + + The HELM Element Set v0.1 + The HELM Theory Element Set v0.1 + The HELM Project + The HELM metadata vocabulary is a simple vocabulary + intended to facilitate discovery of mathematical resources. + + English + + + + 2000-6-3 + 2002-9-6 + + + + + + + + Mathematical resources + + + + + + Mathematical resources represented by theories + + + + + + Theory items represented by: axiom, fact, definition, theorem, lemma, corollary, variable, specified by a XPath expression + + + + + Creator contact information + + + + + + + HELM URIs of a mathematical resource. Subclass of dcq:URI +which is an instance of the IdentifierScheme class + + + + + + 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 + + + + + + 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 + + + + + + + + + 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. + + + + + + Instance of the class IdentifierScheme to describe HELM +identifiers + + + + + + + + + Any additional information about the first version of the +mathematical resource + + + + + + + Any additional information about the modified version of the +mathematical resource + + + + + + + Affiliated institution of the creator of the mathematical +resource + + + + + + + + Contact of the creator of the mathematical +resource + + + + + + + + A relation between mathematical resources + + + + + + + + A relation between mathematical resources + + + + + + + + A relation between mathematical resources + + + + + + + + A relation between mathematical resources + + + + + + + + A dependence between theory items (for instance: between a theorem or anything else and a variable) + + + + + + A dependence between theory items (for instance: between a variable and +a theorem or anything else) + + + + + + A dependence between theory items (for instance: between a theorem and +a corollary) + + + + + + A dependence between theory items (for instance: between a corollary +and a theorem). Alternatively: IsResultOf + + + + + + A dependence between theory items (for instance: between a theorem +and a lemma) + + + + + + A dependence between theory items (for instance: between a lemma +and a theorem) + + + + + + + + Theory item + + + + + + + Dependence between theory items + + + + + + + Axiom, Fact, Definition, Theorem, Lemma, Corollary, +Variable. Redundant info: it is already captured by the corresponding xml data + + + + + + + Description of the kind of objects: data type, +algorithm, specification, theorem containing algorithm, verification (that the +implementation satisfies the specification), predicate/relation, proposition + + + + + + + + A Definition item can be a coercion + + + + + + + + Identifier of a theory item + + + + + + + E-mail of the creator of the mathematical +resource + + + + + + + Address of the creator of the mathematical +resource + + + + + + + + diff --git a/helm/schemas/schema-hth.rdf b/helm/schemas/schema-hth.rdf deleted file mode 100644 index 6c54ff916..000000000 --- a/helm/schemas/schema-hth.rdf +++ /dev/null @@ -1,280 +0,0 @@ - - - - - - - - - - - ]> - - - - - - - - - - The HELM Element Set v0.1 - The HELM Theory Element Set v0.1 - The HELM Project - The HELM metadata vocabulary is a simple vocabulary - intended to facilitate discovery of mathematical resources. - - English - - 2001-12-12 - - - - - - - Mathematical resources - - - - - - Mathematical resources represented by theories - - - - - - Theory items represented by: axiom, fact, definition, theorem, lemma, corollary, variable, specified by a XPath expression - - - - - 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. - - - - - - HELM URIs of a mathematical resource - - - - - - HELM identifiers - - - - - Creator contact information - - - - - - - A relation between mathematical resources - - - - - - - - A relation between mathematical resources - - - - - - - - A relation between mathematical resources - - - - - - - - A relation between mathematical resources - - - - - - - - - - A dependence between theory items (for instance: between a theorem or anything else and a variable) - - - - - - A dependence between theory items (for instance: between a variable and -a theorem or anything else) - - - - - - A dependence between theory items (for instance: between a theorem and -a corollary) - - - - - - A dependence between theory items (for instance: between a corollary -and a theorem). Alternatively: IsResultOf - - - - - - A dependence between theory items (for instance: between a theorem -and a lemma) - - - - - - A dependence between theory items (for instance: between a lemma -and a theorem) - - - - - - - - - - - - - Theory item - - - - - - - Dependence between theory items - - - - - - - Axiom, Fact, Definition, Theorem, Lemma, Corollary, -Variable. Redundant info: it is already captured by the corresponding xml data - - - - - - - Description of the kind of objects: data type, -algorithm, specification, theorem containing algorithm, verification (that the -implementation satisfies the specification), predicate/relation, proposition - - - - - - - - A Definition item can be a coercion - - - - - - - - Identifier of a theory item - - - - - - - - Any additional information about the first version of the -mathematical resource - - - - - - - Any additional information about the modified version of the -mathematical resource - - - - - - - Affiliated institution of the creator of the mathematical -resource - - - - - - - - Contact of the creator of the mathematical -resource - - - - - - - - E-mail of the creator of the mathematical -resource - - - - - - - Address of the creator of the mathematical -resource - - - - - - - - - -