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]

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.

Received on Thursday, 25 October 2012 16:16:59 UTC