----------------------------------------------------------------------

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 (file)
index 0000000..7a8c104
--- /dev/null
+++ b/helm/schemas/schema-h.rdf
@@ -0,0 +1,190 @@
+<?xml version="1.0"?>
+
+<!-- Rdf Schema definition for CIC XML files:
+xmlns:h="http://www.cs.unibo.it/~schena/schema-h.rdf#" -->
+
+<rdf:RDF xml:lang="en"
+       xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+       xmlns:rdfs="http://www.w3.org/2000/01/rdf-schema#"
+       xmlns:hth="http://www.cs.unibo.it/~schena/schema-hth.rdf#">
+
+<!-- RICORDA: aggiungi commento anche a proprieta' e istanze -->
+<!-- RICORDA: studiare tipi di dato (invece di Literal) -->
+<!-- RICORDA: specificare i contenuti dei dc elements -->
+<!-- RICORDA: aggiungi euler properties -->
+<!-- RICORDA: metadati solo su oggetto (come teoria ma piu' specifici) (non 
+distinzione tipi di body) e non ridondanze se non riducono il numero di doc 
+da parsare  -->
+<!-- RICORDA: definire soprattutto i metadati da inserire a mano -->
+
+<!-- Classes -->
+
+<rdfs:Class rdf:ID="Object">
+     <rdfs:comment>Mathematical object represented by a CIC XML 
+file</rdfs:comment>
+     <rdfs:subClassOf rdf:resource="http://www.cs.unibo.it/~schena/schema-hth.rdf#MathResource"/>
+</rdfs:Class>
+
+<!-- Objects can inherit its dc properties -->
+<rdfs:Class rdf:ID="DirectoryOfObjects">
+     <rdfs:comment>Mathematical resource (directory) represented by a set of 
+CIC XML files, contained in the tree that has the dir as root </rdfs:comment>
+     <rdfs:subClassOf rdf:resource="http://www.cs.unibo.it/~schena/schema-hth.rdf#MathResource"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Statement">
+     <rdfs:comment>Type of the object</rdfs:comment>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Body">
+     <rdfs:comment>Term of the object</rdfs:comment>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Occurrence">
+     <rdfs:comment>Occurrence of an object inside an object</rdfs:comment>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Postit">
+     <rdfs:comment>Additional information associated to fragments of the objects</rdfs:comment>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Const">
+     <rdfs:comment>Constant in the body of an object</rdfs:comment>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="StatementId">
+     <rdfs:comment>Ids in the statement</rdfs:comment>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="BodyId">
+     <rdfs:comment>Ids in the body</rdfs:comment>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="ImplArg">
+     <rdfs:comment>Implicit arguments</rdfs:comment>
+</rdfs:Class>
+
+<!-- Instances of the class h:Occurrence -->
+
+<rdfs:Class rdf:ID="MainHypothesis">
+    <rdfs:comment>Occurrence of an object in head position of some hypothesis 
+     of an object statement</rdfs:comment>
+    <rdf:type rdf:resource="#Occurrence"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="InHypothesis">
+    <rdfs:comment>Occurrence of an object in the hypotheses of an object 
+     statement</rdfs:comment>
+    <rdf:type rdf:resource="#Occurrence"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="MainConclusion">
+    <rdfs:comment>Occurrence of an object in head position of the 
+     conclusion of an object statement</rdfs:comment>
+    <rdf:type rdf:resource="#Occurrence"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="InConclusion">
+    <rdfs:comment>Occurrence of an object in the conclusion of an object
+     statement</rdfs:comment>  
+    <rdf:type rdf:resource="#Occurrence"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="InBody">
+    <rdfs:comment>Occurrence of an object only in an object body (not in the 
+     statement)</rdfs:comment>
+    <rdf:type rdf:resource="#Occurrence"/>
+</rdfs:Class>
+
+<!-- Properties -->
+
+<rdf:Property rdf:ID="statement">
+    <rdfs:domain rdf:resource="#Object"/>
+    <rdfs:range rdf:resource="#Statement"/>
+</rdf:Property>
+
+<rdf:Property rdf:ID="body">
+    <rdfs:domain rdf:resource="#Object"/>
+    <rdfs:range rdf:resource="#Body"/>
+</rdf:Property>
+
+<rdf:Property rdf:ID="statementId">
+    <rdfs:domain rdf:resource="#Statement"/>
+    <rdfs:range rdf:resource="#StatementId"/>
+</rdf:Property>
+
+<rdf:Property rdf:ID="constrId">
+    <rdfs:domain rdf:resource="#StatementId"/>
+    <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+</rdf:Property>
+
+<rdf:Property rdf:ID="listId">
+    <rdfs:comment>List of all ids in the domain</rdfs:comment>
+    <rdfs:domain rdf:resource="#StatementId"/>
+    <rdfs:domain rdf:resource="#BodyId"/>
+    <rdfs:range rdf:resource="http://www.w3.org/1999/02/22-rdf-syntax-ns#Seq"/>
+</rdf:Property>
+
+<rdf:Property rdf:ID="bodyId">
+    <rdfs:domain rdf:resource="#Body"/>
+    <rdfs:range rdf:resource="#BodyId"/>
+</rdf:Property>
+
+<rdf:Property rdf:ID="refObj">
+    <rdfs:comment>Reference to an object</rdfs:comment>
+    <rdfs:domain rdf:resource="#Object"/>
+    <rdfs:range rdf:resource="#Occurrence"/>
+</rdf:Property>
+
+<rdf:Property rdf:ID="constrImplArg">
+    <rdfs:comment>Implicit arguments of constructors</rdfs:comment>
+    <rdfs:domain rdf:resource="#Statement"/>
+    <rdfs:range rdf:resource="#ImplArg"/>
+</rdf:Property>
+
+<rdf:Property rdf:ID="objImplArg">
+    <rdfs:comment>Implicit arguments of objects</rdfs:comment>
+    <rdfs:domain rdf:resource="#Object"/>
+    <rdfs:range rdf:resource="#ImplArg"/>
+</rdf:Property>
+
+<rdf:Property rdf:ID="listImplArg">
+    <rdfs:comment>List of implicit arguments</rdfs:comment>
+    <rdfs:domain rdf:resource="#ImplArg"/>
+    <rdfs:range rdf:resource="http://www.w3.org/1999/02/22-rdf-syntax-ns#Seq"/>
+</rdf:Property>
+
+<rdf:Property rdf:ID="backPointer">
+    <rdfs:comment>Backwards pointer: who points the object</rdfs:comment>
+    <rdfs:domain rdf:resource="#Object"/>
+    <rdfs:range rdf:resource="#Occurrence"/>
+</rdf:Property>
+
+<rdf:Property rdf:ID="postit">
+    <rdfs:comment>Postit</rdfs:comment>
+    <rdfs:domain rdf:resource="#Object"/>
+    <rdfs:range rdf:resource="#Postit"/>
+</rdf:Property>
+
+<rdf:Property rdf:ID="content">
+    <rdfs:comment>Content of a Postit</rdfs:comment>
+    <rdfs:domain rdf:resource="#Postit"/>
+    <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+</rdf:Property>
+
+<rdf:Property rdf:ID="refersTo">
+    <rdfs:comment>Identifies the object fragment (Xpointer) which Postit
+refers to</rdfs:comment>
+    <rdfs:domain rdf:resource="#Postit"/>
+    <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+</rdf:Property>
+
+</rdf:RDF>
+
+
+
+
+
+
+
+

