- From: Luc Moreau <l.moreau@ecs.soton.ac.uk>
- Date: Thu, 28 Feb 2013 12:20:57 +0000
- To: James Cheney <jcheney@inf.ed.ac.uk>
- CC: "public-prov-wg@w3.org" <public-prov-wg@w3.org>
Hi James Sorry I am confused, I thought this example has a NF and satisfies all prov-constraints, but there is no model for it in the semantics. Luc On 28/02/13 12:09, James Cheney wrote: > This is an example of incompleteness (something is true in the models we consider, but not derivable from the constraints), not of unsoundness. That's why I don't claim any kind of completeness. It's a good example to illustrate the limitations of the naive model with linear time. > > An unsoundness would be a situation where something is implied by inferences/constraints but not true in the model. However, the models here are not, and are not intended to be, complete, just to illustrate some of the intuitions of the semantics. (We can trivially get a soundness/completeness result from mapping everything to first-order logic, but the models we get are not guaranteed to have anything to do with the ones we've been discussing in the semantics). > > There is still work to be done to translate the formal constraints to appropriate constraints on the semantics to ensure soundness, though. For example, there is nothing in the definition of structures that enforces inference 5 (and many other inferences). > > --James > > On Feb 28, 2013, at 11:32 AM, Luc Moreau <l.moreau@ecs.soton.ac.uk> wrote: > >> Hi James, >> >> Here is a prov instance that is valid, I believe. >> >> 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 >> >> >> Indeed, prov-constraints now allows multiple generations for a given entity. >> >> There is a requirement that: >> gen1 <= gen2 and gen2 <= gen1 >> >> But there is no requirement that 2011-11-16T16:05:00 and 2012-11-16T16:05:00 be equal. >> >> However, formalism 29 of prov-sem seems to imply that >> 2011-11-16T16:05:00 == 2012-11-16T16:05:00 >> >> The reason of this difference is that prov-sem maps all events to a time on a time line, and >> compares time information, whereas prov-constraints does not. >> >> If my reasoning is right, this would indicate that the constraints are not sound with respect >> to this semantics. Thoughts? >> >> Luc >> >> -- >> Professor Luc Moreau >> Electronics and Computer Science tel: +44 23 8059 4487 >> University of Southampton fax: +44 23 8059 2865 >> Southampton SO17 1BJ email: l.moreau@ecs.soton.ac.uk >> United Kingdom http://www.ecs.soton.ac.uk/~lavm >> >> > -- Professor Luc Moreau Electronics and Computer Science tel: +44 23 8059 4487 University of Southampton fax: +44 23 8059 2865 Southampton SO17 1BJ email: l.moreau@ecs.soton.ac.uk United Kingdom http://www.ecs.soton.ac.uk/~lavm
Received on Thursday, 28 February 2013 12:22:51 UTC