From: Irene Schena Date: Mon, 10 Dec 2001 16:28:04 +0000 (+0000) Subject: ---------------------------------------------------------------------- X-Git-Tag: mlminidom_0_2_2~13 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b585030cb67e164ec9a043abcd938be756d9ad1f;p=helm.git ---------------------------------------------------------------------- Modified Files: 1) schema-h.rdf, schema-hth.rdf: updated DC schemas + class and property refinements + value types. ---------------------------------------------------------------------- --- diff --git a/helm/schemas/schema-h.rdf b/helm/schemas/schema-h.rdf index 7a8c1046c..ce2d8ed2e 100644 --- a/helm/schemas/schema-h.rdf +++ b/helm/schemas/schema-h.rdf @@ -3,10 +3,19 @@ + + + + + ]> + + xmlns:rdf="&rdfns;" + xmlns:rdfs="&rdfsns;" + xmlns:hth="&hthns;" + xmlns:xs="&xschemans;"> + @@ -22,14 +31,14 @@ da parsare --> Mathematical object represented by a CIC XML file - + Mathematical resource (directory) represented by a set of CIC XML files, contained in the tree that has the dir as root - + @@ -44,6 +53,10 @@ CIC XML files, contained in the tree that has the dir as root Occurrence of an object inside an object + + Position of an occurrence of an object inside an object + + Additional information associated to fragments of the objects @@ -64,36 +77,36 @@ CIC XML files, contained in the tree that has the dir as root Implicit arguments - + Occurrence of an object in head position of some hypothesis of an object statement - + Occurrence of an object in the hypotheses of an object statement - + Occurrence of an object in head position of the conclusion of an object statement - + Occurrence of an object in the conclusion of an object statement - + Occurrence of an object only in an object body (not in the statement) - + @@ -115,14 +128,14 @@ CIC XML files, contained in the tree that has the dir as root - + List of all ids in the domain - + @@ -151,7 +164,7 @@ CIC XML files, contained in the tree that has the dir as root List of implicit arguments - + @@ -160,6 +173,19 @@ CIC XML files, contained in the tree that has the dir as root + + URI of an object + + + + + + Position of an occurrence + + + + + Postit @@ -169,14 +195,14 @@ CIC XML files, contained in the tree that has the dir as root Content of a Postit - + Identifies the object fragment (Xpointer) which Postit refers to - - + + diff --git a/helm/schemas/schema-hth.rdf b/helm/schemas/schema-hth.rdf index 6953b0e5a..110bf62fd 100644 --- a/helm/schemas/schema-hth.rdf +++ b/helm/schemas/schema-hth.rdf @@ -3,10 +3,20 @@ + + + + + + ]> + + xmlns:rdf="&rdfns;" + xmlns:rdfs="&rdfsns;" + xmlns:dc="&dcns;" + xmlns:dcq="&dcqns;" + xmlns:xs="&xschemans;"> @@ -18,7 +28,7 @@ xmlns:hth="http://www.cs.unibo.it/~schena/schema-hth.rdf#" --> Mathematical resource - + @@ -30,43 +40,53 @@ xmlns:hth="http://www.cs.unibo.it/~schena/schema-hth.rdf#" --> Theory item represented by: axiom, fact, definition, theorem, lemma, corollary, variable, specified by a XPath expression - - File format of a mathematical resource (possible values of the -Dublin Core property Format) + + 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. + + + + + HELM URI of a mathematical resource + + + + HELM identifier - - Type of mathematical resource (possible values of the Dublin Core -property Type) + + Creator contact information - + - + A relation between mathematical resources - + - + A relation between mathematical resources - + - + A relation between mathematical resources - + - + A relation between mathematical resources @@ -107,124 +127,14 @@ and a lemma) and a theorem) - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + @@ -235,14 +145,14 @@ and a theorem) - + Axiom, Fact, Definition, Theorem, Lemma, Corollary, Variable. Redundant info: it is already captured by the corresponding xml data - + @@ -250,58 +160,54 @@ Variable. Redundant info: it is already captured by the corresponding xml data - + A Definition item can be a coercion - + - + + + - + + - + - - - + + + - - - + + + - - - - + + - - - - -