--- a/ontology/ProvenanceFormalModel.html	Fri Oct 07 14:25:28 2011 -0400
+++ b/ontology/ProvenanceFormalModel.html	Fri Oct 07 14:31:47 2011 -0400
@@ -705,7 +705,6 @@
          </a>
          <br>         
          <em>Example extension of PROV ontology in order to describe the crime file scenario</em>
-      </p>		
 	  </section>
 	</section>
 	<section> 
@@ -1208,13 +1207,15 @@
 	</section>
 	<section>
       <h2>Formal Semantics of the PROV Ontology</h2>
-      <p>The PROV ontology uses OWL2 as the ontology language, hence it supports a set of entailments based on the standard RDF semantics [[!RDF-MT]] and OWL2 semantics ([[!OWL2-DIRECT-SEMANTICS]], [[!OWL2-RDF-BASED-SEMANTICS]]). In this section, we describe these set of semantics as applied to the PROV ontology along with a set of constraints introduced in the PROV-DM [[PROV-DM]] that are provenance-specific. It is intended that provenance applications can leverage this normative description of the formal semantics of PROV ontology to support:
+      <p>The PROV ontology uses OWL2 as the ontology language, hence it supports a set of entailments based on the standard RDF semantics [[!RDF-MT]] and OWL2 semantics ([[!OWL2-DIRECT-SEMANTICS]], [[!OWL2-RDF-BASED-SEMANTICS]]). In this section, we describe these set of semantics as applied to the PROV ontology along with a set of constraints introduced in the PROV-DM [[PROV-DM]] that are provenance-specific. It is intended that provenance applications can leverage this normative description of the formal semantics of PROV ontology to support:</p>
 	<ul>
 		<li><b>Automated consistency checking </b>of provenance assertions (in RDF): Any RDF graph generated to represent provenance information using the PROV ontology as schema can be automatically checked for consistency using reasoning tool, such as FaCT++, Pellet, and Racer among others.</li>
 		<li><b>Inferencing</b>: Make implicit knowledge explicit from RDF-encoded provenance datasets using valid entailment rules</li>			
 	</ul>		
-      </p>
-	<section>
+	
+
+
+   <section>
 		<h3>RDF Semantics for PROV Ontology</h3>
 		<p> We briefly summarize the essential features of the RDF Semantics and refer to the RDF semantics [[!RDF-MT]] for the normative specification. The RDF Semantics uses model theory, with a notion of interpretation I defined over RDF (rdf-interpretation) or RDFS (rdfs-interpretation) vocabulary, for specifying the formal semantics of a RDF or RDFS graph [[!RDF-MT]]. The rdf-interpretation is an interpretation that satisfies a set of constraints called "<i>RDF semantic conditions</i>" and a set of "<i>RDF axiomatic triples</i>" (see Section 3.1 of RDF Semantics [[!RDF-MT]]). The rdfs-interpretation is defined over the additional terms in the RDFS vocabulary, including <i>rdfs:domain</i>, <i>rdfs:range</i>, <i>rdfs:Class</i>, <i>rdfs:subClassOf</i>, and <i>rdfs:subPropertyOf</i>. An rdfs-interpretation satisfies a set of constraints called "<i>RDFS semantic conditions</i>" and "<i>RDFS axiomatic triples</i>" (see Section 4.1 of RDFS Semantics  [[!RDF-MT]]).
 		</p>
@@ -1271,10 +1272,13 @@
 	</section>
 	<section>
 	<h3>Provenance-specific Entailments Supported by PROV Ontology</h3>
-	<p>The PROV-DM [[PROV-DM]] introduces a set of specific constraints applicable to PROV ontology. The following is a list of constraints that will be supported by the PROV ontology and any provenance application that uses the PROV ontology.
-<ul><li> <a name="PROV:0001" href="#PROV:0001">PROV:0001</a> "From the
+	<p>The PROV-DM [[PROV-DM]] introduces a set of specific constraints applicable to PROV ontology. The following is a list of constraints that will be supported by the PROV ontology and any provenance application that uses the PROV ontology.</p>
+
+   <ul>
+<li> <a name="PROV:0001" href="#PROV:0001">PROV:0001</a> "From the
   assertion of a process execution, one can infer that the start
   precedes the end of the represented activity." (<a href="../model/ProvenanceModel.html#PROV:0001">link</a>)
+
 </li><li> <a name="PROV:0002" href="#PROV:0002">PROV:0002</a> "Given a process execution <b>pe</b>, entity <b>e</b>, role <b>r</b>, and optional time <b>t</b>,
 if the assertion <b>wasGeneratedBy(e,pe,r)</b>
 or <b>wasGeneratedBy(e,pe,r,t)</b> holds, the values of <em>some</em> of <b>e</b>'s
@@ -1296,38 +1300,46 @@
 </li><li><a name="PROV:0005" href="#PROV:0005">PROV:0005</a> "Given a process execution <b>pe</b>, entity <b>e</b>, role <b>r</b>, and optional time <b>t</b>, if
  assertion <b>used(pe,e,r)</b> or <b>used(pe,e,r,t)</b> holds, 
 the existence of the value of an attribute of <b>e</b>' is a pre-condition for the activity denoted by <b>pe</b> to terminate."  (<a href="../model/ProvenanceModel.html#PROV:0005">link</a>)
