- From: James Cheney <jcheney@inf.ed.ac.uk>
- Date: Fri, 8 Mar 2013 12:43:36 +0000
- To: Provenance Working Group <public-prov-wg@w3.org>
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.
Received on Friday, 8 March 2013 12:44:40 UTC