Re: a question on semantics prov-sem and soundness of constraints (issue-630)

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
> 
> 


-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Received on Thursday, 28 February 2013 12:10:02 UTC