- From: James Cheney <jcheney@inf.ed.ac.uk>
- Date: Thu, 28 Feb 2013 12:42:28 +0000
- To: Luc Moreau <L.Moreau@ecs.soton.ac.uk>
- Cc: "public-prov-wg@w3.org" <public-prov-wg@w3.org>
That's correct, but that is an example of incompleteness, not unsoundness. If we take the view that the "models" are the structures of the reference semantics and the "theory" is (the first order version of) PROV-CONSTRAINTS, then: Soundness means that if an inference is derivable then it holds in all models (|- phi => |= phi). This is intended (but not yet the case for trivial reasons) for the reference semantics, but your example is not a counterexample to this. Completeness means that if an inference holds in all models then it's derivable (|= phi => |- phi). Your example is a counterexample to completeness. In all of the reference-semantics models, it is the case that the two times of different generations of the same entity must be equal, but there is no way to derive this using the (first-order version of) the constraints. --James On Feb 28, 2013, at 12:20 PM, Luc Moreau <L.Moreau@ecs.soton.ac.uk> wrote: > 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 > > > -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Received on Thursday, 28 February 2013 12:42:59 UTC