owlcs / jfact

JFact repository
13 stars 8 forks source link

HermiT issue with dateTime timezone semantics for DataOneOf #21

Closed ubbc closed 4 years ago

ubbc commented 4 years ago

Hi, I think that HermitT 1.4.3 is not taking into account timezones in xsd:dateTime when computing DataOneOf. In the example below the times: "2020-01-07T12:32:00Z"^^xsd:dateTime (in :test) "2020-01-07T11:32:00-01:00"^^xsd:dateTime (in :test4) "2020-01-07T12:32:00+00:00"^^xsd:dateTime (in the GCA) should correspond to the same point on the timeline. HermiT correctly infers :test as class :D but not :test4 Whereas, Pellet and Fact++ infer both. Kind regards Graham

--- Example ontology ---

Prefix(:=<http://www.ubbc.co.uk/ontologies/hermitBug#>)
Prefix(owl:=<http://www.w3.org/2002/07/owl#>)
Prefix(rdf:=<http://www.w3.org/1999/02/22-rdf-syntax-ns#>)
Prefix(xml:=<http://www.w3.org/XML/1998/namespace>)
Prefix(xsd:=<http://www.w3.org/2001/XMLSchema#>)
Prefix(rdfs:=<http://www.w3.org/2000/01/rdf-schema#>)
Ontology(<http://www.ubbc.co.uk/ontologies/hermitBug>

Declaration(Class(:C))
Declaration(Class(:D))
Declaration(DataProperty(:hasDate))
Declaration(NamedIndividual(:test))
Declaration(NamedIndividual(:test2))
Declaration(NamedIndividual(:test3))
Declaration(NamedIndividual(:test4))
Declaration(NamedIndividual(:test5))
Declaration(NamedIndividual(:today))

############################
#   Named Individuals
############################

# Individual: :test (:test)
DataPropertyAssertion(:hasDate :test "2020-01-07T12:32:00Z"^^xsd:dateTime)
# Individual: :test2 (:test2)
DataPropertyAssertion(:hasDate :test2 "2020-01-07T11:22:33-01:00"^^xsd:dateTimeStamp)
# Individual: :test3 (:test3)
DataPropertyAssertion(:hasDate :test3 "2020-02-02T00:00:00"^^xsd:dateTime)
# Individual: :test4 (:test4)
DataPropertyAssertion(:hasDate :test4 "2020-01-07T11:32:00-01:00"^^xsd:dateTime)
# Individual: :test5 (:test5)
DataPropertyAssertion(:hasDate :test5 "2020-01-07T11:32:00+01:00"^^xsd:dateTime)
SubClassOf(DataSomeValuesFrom(:hasDate DataOneOf("2020-01-07T12:32:00+00:00"^^xsd:dateTime)) :D)
SubClassOf(DataSomeValuesFrom(:hasDate DatatypeRestriction(xsd:dateTime xsd:minExclusive "2020-01-31T00:00:00"^^xsd:dateTime)) :C)
ubbc commented 4 years ago

I believe this is not an issue with Hermit it is actually the older reasoners that are in error.

The literals "2020-01-07T12:32:00Z"^^xsd:dateTime and "2020-01-07T12:32:00+00:00"^^xsd:dateTime represent the same instants in the same time zone. "2020-01-07T11:32:00-01:00"^^xsd:dateTime represents the same instant in a different time zone and is considered an equal but not identical literal. (see Structural Spec 4.7).

DataOneOf treats "2020-01-07T12:32:00+00:00"^^xsd:dateTime as a different literal and :test4 is not inferred as class :D.

To build a GCA that compares time instant values a restriction with two facets can be combined for value equality: DatatypeRestriction(xsd:dateTime xsd:minInclusive "2020-01-07T12:32:00Z"^^xsd:dateTime xsd:maxInclusive "2020-01-07T12:32:00Z"^^xsd:dateTime))

ignazio1977 commented 4 years ago

I love the fact that the example in the specs uses dates of birth, which in many countries do not necessarily include a time component at all. In UK, for example, the time is recorded only for twins. The hospital keeps a record of the time but it does not make it onto registrar documents otherwise.

ubbc commented 4 years ago

:) and then one may need to take into account the +/- 14hrs....

I don't think either Pellet or Fact++ are still maintained, so I guess can be closed off? Thanks for checking in on it.

ignazio1977 commented 4 years ago

They are, far as I'm aware - or their forks are. Not by this team, though. I'll see if it's wort putting this on their trackers.

ignazio1977 commented 4 years ago

There's a w3c Reasoner test for 1^^xsd:int and 01^^xsd:int being treated the same, and it's basically the same issue, non-equal literals being semantically equivalent. Not sure if there's one for dates - certainly timezones are a pain point worldwide, so worth keeping in mind.

ubbc commented 4 years ago

Ok many thanks.