Re: Fwd: PROV-DM semantics

Thanks, Paul (and Szymon!)

Of course, the semantics draft is vague.  This is intentional.  I'm trying to track the developments of the Data Model (a rapidly moving target) while not devoting the full effort into developing a rigorous model theory prematurely.  Once there is some agreement about the purpose and scope of the semantics (which there isn't yet) I can easily make it precise.

My preference would have been to develop a clean model/theory first, and develop syntax, ontologies etc. once that was well-understood.  I actually asked about doing this early in the process and there wasn't support for this.

In my view many of the questions Szymon raises are also issues for PROV-DM, so it would be helpful to know how the semantics compares to the PROV-DM draft in explaining what's going on to someone with a formal background but not familiar with the various PROV WG drafts.

I'll be visiting Amsterdam Thursday and Friday for the WG face to face meeting and would be happy to discuss this with Szymon if he's around.


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

----- Original message -----
> Hi James, All
> I had a colleague look at the formal semantics. His comments are below. They may
> be useful in helping point out unclear bits.
> Cheers
> Paul
> Begin forwarded message:
> > From: "Szymon Klarman" <>
> > Date: January 30, 2012 19:01:15 GMT+01:00
> > To: "Paul Groth" <>
> > Subject: PROV-DM semantics
> >
> > Hi Paul,
> >
> > I went through the document. I see it's still in an early stage, so naturally
> > it's hard to offer some systematic, concrete feedback. Generally I think it
> > might turn ok, but for the moment my biggest problem with the proposal is a
> > somewhat vague (or incomplete) notion of model (in the mathematical sense of
> > the model theory). The author warns about some potential confusions there and
> > he tries to avoid them but still he loses me. What is a model? Is it an
> > interpretation I? Is it an interpretation together with the function "value"?
> > Is it all these together with a set of time instants and a set of worlds? What
> > are the worlds then? Then, as a consequence, what is the notion of
> > satisfaction, ie. when is a formula satisfied in a model, and how can I
> > effectively verify whether a model for a formula exists? How do I effectively
> > verify that one set of formulas (assertions) entails another formula according
> > to this semantics? And so on. I'm not saying that something is essentially
> > wrong there, but currently the proposal is just still to loose to answer all
> > these questions. And of course you need to be able to answer them, cause
> > that's the core motivation behind any attempt of defining a formal language.
> >
> > Secondly, I'd be quite careful in defining semantics for some relations which
> > assume certain operations on time, eg. specificationOf, where the condition
> > says that the lifetime of one object has to be contained in a lifetime of
> > another one. Very simple formalisms can easily get computationally intractable
> > once you start building in such conditions into the semantics. Again, at this
> > stage I wouldn't be able to determine if there are already some concrete
> > problems, but one should pay attention to these kind of aspects while
> > designing a language. You said that computational aspects are of minor
> > importance here. Perhaps you're right, but my intuition tells me otherwise.
> > The rationale behind proposing a formal language for CS applications is that a
> > software developer can write a program which properly interprets the
> > statements written by someone else and can infer from them exactly the same
> > knowledge as any other software would infer, provided they both conform to the
> > same smantics. Without a prospect of doing inference, there's no real point of
> > designing a formal language in CS.
> >
> > If you have some time tomorrow or Wednesday we can take a look at the document
> > together and discuss these things.
> >
> > Cheers,
> > Szymon

Received on Monday, 30 January 2012 21:27:02 UTC