The domain of time:inside #1448
Description
This is a question of how to interpret two parts of the implementation of time:inside (link is to today's definition). The short summary is: I think the definition of time:inside should be changed to include the word "proper" near the end.
Related-Issue check: I did a scan for time:inside on the issue tracker, and only saw it noted on #1126 , and on no PRs. That discussion was helpful for introducing :equals, but I don't think its scope matches what I'm covering below.
The domain of time:inside is:
time:inside rdfs:domain time:Interval .The definition reads as follows, with emphasis added:
An instant that falls inside the interval. It is not intended to include beginnings and ends of intervals.
How firmly should "not intended" be read there? If the beginning and end of an interval are not included, then the length of the interval is non-0, and thus the interval is a time:ProperInterval.
Why, then, would the domain be the 0-duration-permitted time:Interval? Wouldn't it always be time:ProperInterval?
I think this example graph suggests a reconciliation:
ex:Instant-1
a time:Instant ;
.
ex:Interval-1
a time:Interval ;
time:hasBeginning ex:Instant-1 ;
time:inside ex:Instant-1 ;
time:hasEnd ex:Instant-1 ;
.A benefit to the domain being as it is, just time:Interval, is this graph is consistent with the OWL implementation if ex:Interval-1 a time:Instant would be inferred or entailed. Changing the domain to time:ProperInterval would raise OWL inconsistency errors if time:Instant were inferred or entailed.
However, this graph is inconsistent with the noted intention in the definition (rdfs:comment), as the beginning and end are included. If the definition (comment) were changed to read as follows, this graph would then be consistent, because a proper interval isn't involved:
An instant that falls inside the interval. It is not intended to include beginnings and ends of proper intervals.
An aside on encoding the intention
It also might be clarifying to encode the "not intended" with property-disjoint statements; but, in OWL, IIRC, this can only be done globally at the property level, and can't be scoped to just time:ProperInterval while excusing time:Interval:
time:inside
owl:propertyDisjointWith
time:hasBeginning ,
time:hasEnd
;
.I'm aware of SHACL being able to provide a class-specific shape that encodes this, but I also appreciate OWL-Time doesn't currently provide SHACL shapes. For reference, sh:disjoint would be the mechanism:
ex:ExampleShape
sh:targetClass time:ProperInterval ;
sh:property [
sh:path time:hasBeginning ;
sh:disjoint time:inside ;
sh:message "The set of instants inside a proper interval is not intended to include the beginning of the interval."@en ;
] ;
sh:property [
sh:path time:hasEnd ;
sh:disjoint time:inside ;
sh:message "The set of instants inside a proper interval is not intended to include the end of the interval."@en ;
] ;
.