--- a/ontology/ProvenanceFormalModel.html	Fri Oct 07 14:31:47 2011 -0400
+++ b/ontology/ProvenanceFormalModel.html	Fri Oct 07 14:38:36 2011 -0400
@@ -1265,11 +1265,16 @@
 		  </pre>
 		</div>		
 	</section>
+
+
+
 	<section>
 		<h3>OWL2 Semantics for PROV Ontology</h3>
 		<p>In addition to RDF Semantics, the OWL2 semantics as described in [[!OWL2-DIRECT-SEMANTICS]], [[!OWL2-RDF-BASED-SEMANTICS]] are also applicable to PROV ontology. We consider the OWL2 RDF-Based Semantics (since it is a semantics superset of OWL2 Direct Semantics) and specifically the extension of the D-interpretation, which satisfies the constraints for rdf-interpretation, rdfs-interpretation (as defined in previous section), graphs with blank nodes, and interpretation defined for RDF datatypes (see Section 5.1 in RDF Semantics [[!RDF-MT]]). The OWL2 RDF-based semantics introduces the notion of "facets" to constrain datatypes, both the rdf:XMLLiteral defined in the RDF Semantics [[!RDF-MT]] and datatypes defined in the OWL2 Structural Specifications [[!OWL2-SYNTAX]]. The OWL2 RDF-based interpretation, also called <b>D-interpretation with facets</b> is a D-interpretation that also satisfies the OWL2 RDF-based semantics called "semantic constraints" (see Section 5 in OWL2 RDF-Based Semantics [[!OWL2-RDF-BASED-SEMANTICS]]).  
 		</p>
 	</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.</p>
@@ -1278,8 +1283,9 @@
 <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><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>,
+<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
 attributes are determined by the activity denoted by <b>pe</b> and the
@@ -1288,45 +1294,57 @@
 since, in an open world, not all used entities may have been
 asserted."
  (<a href="../model/ProvenanceModel.html#PROV:0002">link</a>)
-</li><li><a name="PROV:0003" href="#PROV:0003">PROV:0003</a> "Given an assertion <b>wasGeneratedBy(x,pe,r)</b> or <b>wasGeneratedBy(x,pe,r,t)</b>, one can
+</li>
+
+<li><a name="PROV:0003" href="#PROV:0003">PROV:0003</a> "Given an assertion <b>wasGeneratedBy(x,pe,r)</b> or <b>wasGeneratedBy(x,pe,r,t)</b>, one can
 infer that the generation of the thing denoted by <b>x</b> precedes the end
 of <b>pe</b> and follows the beginning of <b>pe</b> "
  (<a href="../model/ProvenanceModel.html#PROV:0003">link</a>)
+</li>
 
-</li><li><a name="PROV:0004" href="#PROV:0004">PROV:0004</a> "Use
+<li><a name="PROV:0004" href="#PROV:0004">PROV:0004</a> "Use
 represents the consumption of a characterized entity by an activity."
 (Defunct.)
+</li>
 
-</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
+
+<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><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
+<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><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>
+<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><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>
+<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><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>,
+<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><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>,
+<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>
@@ -1339,16 +1357,18 @@
 
 <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</li>
-  <li>B has some attribute that A does not have
-</li></ol>" (<a href="../model/ProvenanceModel.html#PROV:0013">link</a>)
+      <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" (<a href="../model/ProvenanceModel.html#PROV:0013">link</a>) </li>
+   </ol>
 </li>
+
 <li><a name="PROV:0014" href="#PROV:0014">PROV:0014</a> "Given a process execution <b>pe</b> and entity <b>e</b>, <b>hadPariticipant(pe,e)</b> holds if and only if:
-<ul> 
-<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>hadParticipant(pe,e1)</b>  some process execution <b>pe</b>.</li>
+   <ul> 
+      <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>hadParticipant(pe,e1)</b>  some process execution <b>pe</b>.</li>
+   </ul>
+</li>
 </ul>
 
 <div class="note">The following constraints are extracted from the