Equality and \top axiomatisation

KRR-Oxford / RSAComb

Re-implementation of the combined approach for CQ answering over RSA ontologies

https://www.cs.ox.ac.uk/isg/tools/RSAComb

Apache License 2.0

2 stars 0 forks source link

Equality and \top axiomatisation #1

Closed dyamon closed 3 years ago

dyamon commented 4 years ago

The RSA check needs additional LP rules:

[x] Equality axiomatization: I thought this could be solved just using RDFox built-in equality features. Still, looking at this it seems like there is no way to both enable the equality feature and use other features like aggregates or negation-as-failure.
[x] \top axiomatization: It seems like RDFox supports owl:Nothing out of the box but it doesn't seem to recognize owl:Thing. It seems weird...
[x] E predicate derivation

dyamon commented 4 years ago

\top axiomatization: We decided to proceed with a simple axiomatisation of \top, as suggested in the paper. According to the documentation it seems to be possible for RDFox to automatically consider owl:Thing as the top class, but we haven't been able to make it work so far. We will keep this as a future optimization.

Equality axiomatization: For now we will settle with a simple axiomatisation of owl:sameAs. The internal equality support is unavailable but enabling owl-in-rdf-support might provide at least an automated axiomatisation of the predicate.

dyamon commented 4 years ago

After we made the switch to using Atom.rdf(..) to create Atoms, the IRI.THING enum entry in JRDFox makes more sense and can be introduced when converting the ontology to logic rules. It might explain why RDFox couldn't axiomatise top directly.

Edit: RDFox still does not axiomatise \top. At least we don't need to introduce a fake \top IRI to simulate owl:Thing

dyamon commented 4 years ago

We decided to put the axiomatisation of owl:sameAs on hold for now and deal only with one for \top (following the procedure proposed by RDFox).

dyamon commented 3 years ago

1) owl:Thing axiomatization has been implemented.

After doing some more research on this it seems that RDFox indeed axiomatise owl:Thing when axioms are given as RDF triples (see here, but in our case we convert triples in Datalog rules, losing RDFox OWL2 built-in support.

2) A first implementation of equality axiomatization has been pushed. At the moment it is introducing owl:sameAs triples (not ideal but needed for the system to work). In the long term it might be better to shift to an internal "equality" predicate that does not interfere with RDFox. At the moment "substitution" rules are also missing and we might need a clever way to introducing them to avoid an esponential explosion of the canonical model.

dyamon commented 3 years ago

Both axiomatisations have being implemented, and equality is handled with a different predicate rsacomb:congruent.