Re: PROV-SEM staged, ready for review

Hi James,

I didn't find the time to go over the document extensively myself, but my
colleague, Joachim Van Herwegen did, and we discussed his remarks
internally.
We see no blockers and have the following minor remarks:

1. Introduction:
  PROv -> PROV
  The semantics does not (as yet) cover --> The semantics do not (as yet)
cover

3.1
  an associates set of Events --> associated

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?

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)

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.
3.2.4.1
    started(st)=(a,e,a′) implies start∈ --> st is undefined. Change to
started(start)
3.3
    6. 'a' is undefined --> there exist gen, assoc and a
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?

4.3.2
    startTime/endTime(id): --> should be act instead of id
4.4.10.1 use event ρ(u)∈Usages. --> use event use = ρ(u) ∈Usages

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)

So in short: good job!

Regards,
Tom and Joachim

2013/4/9 Khalid Belhajjame <Khalid.Belhajjame@cs.man.ac.uk>

>
> Hi James,
>
> The ProvSem document is quite good, and it is much more complete compared
> with the previous version. Below, you will find the answers to the
> questions you asked. You will also find minor comments that you may want o
> consider.
>
> Regards, khalid
>
> 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.
>
> 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.
>
> 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.
>
> 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.
>
> 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.
>
> 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"
>
> 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.
>
>
> On 5 April 2013 17:38, James Cheney <jcheney@inf.ed.ac.uk> wrote:
>
>> Hi,
>>
>> PROV-SEM is now ready for review here:
>>
>>
>> https://dvcs.w3.org/hg/prov/raw-file/default/semantics/releases/NOTE-prov-sem-20130430/Overview.html
>>
>> As before, because it renders math using MathML, different browsers do
>> better/worse jobs with it.  I get the best results with Safari (Mac OS X)
>> and Firefox does OK, while Chrome does not do very well.  Accordingly, I've
>> put a PDF built using Safari here:
>>
>>
>> https://dvcs.w3.org/hg/prov/raw-file/default/semantics/releases/NOTE-prov-sem-20130430/prov-sem.pdf
>>
>> Several people volunteered to review by next week's teleconference, when
>> (I believe) we will vote on all remaining NOTEs.
>>
>>
>> Please address the following review questions:
>>
>> 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?
>>
>> 2. Are there minor issues that can be corrected easily prior to final
>> release?
>>
>> 3. Are there blocking issues that must be addressed prior to final
>> release?
>>
>> 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?
>>
>> 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?
>>
>> --James
>>
>>
>> --
>> The University of Edinburgh is a charitable body, registered in
>> Scotland, with registration number SC005336.
>>
>>
>>
>