+
 </li><li><a name="PROV:0006" href="#PROV:0006">PROV:0006</a> "Given a process execution <b>pe</b>, entity <b>e</b>, role <b>r</b>, and optional time <b>t</b>, if
  assertion <b>used(pe,e,r)</b> or <b>used(pe,e,r,t)</b> holds, one can
 infer that the use of the thing denoted by <b>e</b> precedes the end
 of <b>pe</b> and follows the beginning of <b>pe</b>. Furthermore, we
 can infer that the generation of the thing denoted by <b>e</b> always precedes
 its use."  (<a href="../model/ProvenanceModel.html#PROV:0006">link</a>)
+
 </li><li> <a name="PROV:0007" href="#PROV:0007">PROV:0007</a> "Given a process execution <b>pe</b>, entities <b>e1</b> and <b>e2</b>, roles <b>r1</b> and <b>r2</b>, if the assertion <b>wasDerivedFrom(e2,e1,pe,r2,r1)</b>
 or <b>wasDerivedFrom(e2,e1)</b> holds, if and only if:
  the values of some attributes
 of <b>e2</b> are partly or fully determined by the values of some
 attributes of <b>e1</b>."  (<a href="../model/ProvenanceModel.html#PROV:0007">link</a>)
+
 </li><li><a name="PROV:0008" href="#PROV:0008">PROV:0008</a> "Given a process execution <b>pe</b>, entities <b>e1</b> and <b>e2</b>, roles <b>r1</b> and <b>r2</b>, if the assertion <b>wasDerivedFrom(e2,e1,pe,r2,r1)</b>
 or <b>wasDerivedFrom(e2,e1)</b> holds, then
 the use
 of characterized thing denoted by <b>e1</b> precedes the generation of
 the characterized thing denoted by <b>e2</b>."  (<a href="../model/ProvenanceModel.html#PROV:0008">link</a>)
+
 </li><li><a name="PROV:0009" href="#PROV:0009">PROV:0009</a> "If <b>wasDerivedFrom(e2,e1)</b> holds, then there exists a process execution <b>pe</b>, and roles <b>r1</b>,<b>r2</b>,
 such that:
   <b>wasGeneratedBy(e2,pe,r2)</b> and <b>used(pe,e1,r1)</b>."  (<a href="../model/ProvenanceModel.html#PROV:0009">link</a>)
+
 </li><li><a name="PROV:0010" href="#PROV:0010">PROV:0010</a> "If <b>wasDerivedFrom(e2,e1,pe,r2,r1)</b> holds, then <b>wasGeneratedBy(e2,pe,r2)</b> and <b>used(pe,e1,r1)</b> also hold." (<a href="../model/ProvenanceModel.html#PROV:0010">link</a>)
+
 </li><li><a name="PROV:0011" href="#PROV:0011">PROV:0011</a> "Given a process execution <b>pe</b>, entities <b>e1</b> and <b>e2</b>, and role <b>r2</b>,
 if <b>wasDerivedFrom(e2,e1)</b> and <b>wasGeneratedBy(e2,pe,r2)</b> hold, then there exists a role <b>r1</b>,
 such that <b>used(pe,e1,r1)</b> also holds." (<a href="../model/ProvenanceModel.html#PROV:0011">link</a>)
 </li>
+
 <li><a name="PROV:0012" href="#PROV:0012">PROV:0012</a> "Given two entities <b>e1</b> and <b>e2</b>, if the assertion <b>isEventuallyDerivedFrom(e2,e1)</b>
  holds, then:
 generation of the characterized thing denoted by <b>e1</b> precedes the generation of
 the characterized thing denoted by <b>e2</b>." (<a href="../model/ProvenanceModel.html#PROV:0012">link</a>)
 </li>
+
 <li><a name="PROV:0013" href="#PROV:0013">PROV:0013</a> "An assertion "wasComplementOf(B,A)" holds over the temporal intersection of A and B, <em>only if</em>: 
-<ol>
-<li> if a mapping can be established from an attribute X of B to an attribute Y of A, then the values of A and B must be consistent with that mapping</em>  </li>
+   <ol>
+   <li> if a mapping can be established from an attribute X of B to an attribute Y of A, then the values of A and B must be consistent with that mapping</li>
   <li>B has some attribute that A does not have
 </li></ol>" (<a href="../model/ProvenanceModel.html#PROV:0013">link</a>)
 </li>
@@ -1336,9 +1348,9 @@
 <li> <b>used(pe,e)</b> holds, or</li>
 <li> <b>wasControlledBy(pe,e)</b> holds, or</li>
 <li>  <b>wasComplementOf(e1,e)</b> holds for some entities <b>e1</b>, and 
- <b>hadPariticipant(pe,e1)</b>  some process execution <b>pe</b>.</li>
+ <b>hadParticipant(pe,e1)</b>  some process execution <b>pe</b>.</li>
 </ul>
-</p>
+
 <div class="note">The following constraints are extracted from the
   ProvenanceModel document.  The text below should be kept consistent
   with the other document, with bidirectional links.  The plan is to
@@ -1352,13 +1364,16 @@
   If a constraint is dropped, please mark it as "defunct" - don't
   delete it!
   </div>
-	  </section>	
     </section>   	  
+
+
+
     <section class='appendix'>
       <h2>Acknowledgements</h2>
       <p>
         The Provenance Working Group Members.
       </p>
     </section>
+
   </body>
 </html>