> 1. Introduction: > PROv -> PROV > The semantics does not (as yet) cover --> The semantics do not (as yet) cover > Fixed > 3.1 > an associates set of Events --> associated Fixed > > 3.2 > It is also possible to have two different objects that are indistinguishable by their attributes and time intervals --> did you mean events instead of time intervals? Fixed - incomplete search & replace. > > 3.2.1.2 > Just wondering why you decided to use a relation for contains here, whereas for the rest of the document, you use functions. Both are correct, but this is the only place a relation was used. (unless we missed something) Yes, that change seems like a win! (We do use relations for event ordering though.) much better for stating emptiness constraints. > > 3.2.2 > An activity is an object that encompasses a set of events. --> Earlier in the document an object is described as encompassing a set of events, so according to this, all objects would be activities. Well, this isn't an if and only if. But there is no reason to be so specific., clarified this. > 3.2.4.1 > started(st)=(a,e,a′) implies start∈ --> st is undefined. Change to started(start) Fixed > 3.3 > 6. 'a' is undefined --> there exist gen, assoc and a Fixed > Also, the remark about axioms 22 and 23 is correct, but why is it arguable? If the constraint exists, why leave invalidations out here? Does it break something else? > If we omit invalidations, then the weak completeness result won't hold, or at least, I'm not sure how to prove it. Trying to come up with a counterexample. > 4.3.2 > startTime/endTime(id): --> should be act instead of id Fixed > 4.4.10.1 use event ρ(u)∈Usages. --> use event use = ρ(u) ∈Usages > Fixed > I see most of these have been fixed already after other reviews. > Overall, it's a good document, and for the most part understandable if you know the basic syntax. Chapter 6 is harder to follow, especially if you're not that familiar with formal logic, or a bit rusty. (which is probably not the audience for this document anyway) >