From: Irene Schena Date: Mon, 3 Dec 2001 16:17:59 +0000 (+0000) Subject: ---------------------------------------------------------------------- X-Git-Tag: mlminidom_0_2_2~33 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9d25a028a1ec3f0331d417b7c0b648e8c5d622a3;p=helm.git ---------------------------------------------------------------------- Added Files: 1) schema-h.rdf, schema-hth.rdf: first draft of rdf schemas for objects and theories ---------------------------------------------------------------------- --- diff --git a/helm/schemas/schema-h.rdf b/helm/schemas/schema-h.rdf new file mode 100644 index 000000000..7a8c1046c --- /dev/null +++ b/helm/schemas/schema-h.rdf @@ -0,0 +1,190 @@ + + + + + + + + + + + + + + + + + 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 + + + + + Type of the object + + + + Term of the object + + + + Occurrence of an object inside an object + + + + Additional information associated to fragments of the objects + + + + Constant in the body of an object + + + + Ids in the statement + + + + Ids in the body + + + + 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) + + + + + + + + + + + + + + + + + + + + + + + + + + + List of all ids in the domain + + + + + + + + + + + + Reference to an object + + + + + + Implicit arguments of constructors + + + + + + Implicit arguments of objects + + + + + + List of implicit arguments + + + + + + Backwards pointer: who points the object + + + + + + Postit + + + + + + 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 new file mode 100644 index 000000000..6953b0e5a --- /dev/null +++ b/helm/schemas/schema-hth.rdf @@ -0,0 +1,314 @@ + + + + + + + + + + + + + + + + Mathematical resource + + + + + Mathematical resource represented by a theory + + + + + 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) + + + + Type of mathematical resource (possible values of the Dublin Core +property Type) + + + + + + + + + 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) + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 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 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +