Hi Dave, thank you for your prompt feedback and great explanation! I'll open a ticket for this case, but in the meantime I'll move on with the inverseOf forward declaration workaround.
Kind regards, Andrea Leofreddi ----- Original Message ----- From: "Dave Reynolds" <[email protected]> To: [email protected] Sent: Thursday, 9 January, 2020 10:16:02 Subject: Re: Missed inference in Jena Fuseki 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
