PROV comments from Clark&Parsia

Hi all,

We are working towards supporting PROV inferences and constraints in
our RDF database Stardog [1]. Below are some comments about PROV
specification documents that we identified while working on our
implementation.

* PROV Constraints

1. The flow control arrows in Figure 1 seem to be backwards.
2. Definition 2.1 seems to be missing the id on the right-hand side.
3. Since uniqueness constraints are ‘applied’ and can derive new
atoms, it is misleading to call them constraints. The same applies to
typing constraints.
4. The definition of enforcement of uniqueness constraints states one
should apply the resulting substitution to the whole PROV instance.
However, the scope of the variables is not sets of rules.
5. Inference 9 (wasStartedBy-inference) should be: IF
wasStartedBy(_id; _a,e1,a1,_t,_attrs), THEN there exist _gen and _t1
such that wasGeneratedBy(_gen; e1,a1,_t1,[]).
6. Inference 10 (wasEndedBy-inference) should be: IF wasEndedBy(_id;
_a,e1,a1,_t,_attrs), THEN there exist _gen and _t1 such that
wasGeneratedBy(_gen; e1,a1,_t1,[]).
7. Inference 15.4 should be: IF wasStartedBy(id; a2,e,_a1,_t,attrs)
THEN wasInfluencedBy(id; a2, e, attrs).
8. Inference 15.7 should be: IF wasDerivedFrom(id; e2, e1, _a, _g, _u,
attrs) THEN wasInfluencedBy(id; e2, e1, attrs).
9. Constraint 56 should be: IF hadMember(c,e) and
'prov:EmptyCollection' ∈ typeOf(c) THEN INVALID.

* PROV-O

PROV Ontology contains several axioms for inferencing but it does not
cover all the inferences described in the PROV constraints document
even though these inferences can be encoded in OWL in a
straightforward way. We think these inferences are useful not just for
validation but also for querying PROV documents. For this reason, we
believe these inferences should be included in PROV-O.

Here are some example OWL axioms encoding some of the inferences from
PROV constraints document:

# Inference 16 (alternate-reflexive)
# IF entity(e) THEN alternateOf(e,e).

:Entity
   rdfs:subClassOf [
       a owl:Restriction ;
       owl:hasSelf true ;
       owl:onProperty :alternateOf
   ] .

# Inference 17 (alternate-transitive)
# IF alternateOf(e1,e2) and alternateOf(e2,e3) THEN alternateOf(e1,e3).

:alternateOf a owl:TransitiveProperty .

# Inference 18 (alternate-symmetric)
# IF alternateOf(e1,e2) THEN alternateOf(e2,e1).

:alternateOf a owl:SymmetricProperty .

# Inference 19 (specialization-transitive)
# IF specializationOf(e1,e2) and specializationOf(e2,e3) THEN
specializationOf(e1,e3).

:specializationOf a owl:TransitiveProperty .

# Inference 20 (specialization-alternate-inference)
# IF specializationOf(e1,e2) THEN alternateOf(e1,e2).

:specializationOf rdfs:subPropertyOf owl:TransitiveProperty .

* PROV-CONSTRAINTS Test Cases

We appreciate as implementers the PROV-Constraints test suite. We
would like to see test suites for the other operational parts of PROV,
in particular for testing inferences separate from validation. This
request arises from our general belief that interoperability with a
formal spec is typically less high than interoperability with a formal
spec *and* an executable test suite. Test suites are invaluable for
implementations. Further, while we would like to see the test suites
be made normative parts of PROV (since that gives a nice algorithm for
resolving disagreements between spec test and test suite (i.e., tie
goes to the test suite)), we would prefer non-normative test suites to
no test suites at all.

We identified the following issues in the following RDF test cases:

* prov-o-class-Invalidation-PASS.ttl: At line 37, there are repeated
semi-colons ‘;;’ which is invalid according to the Turtle grammar
(neither [2] nor [3] seems to allow this).
* prov-o-class-Collection-PASS.ttl: Invalid xsd:dateTime literals
missing minutes and timezone identifier.
* prov-o-property-hadMember-PASS.ttl: Invalid xsd:dateTime literals
missing minutes and timezone identifier.
* ordering-association2-PASS-c47.ttl: This test is marked PASS but it
is inconsistent because the individual ex:ag is an instance of
disjoint classes prov:Entity and prov:Activity.
* prov-o-property-qualifiedCommunication-PASS.ttl: This test is marked
PASS but it is inconsistent because the individual
:writing-celebrity-gossip is an instance of prov:Activity but uses the
property prov:wasAttributedTo whose domain is the disjoint class
prov:Entity. Same argument is also true for the individual
:voicemail-interception.
* prov-o-property-qualifiedRevision-PASS.ttl: This test is marked PASS
but it is inconsistent because the individual :draft2 is an instance
of prov:Entity but uses the property prov:wasAssociatedWith whose
domain is the disjoint class prov:Activity.

We think following tests should not have been included in
rdf-tests.txt because the invalid PROV-N constructs cannot be
expressed in RDF and thus their RDF representation is valid:
           unification-association-f4-FAIL-c23.ttl
           unification-association-f5-FAIL-c23.ttl
           unification-derivation-f1-FAIL-c23.ttl
           unification-derivation-f2-FAIL-c23.ttl
           unification-derivation-f3-FAIL-c23.ttl
           unification-derivation-f4-FAIL-c23.ttl

Best,
Evren

[1] http://stardog.com/
[2] http://www.w3.org/TeamSubmission/turtle/#sec-grammar
[3] http://www.w3.org/TR/turtle/#sec-grammar


--
Evren Sirin
CTO
Clark & Parsia, LLC
http://clarkparsia.org

Received on Friday, 4 January 2013 17:24:43 UTC