[owlapi] incomplete complex assertion to KB transformation.

[irina-dragoste]

For an OWL ontology containing (only) the following complex assertion

ClassAssertion(ObjectSomeValuesFrom(<a> <b>) <c>)

OwlToRulesConverter generates a kb with an empty set of facts and the single rule

a(c, !Y1), b(!Y1) :- <http://www.w3.org/2002/07/owl#Thing>(c) .

As our reasoner is agnostic of the fact that <http://www.w3.org/2002/07/owl#Thing>(x) is true for any individual x, a complete transformation must also produce the fact <http://www.w3.org/2002/07/owl#Thing>(c) ..

Find attached a java class with code that reproduces the bug (in .txt format)

[mkroetzsch]

Do we actually ever produce any owl:Thing facts for individuals? If we want completeness w.r.t. owl:Thing, we would also need to add further facts of this kind ... Probably the converter should also clarify in its documentation what the expected behaviour is; maybe completness w.r.t. to owl:Thing is not desirable anyway (too many facts); but cases like in this bug should of course be covered..

[irina-dragoste]

Do we actually ever produce any owl:Thing facts for individuals? If we want completeness w.r.t. owl:Thing, we would also need to add further facts of this kind ... Probably the converter should also clarify in its documentation what the expected behaviour is; maybe completness w.r.t. to owl:Thing is not desirable anyway (too many facts); but cases like in this bug should of course be covered..

Indeed, we never create any owl:Thing facts. We only use owl:Thing for rules with empty bodies and owl:Nothing for rules with empty heads. Is this intended? Are we supposed to clarify in the documentation that the ontology provider has the responsibility to ensure completeness w.r to owl:Thing? (for example, creating axioms that insure that each class in the ontology is a subclass of owl:Thing, and each role has domain and range owl:Thing)?

[francesco-kriegel]

Wouldn't it be a fix to allow for rules with an empty body? Then one could translate the problematic OWL class assertion into the rule a(c, !Y1), b(!Y1) :- .. According to your IJCAR2018 paper "Efficient Model Construction for Horn Logic with VLog" such rules should be supported, but the Rulewerk grammar only allows to construct rules the bodies of which contain at least one literal.

There is also a difference in the treatment of the notion "fact". In the IJCAR2018 paper a fact is a rule with an empty body. Thus a(c, !Y1), b(!Y1) :- . (or even a(c, !Y1), b(!Y1) .) should be legal fact. The rulewerk grammar only supports facts in which all terms are constants.