Re: Fwd: PROV-DM semantics

I can relate to the concern about the term "model".   The provenance data 
"model" is certainly not a model in the sense of model theoretic semantics.

But the comment "when is a formula satisfied in a model" seems odd to me - my 
understanding that, per MT semantics, a *model* (of some formula or expression) 
is defined as an interpretation that satisfies the formula?

#g
--

On 30/01/2012 19:15, Paul Groth wrote:
> 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"<klarman@wp.pl>
>> Date: January 30, 2012 19:01:15 GMT+01:00
>> To: "Paul Groth"<pgroth@gmail.com>
>> 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 wr
ong 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 sman
tics. 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 Tuesday, 31 January 2012 09:56:19 UTC