diff --git a/helm/schemas/schema-hth.rdf b/helm/schemas/schema-hth.rdf
new file mode 100644 (file)
index 0000000..6953b0e
--- /dev/null
+++ b/helm/schemas/schema-hth.rdf
@@ -0,0 +1,314 @@
+<?xml version="1.0"?>
+
+<!-- Rdf Schema definition for theory files:
+xmlns:hth="http://www.cs.unibo.it/~schena/schema-hth.rdf#" -->
+
+<rdf:RDF xml:lang="en"
+       xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+       xmlns:rdfs="http://www.w3.org/2000/01/rdf-schema#"
+       xmlns:dc="http://www.cs.unibo.it/~schena/dublin_core.rdf#">
+
+<!-- RICORDA: aggiungi commento anche a proprieta' e istanze -->
+<!-- RICORDA: studiare tipi di dato (invece di Literal) -->
+<!-- RICORDA: specificare i contenuti dei dc elements -->
+<!-- RICORDA: verifica formato xml.helm.cic  -->
+<!-- RICORDA: aggiungi euler properties -->
+
+<!-- Classes -->
+
+<rdfs:Class rdf:ID="MathResource">
+     <rdfs:comment>Mathematical resource</rdfs:comment>
+     <rdfs:subClassOf rdf:resource="http://www.w3.org/2000/01/rdf-schema#Resource"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Theory">
+     <rdfs:comment>Mathematical resource represented by a theory</rdfs:comment>
+     <rdfs:subClassOf rdf:resource="#MathResource"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="TheoryItem">
+     <rdfs:comment>Theory item represented by: axiom, fact, definition, theorem, lemma, corollary, variable, specified by a XPath expression </rdfs:comment>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="ResourceFormat">
+     <rdfs:comment>File format of a mathematical resource (possible values of the 
+Dublin Core property Format)</rdfs:comment>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="ResourceType">
+     <rdfs:comment>Type of mathematical resource (possible values of the Dublin Core
+property Type)</rdfs:comment>
+</rdfs:Class>
+
+<!-- Added subProperties of the Property dc:relation -->
+
+<rdf:Property rdf:ID="isBasedOn">
+    <rdfs:subPropertyOf rdf:resource="http://www.cs.unibo.it/~schena/dublin_core.rdf#relation"/>
+    <rdfs:domain rdf:resource="#MathResource"/>
+    <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+    <rdfs:comment>A relation between mathematical resources</rdfs:comment>
+</rdf:Property>
+
+<rdf:Property rdf:ID="isBasisFor">
+    <rdfs:subPropertyOf rdf:resource="http://www.cs.unibo.it/~schena/dublin_core.rdf#relation"/>
+    <rdfs:domain rdf:resource="#MathResource"/>
+    <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+    <rdfs:comment>A relation between mathematical resources</rdfs:comment>
+</rdf:Property>
+
+<rdf:Property rdf:ID="isSourceFor">
+    <rdfs:subPropertyOf rdf:resource="http://www.cs.unibo.it/~schena/dublin_core.rdf#relation"/>
+    <rdfs:domain rdf:resource="#MathResource"/>
+    <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+    <rdfs:comment>A relation between mathematical resources</rdfs:comment>
+</rdf:Property>
+
+<rdf:Property rdf:ID="hasSource">
+    <rdfs:subPropertyOf rdf:resource="http://www.cs.unibo.it/~schena/dublin_core.rdf#relation"/>
+    <rdfs:domain rdf:resource="#MathResource"/>
+    <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+    <rdfs:comment>A relation between mathematical resources</rdfs:comment>
+</rdf:Property>
+
+<!--  subProperties of Property hth:dependence -->
+
+<rdf:Property rdf:ID="uses">
+    <rdfs:subPropertyOf rdf:resource="#dependence"/>
+    <rdfs:comment>A dependence between theory items (for instance: between a theorem or anything else and a variable)</rdfs:comment>
+</rdf:Property>
+
+<rdf:Property rdf:ID="isUsedBy">
+    <rdfs:subPropertyOf rdf:resource="#dependence"/>
+    <rdfs:comment>A dependence between theory items (for instance: between a variable and
+a theorem or anything else)</rdfs:comment>
+</rdf:Property>
+
+<rdf:Property rdf:ID="hasConsequence">
+    <rdfs:subPropertyOf rdf:resource="#dependence"/>
+    <rdfs:comment>A dependence between theory items (for instance: between a theorem and
+a corollary)</rdfs:comment>
+</rdf:Property>
+
+<rdf:Property rdf:ID="isConsequenceOf">
+    <rdfs:subPropertyOf rdf:resource="#dependence"/>
+    <rdfs:comment>A dependence between theory items (for instance: between a corollary
+and a theorem). Alternatively: IsResultOf</rdfs:comment>
+</rdf:Property>
+
+<rdf:Property rdf:ID="hasPremise">
+    <rdfs:subPropertyOf rdf:resource="#dependence"/>
+    <rdfs:comment>A dependence between theory items (for instance: between a theorem
+and a lemma)</rdfs:comment>
+</rdf:Property>
+
+<rdf:Property rdf:ID="isPremiseOf">
+    <rdfs:subPropertyOf rdf:resource="#dependence"/>
+    <rdfs:comment>A dependence between theory items (for instance: between a lemma
+and a theorem)</rdfs:comment>
+</rdf:Property>
+
+<!-- Text.general describes a document not of the following types. -->
+<!-- A helm theory has no type per se                              -->
+<!-- Instances of hth:ResourceType -->
+
+<rdfs:Class rdf:ID="Text.Abstract">
+    <rdf:type rdf:resource="#ResourceType"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Text.Paper">
+    <rdf:type rdf:resource="#ResourceType"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Text.Bibliography">
+    <rdf:type rdf:resource="#ResourceType"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Text.HomePage">
+    <rdf:type rdf:resource="#ResourceType"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Text.LectureNotes">
+    <rdf:type rdf:resource="#ResourceType"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Text.Monograph">
+    <rdf:type rdf:resource="#ResourceType"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Text.PatentSpec">
+    <rdf:type rdf:resource="#ResourceType"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Text.Preprints">
+    <rdf:type rdf:resource="#ResourceType"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Text.Proceedings">
+    <rdf:type rdf:resource="#ResourceType"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Text.Review">
+    <rdf:type rdf:resource="#ResourceType"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Text.Separatum">
+    <rdf:type rdf:resource="#ResourceType"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Text.Serial">
+    <rdf:type rdf:resource="#ResourceType"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Text.TechReport">
+    <rdf:type rdf:resource="#ResourceType"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Text.Thesis">
+    <rdf:type rdf:resource="#ResourceType"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Text.Enclosure">
+    <rdf:type rdf:resource="#ResourceType"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Text.General">
+    <rdf:type rdf:resource="#ResourceType"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Image">
+    <rdf:type rdf:resource="#ResourceType"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Software.Exec">
+    <rdf:type rdf:resource="#ResourceType"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Software.Source">
+    <rdf:type rdf:resource="#ResourceType"/>
+</rdfs:Class>
+
+<!-- NOTE: each helm format describes a logical framework -->
+<!-- Instances of hth:ResourceFormat                      -->
+
+<rdfs:Class rdf:ID="Text.xml">
+    <rdf:type rdf:resource="#ResourceFormat"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Text.xhtml">
+    <rdf:type rdf:resource="#ResourceFormat"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Text.mml">
+    <rdf:type rdf:resource="#ResourceFormat"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Text.ps">
+    <rdf:type rdf:resource="#ResourceFormat"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Text.pdf">
+    <rdf:type rdf:resource="#ResourceFormat"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="Text.tex">
+    <rdf:type rdf:resource="#ResourceFormat"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="XML.helm.cic">
+    <rdf:type rdf:resource="#ResourceFormat"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="XML.helm.mizar">
+    <rdf:type rdf:resource="#ResourceFormat"/>
+</rdfs:Class>
+
+<rdfs:Class rdf:ID="XML.helm.hol">
+    <rdf:type rdf:resource="#ResourceFormat"/>
+</rdfs:Class>
+
+<!-- Properties -->
+
+<rdf:Property rdf:ID="theoryItem">
+    <rdfs:domain rdf:resource="#Theory"/>
+    <rdfs:range rdf:resource="#TheoryItem"/>
+</rdf:Property>
+
+<rdf:Property rdf:ID="dependence">
+    <rdfs:domain rdf:resource="#TheoryItem"/>
+    <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+</rdf:Property>
+
+<rdf:Property rdf:ID="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="#TheoryItem"/>
+    <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+</rdf:Property>
+
+<rdf:Property rdf:ID="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="#TheoryItem"/>
+    <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+</rdf:Property>
+
+<!-- ex. f:N->Z => N>->Z and n:Nat => n:Z -->
+<rdf:Property rdf:ID="isCoercion">
+    <rdfs:comment>A Definition item can be a coercion</rdfs:comment>
+    <rdfs:domain rdf:resource="#TheoryItem"/>
+    <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+</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:ID="ident">
+    <rdfs:domain rdf:resource="#TheoryItem"/>
+    <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+</rdf:Property>
+
+<rdf:Property rdf:ID="institution">
+    <rdfs:domain rdf:resource="#MathResource"/>
+    <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+</rdf:Property>
+
+<rdf:Property rdf:ID="contact">
+    <rdfs:domain rdf:resource="#MathResource"/>
+    <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+</rdf:Property>
+
+<rdf:Property rdf:ID="firstVersion">
+    <rdfs:domain rdf:resource="#MathResource"/>
+    <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+</rdf:Property>
+
+<rdf:Property rdf:ID="modified">
+    <rdfs:domain rdf:resource="#MathResource"/>
+    <rdfs:range rdf:resource="http://www.w3.org/2000/01/rdf-schema#Literal"/>
+</rdf:Property>
+
+<!-- ATTENZIONE: si dovrebbero generare constraint che il dominio delle 
+dc properties sia hth:MathResource e che il range sia strutturato. Ma per
+fare questo e' necessario definire NUOVE proprieta' (nuovo namespace) -->
+
+<rdf:Property rdf:ID="type">
+    <rdfs:subPropertyOf rdf:resource="http://www.cs.unibo.it/~schena/dublin_core.rdf#type"/>
+    <rdfs:domain rdf:resource="#MathResource"/>
+    <rdfs:range rdf:resource="#ResourceType"/>
+</rdf:Property>
+
+<rdf:Property rdf:ID="format">
+    <rdfs:subPropertyOf rdf:resource="http://www.cs.unibo.it/~schena/dublin_core.rdf#format"/>
+    <rdfs:domain rdf:resource="#MathResource"/>
+    <rdfs:range rdf:resource="#ResourceFormat"/>
+</rdf:Property>
+
+</rdf:RDF>
+
+
+
+
+
+
+
+