--- a/ontology/ProvenanceFormalModel.html	Sat Aug 06 09:16:01 2011 +0100
+++ b/ontology/ProvenanceFormalModel.html	Mon Aug 08 17:35:28 2011 +0100
@@ -290,7 +290,25 @@
 </td><td style="border-style: solid; border-width: 0 1px 1px 0">Yes
 </td></tr></table>
 	  <section>
-		<h4>Transitivity</h4>
+		<h4>Additional properties </h4>
+<div class="note">TODO: Number these and cross-reference with
+  Provenance Model, to make it easier to keep the definitions
+  consistent (and ensure we don't forget some properties).
+  </div>
+<ul><li> "From the assertion of a process execution, one can infer that the start precedes the end of the represented activity. "
+</li><li> "Given an assertion isGeneratedBy(x,pe,r) or isGeneratedBy(x,pe,r,t), the activity denoted by pe and the entities used by pe dermine values of some of x's attributes."
+</li><li>"Given an assertion isGeneratedBy(x,pe,r) or isGeneratedBy(x,pe,r,t), one can infer that the generation of the entity denoted by x precedes the end of pe and follows the beginning of pe. "
+</li><li> "Use represents the consumption of a characterized entity by an activity."
+
+</li><li> "Given an assertion uses(pe,x,r) or uses(pe,x,r,t), at least one value of x's attributes is a pre-condition for the activity denoted by pe to terminate."
+</li><li> "Given an assertion uses(pe,x,r) or uses(pe,x,r,t), one can infer that the use of the entity denoted by x precedes the end of pe and follows the beginning of pe. Furthermore, we can infer that the generation of the entity x always precedes its use. * "From an assertion isDerivedFrom(B,A), the values of some attributes of B are at least partially determined by the values of some attributes of A."
+</li><li> "Given an assertion isDerivedFrom(B,A), one can infer that the use of characterized entity denoted by A precedes the generation of the characterized entity denoted by B. "
+</li><li> "if isDerivedFrom(e1,e0) holds, then there exists a process execution pe, and roles r0,r1, such that: isGeneratedBy(e1,pe,r1) and uses(pe,e0,r0)."
+</li><li> "The relationship isDerivedFrom is transitive. "
+</li><li> "The relationship isDerivedFrom+ is the transitive closure of isDerivedFrom."
+</li><li> Various things involving IVP-of
+</li></ul>
+
 	  </section>	
     </section>
     <section class='appendix'>