> 1. Is the purpose of the document clear and consistent with the working group's consensus about the semantics? If not, can you suggest clarifications or improvements?
 > 
 > Yes
 > 
 > 2. Are there minor issues that can be corrected easily prior to final release?
 > 
 > Yes (see below)
 > 
 > 3. Are there blocking issues that must be addressed prior to final release?
 > 
 > No
 > 
 > 4. ISSUE-579 requested that we incorporate an axiomatization using a more standard logic formalism e.g. first-order logic.  The current draft attempts to address this.  Can this issue be closed?
 > 
 > Yes.
 > 
 > 5. ISSUE-635 requested that we address the issues of soundness and completeness in the semantics.  This is currently attempted, by generalizing the semantics (which unfortunately also decreases the connection to intuitive notions of time.)  As a result, we have a soundness and weak completeness result stating that any valid PROV instance has a model and vice versa.  Can this issue be closed?
 > 
 > Yes.
 > 
 > 
 > 
 > C1. In Section 1.1., it will be helpful to provide a reference to Naive Semantics.
 > 

I'm not sure what you mean here.  I've made other copies of "naive semantics" into links to this definition.

If you mean refer to an external resource, please suggest one.

 > C2. In Section 2.1, you state that "To allow for the fact that some
 > attributes can have undefined or multiple values, we sometimes use the set P(Value), that is, the set of sets of values." For clarification, you may add here that you use empty sets for undefined values.

There is a remark to this effect later, but it's good to signpost it.

 > 
 > C3. In Section 3, you use the term component, which is also use in PROV-DM, but with different meaning. It is worth mentioning this.

Done

 > 
 > C4. In the first paragraph of Section 3.2, the correspondence between Things and Objects is not clear, although it is talked about. This confusion is then lifted later on in the same section, but I think it is worth saying something about this earlier.

Done

 > 
 > C5. In Section 3.3, component 14, I could not follow the 5th bullet, I suspect there is a variable that has not been declared.
 > 

Do you mean additional axiom 5?

I believe the unquantified variable was $w$, and I've clarified it.  Basically it is a dummy variable for the stuff in between the beginning and end of a derivation path.


 > C6. In component 15, I was wondering if the following inference is mentioned somewhere: "a path between two entities that is contained in a dervation path, is also a derivation path"
 > 

No, there is no inference to this effect in PROV-CONSTRAINTS, so we do not assume it here.

 > C7. In the sets of structures that are listed in Section 6.2.1, there are variables that are not bound in the set. Some of these variables are associated the imprecise derivation, but there are also others that are not. In particular, if you look at the second set in the union that define Activities, you will notice that aid and aid' are not bound.
 > 
 > 

These are new activities, generations, invalidations, and usages associated with certain ids.  The notations a_id and so on are explained later.