PROV-ISSUE-585 (applying-satisfying-constraints): Suggestion to avoid discussing how to 'apply' constraints; clarify what it means to 'satisfy' constraints [prov-dm-constraints]

PROV-ISSUE-585 (applying-satisfying-constraints):  Suggestion to avoid discussing how to 'apply'  constraints; clarify what it means to 'satisfy' constraints [prov-dm-constraints]

http://www.w3.org/2011/prov/track/issues/585

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


"""
Checking ordering, typing, and impossibility constraints

The ordering, typing, and impossibility constraints are checked rather than applied.  This means that they do not generate new formulas expressible in PROV,
"""

This sentence again strongly suggests that constraints are "applied", in the sense defined previously, indicating that implementations should follow the operations mentioned previously, when in fact there is no reason to force any materialisation or "normalisastion" at all.
This is again supported by the following sentence:

"Checking such constraints follows a saturation strategy similar to that for normalization"

What follows is again dictating an implementation when everything is in fact just logical formulas that have to be consistency-checked.


...

Section 6.1

"""
A PROV instance is valid if its normal form exists and satisfies all of the validity constraints
"""

Here, it is not clear what "satisfies" means. Satisfaction is a standard term in logic, provided that a proper semantics is defined. Here, there is no proper semantics so the notion of satisfaction would have to be defined. Assuming that PROV statements are indeed mapped to FOL, and constraints expressed as FOL axioms, then the standard notion of "satisfaction" would not work here. For example, the empty document doesn't satisfy any of the constraints (an empty FOL theory only satisfies tautologies, a.k.a., valid formulas, in the usual logical sense of "valid").

There wouldn't be any problem and it would be very much shorter with a proper first order semantics.

Received on Thursday, 25 October 2012 16:26:40 UTC