Re: PROV-ISSUE-635 (prov-sem-completeness): Completeness and scope of prov-sem [Formal Semantics]

sounds good to me

pg


On Fri, Mar 8, 2013 at 1:43 PM, James Cheney <jcheney@inf.ed.ac.uk> wrote:

>
> Following offline discussion with Luc, I propose to resolve this by doing
> the following:
>
> 1.  Discuss syntactic models of PROV, where soundness and completeness is
> easy (since they are essentially just valid instances) but the models are
> not necessarily "intuitive".
>
> 2. Flesh out the existing naive semantics to ensure soundness.  This
> means: in any naive model, all of the inferences and constraints are
> satisfied.  This implies: no invalid instance has a model.
>
> 3. If time permits, generalize to a "reference" semantics that provides a
> weak form of completeness, which may require (for example) allowing
> non-linear event orderings.  This will mean soundness + any valid instance
> has a reference model.
>
> I propose that (1,2) are minimal criteria for the final version and (3) is
> desirable-but-optional.
>
> My feeling is that aiming for (2) while keeping (3) in mind will be more
> likely to succeed than trying to do (2) directly.  We can see where the
> incompleteness issues arise once (1,2) are done and try to do the minimum
> needed to recover completeness.
>
> Are there any objections to this strategy, in particular to the potential
> absence of (3)?
>
> --James
>
> On Mar 1, 2013, at 4:58 PM, Provenance Working Group Issue Tracker <
> sysbot+tracker@w3.org> wrote:
>
> > PROV-ISSUE-635 (prov-sem-completeness): Completeness and scope of
> prov-sem [Formal Semantics]
> >
> > http://www.w3.org/2011/prov/track/issues/635
> >
> > Raised by: James Cheney
> > On product: Formal Semantics
> >
> > This issue is a placeholder for discussion of the scope of the
> semantics, and whether we will attempt to develop an intuitive semantics
> such that the PROV-CONSTRAINTS (viewed as a first-order theory) is sound
> and complete in some sense.
> >
> > Alternatively, we can consider completeness to mean that every valid
> PROV instance has a model, and soundness to mean that no invalid instances
> have models.  Currently, only soundness is intended to hold (but more work
> is needed to accomplish that).
> >
> >
> > Luc gives a counterexample to completeness:
> >
> >> entity(e)
> >> activity(a1)
> >> activity(a2)
> >> wasGeneratedBy(gen1; e, a1, 2011-11-16T16:05:00)
> >> wasGeneratedBy(gen2; e, a2, 2012-11-16T16:05:00) //different date
> >>
> >>
> >> gen1 <= gen2 and gen2 <= gen1
> >>
> >>
> >> Formalism 29 implies: 2011-11-16T16:05:00 == 2012-11-16T16:05:00
> >
> >
> >
> >
>
>
> --
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
>
>


-- 
--
Dr. Paul Groth (p.t.groth@vu.nl)
http://www.few.vu.nl/~pgroth/
Assistant Professor
- Knowledge Representation & Reasoning Group |
  Artificial Intelligence Section | Department of Computer Science
- The Network Institute
VU University Amsterdam