[2.1.3] Reasoner explanations contradicting queries

[paul....@gmail.com]

I've created an example schema for modelling chains of objects. The example is analogous to something I'm aiming to produce but doesn't demonstrate that :l1 might have multiple chain:nextLink links, for example, or that any chain:Link might have multiple chain:prevLink predicates. Here is the ontology in turtle, including definitions of :c, :l1, :l2, :l3:

@prefix owl: <http://www.w3.org/2002/07/owl#> .

@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .

@prefix chain: <http://icio.local/chain/0.0#> .

@prefix : <http://icio.local/test/0.0#> .

 

chain:Chain a owl:Class .

 

chain:Link a owl:Class .

 

chain:inChain a owl:Property ;

    owl:inverseOf chain:hasLink ;

    rdfs:range chain:Chain ;

    rdfs:domain chain:Link ;

    owl:propertyChainAxiom ( chain:linksWith chain:inChain ) .

 

chain:linksWith a owl:TransitiveProperty , owl:SymmetricProperty ;

    rdfs:range chain:Link ;

    rdfs:domain chain:Link .

 

chain:nextLink a owl:Property ;

    rdfs:subPropertyOf chain:linksWith ;

    owl:inverseOf chain:prevLink .

 

:l1 chain:inChain :c ;

    chain:nextLink :l2 .

:l2 chain:nextLink :l3 .

and I can query for the relationships between all-of-the-things:

$ stardog query execute chain -r SL "SELECT * { ?s chain:linksWith ?o } ORDER BY ?s ?o"

+-------+-------+

|   s   |   o   |

+-------+-------+

| :l1   | :l1   |

| :l1   | :l2   |

| :l1   | :l3   |

| :l2   | :l1   |

| :l2   | :l2   |

| :l2   | :l3   |

| :l3   | :l1   |

| :l3   | :l2   |

| :l3   | :l3   |

+-------+-------+

 

$ stardog query execute chain -r SL "SELECT * { ?s chain:hasLink ?o } ORDER BY ?s ?o"

+-------+-------+

|   s   |   o   |

+-------+-------+

| :c    | :l1   |

| :c    | :l2   |

| :c    | :l3   |

+-------+-------+ 

The problem appears then when we try to explain why these assertions are coming out of the system. There appears to be a point of complexity past which the reasoner says the inference is impossible.

$ stardog reasoning explain chain -r SL ":l1 chain:linksWith :l2"

INFERRED

   INFERRED :l1 chain:linksWith :l2

      ASSERTED chain:linksWith a owl:SymmetricProperty

      INFERRED :l2 chain:linksWith :l1

         ASSERTED chain:linksWith a owl:SymmetricProperty

         INFERRED :l1 chain:linksWith :l2

            ASSERTED chain:nextLink rdfs:subPropertyOf chain:linksWith

            ASSERTED :l1 chain:nextLink :l2

   INFERRED :l2 chain:prevLink :l1

      ASSERTED chain:nextLink owl:inverseOf chain:prevLink

 

$ stardog reasoning explain chain -r SL ":l1 chain:linksWith :l1"

Input axiom is not a valid inference; no explanation generated.

 

$ stardog reasoning explain chain -r SL ":l1 chain:linksWith :l3"

Input axiom is not a valid inference; no explanation generated. 

Is there a means of configuring the reasoner to go beyond a certain point of explanation, if indeed that is the problem? Otherwise, what else might it be?

Any insight you can provide would be greatly appreciated.

(Gist of copy-pasta)

Paul

[paul....@gmail.com]

I can confirm this is still the case with Stardog 2.2.

[Evren Sirin]

It is a current limitation that explanations don't work with
transitivity or recursive property chains. However, the output of the
explanation should at least show the partial proof tree. We'll look
into this issue.

Best,
Evren

> --
> -- --
> You received this message because you are subscribed to the C&P "Stardog"
> group.
> To post to this group, send email to sta...@clarkparsia.com
> To unsubscribe from this group, send email to
> stardog+u...@clarkparsia.com
> For more options, visit this group at
> http://groups.google.com/a/clarkparsia.com/group/stardog?hl=en