X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fschemas%2Fschema-hth;fp=helm%2Fschemas%2Fschema-hth;h=0000000000000000000000000000000000000000;hp=10e20c08308f1dad0aaaa609b4d4ad11e53313ad;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1 diff --git a/helm/schemas/schema-hth b/helm/schemas/schema-hth deleted file mode 100644 index 10e20c083..000000000 --- a/helm/schemas/schema-hth +++ /dev/null @@ -1,323 +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 - - - - 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 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 - - - - - - - - - Short name (alias) of the mathematical resource - - - - - - - - - - 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 - - - - - - - -