time-prov: Drop alignment axioms that lead to deprecated property

[ajnelson-nist]

The file time-prov.ttl provides a non-normative alignment between OWL-Time and PROV-O. One of the included suggestions is an alignment of prov:endedAtTime with time:inXSDDateTime via a property chain. Unfortunately, in the current draft of OWL-Time, time:inXSDDateTime is deprecated. A similar issue is present for prov:startedAtTime and prov:atTime.

This patch drops alignment axioms that would lead an adopting user to cause their PROV-O data to yield deprecated property usage under OWL entailment.

This contribution is made only by myself, and is not being made by the National Institute of Standards and Technology or any other organization.

[dr-shorthair]

Thanks @ajnelson-nist

As you have noted, the proposed change is to a non-normative artefact which is provided informally in the repository. So there should be no process impediment to the change.

Nevertheless, these alignment axioms are also described in the Recommendation document at https://www.w3.org/TR/owl-time/#time-prov While I don't think the Rec points directly to the RDF files, does there need to be a small corresponding amendment to the document?

My feeling is that the property-chain axiom is a useful pointer, so I would be reluctant to remove it from the document, but maybe it needs to be hedged with some more wording.

Note, however, that changes to the document also have to go through a larger process.

Re. #1421

[ajnelson-nist]

I've stumbled onto another syntactic reason for removal of the property chain axiom.

owl:propertyChainAxiom does not accept owl:DatatypePropertys. It's natural-feeling for the use case underlying this PR to "share" a literal value between some object and another linked object, by making a property chain of owl:ObjectPropertys ending with some owl:DatatypeProperty. But, then I looked at all (5) occurrences of owl:propertyChainAxiom on the OWL 2 Mapping to RDF, which includes strict syntax matching requirements.

The last occurrence of owl:propertyChainAxiom, in the middle of Table 16, reads like this:

x owl:propertyChainAxiom T(SEQ y1 ... yn) . { n ≥ 2, OPE(yi) ≠ ε for each 1 ≤ i ≤ n, and OPE(x) ≠ ε }

(I.e., each yi in the chain is defined as an object property. Notation is described in Section 3.2.1.)

There is no corresponding mapping from RDF to the functional representation that reads x owl:propertyChainAxiom T(SEQ y1 ... yn z); ... ; DPE(z) ≠ ε. So, if a graph contained some property chain ending with a datatype property, the last line of Section 3 ...

At the end of this process, the graph G must be empty.

... would find that the parsing process described through Section 3 didn't exhaustively match the graph, making the graph OWL 2 FULL instead of OWL 2 DL.

I saw a hint of this restriction on chains when I was first learning OWL and PROV-O some years ago. The Turtle encoding of PROV-O includes editorial notes like this:

:endedAtTime
    # ...
    :editorialNote "It is the intent that the property chain holds: (prov:qualifiedEnd o prov:atTime) rdfs:subPropertyOf prov:endedAtTime."@en ;
    # ...
    .

I had thought it odd that they knew their intent enough to put it into English, but didn't encode it in Turtle. I can't guess to their reasoning back then, but I now think a reason is OWL 2 DL doesn't support a chain with a datatype property.

So, it seems this PR also incidentally removes syntax that would move an adopter of this (non-normative) resource into OWL 2 FULL.

@chris-little : Would adopting a similar informal description of the intended---but not encodable in OWL---property chain be satisfactory? E.g., borrowing and adapting the PROV-O wording style:

It is the intent that the property chain holds: (time:hasEnd o time:inXSDDateTime) rdfs:subPropertyOf prov:endedAtTime. However, some translation mechanism should be used to align the timestamp value to time:inXSDDateTimeStamp.

[chris-little]

@ajnelson-nist You have pushed me well beyond my comfort zone. But if I understand correctly, the property chain would require OWL Full, which means some queries could be undecidable, which does not seem right for (simple) reasoning about time. I have been applying "when in doubt, cut it out" which may not be sensible. I need the other reviewers to jump in.