Re: PROV-ISSUE-579 (declarative-fol-specification): Suggestion to replace procedural specification with (equivalent, but shorter and less prescriptive) declarative theory in First-Order Logic [prov-dm-constraints]

Following recent review of PROV-SEM, this issue is now closed.

--James

On Mar 8, 2013, at 12:47 PM, James Cheney <jcheney@inf.ed.ac.uk> wrote:

> I believe that completing the semantics as outlined in ISSUE-635 will close this issue.  Unless there is further discussion, I will make it a review question for the final version of PROV-SEM whether the two issues have been addressed.
> 
> --James
> 
> 
> On Oct 25, 2012, at 5:16 PM, Provenance Working Group Issue Tracker <sysbot+tracker@w3.org> wrote:
> 
>> PROV-ISSUE-579 (declarative-fol-specification): Suggestion to replace procedural specification with (equivalent, but shorter and less prescriptive) declarative theory in First-Order Logic [prov-dm-constraints]
>> 
>> http://www.w3.org/2011/prov/track/issues/579
>> 
>> Raised by: James Cheney
>> On product: prov-dm-constraints
>> 
>> A sub-issue of ISSUE-576.
>> 
>>> From Antoine Zimmermann's email:
>> http://lists.w3.org/Archives/Public/public-prov-comments/2012Oct/0004.html
>> 
>> The document tries to define a kind of semantics for the PROV-DM, but it's not actually defining a proper semantics at all. And since it does not truly define a formal semantics, it has to redefine the terms that are borrowed from logic, and subtly diverge from the standard notions found in logic. For someone who knows about logic, it makes the document larger, more complicated than it should be, more difficult to read, and more difficult to implement. For someone who does not know about logic, it's not made at all simpler, on the contrary.
>> 
>> ...
>> 
>> If a proper semantics was defined, there would be no way the document diverge from legacy logical concepts. There would be less chances for mistakes in the definitions and in the rules laters. There would be more flexibililty in the way implementations support the semantics.
>> 
>> I see two escapes for this:
>> 1)  define an ad hoc model theory for PROV-DM, in the line of what's sketched in PROV-SEM;
>> 2)  rely on a well known logic (such as FOL), to which all PROV statements are mapped, and add FOL axioms to model the constraints.
>> 
>> 1) is ambitious and I understand there is not enough time to investigate it enough. But 2) is really easy. PROV statements already look a lot like FOL predicates, and PROV Constraints already rely heavily on FOL notions and notations.
>> 
>> 
>> 
>> 
> 
> 
> -- 
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
> 
> 
> 


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

Received on Thursday, 11 April 2013 15:15:16 UTC