Hi,
On 08/01/2020 20:57, Andrea Leofreddi wrote:
Hello,
I'm using Jena Fuseki 3.13.1 (with OWLFBRuleReasoner), and I have
asserted (uploaded) the following triples:
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@prefix owl: <http://www.w3.org/2002/07/owl#> .
@prefix f: <http://vleo.net/family#> .
f:Bob f:hasWife f:Alice .
f:Bob f:hasWife f:Alice2 .
f:Alice2 f:hasHusband f:Bob2 .
f:hasWife a owl:FunctionalProperty .
f:hasWife a owl:InverseFunctionalProperty .
f:hasHusband owl:inverseOf f:hasWife .
Now, If I query and ASK { f:Alice owl:sameAs f:Alice2 }, I get
true. However, If I ASK { f:Bob owl:sameAs f:Bob2 }, I get false!
Loading the same triples on another reasoner (owl-rl), I get the
triple f:Bob owl:sameAs f:Bob2 inferred.
I have asked this very question on StackOverflow
(https://stackoverflow.com/questions/59603569/jena-fuseki-missed-inference?noredirect=1#comment105379894_59603569),
and I got pointed out to the owl-fb rules file. Tweaking it a bit I
noticed that If I explicitly add the forward version of inverseOf, I get
that f:Bob owl:sameAs f:Bob2:
[inverseOf2b: (?P owl:inverseOf ?Q), (?X ?P ?Y) -> (?Y ?Q ?X) ]
Am I missing something?
No, that seems right.
The issue is that the default jena rules file for OWL (the fb rules)
uses a mix of forward and backward rules in order to make the various
performance/completeness trade-offs.
Those rules are "stratified". All the forward rules run. Then when you
ask queries those use the backward rules (including extra backward rules
generated by the forward rules) which expand on the results of the
forward phase.
This approach allowed us to get usable performance for a range of use
cases but with the risk of incomplete results in some cases where the
stratification is wrong. The challenge has always been to make the right
trade-off for the average use cases while leaving the areas of
incompleteness understandable enough that developers can work with it.
Originally sameAs reasoning was done in the backward rules and that
proved unscalable due to limitations of the engine. So the sameAs rules
were moved to the forward phase. Which means that the existing inverseOf
backward phase is missed.
Duplicating the inverseOf reasoning into the forward phase, in the way
you've done, is one way to solve this. Since it's working for you, stick
with it.
The general solution is not so clear since the cost of this simple
approach is that all inverseOf implications are fully materialized in
the forward phase, rather than on demand. This means that people who
don't care about sameAs but do care about inverses may see a performance
hit. Since equality reasoning in jena is really slow then I doubt anyone
is relying on that in production whereas the simple things like
inverseOf may be in use.
An alternative could be to look at augmenting the sameAs rules with some
backward rules which handle the interaction with inverseOf. Should be
possible.
If you'd like to create a ticket for this to track the issue that would
be great. Though no promises how quickly I could look at this.
Dave
