Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

refactor unsat object-checking to leverage object hierarchy, for reasoners that support that #1100

Merged

Conversation

jclerman
Copy link
Contributor

@jclerman jclerman commented Feb 28, 2023

Resolves #1096

  • docs/ have been added/updated - N/A
  • tests have been added/updated
  • mvn verify says all tests pass
  • mvn site says all JavaDocs correct
  • CHANGELOG.md has been updated

Summary

Here, I've modified the way the reasoner validate step checks for unsatisfiable object properties.

Before, an algorithm was implemented (by @cmungall in #133) that was needed for reasoners (like Elk) that don't support computation of the object-property hierarchy. That method is maintained here, but wrapped in a new method ReasonerHelper.getUnsatisfiableObjectProperties(), which uses the old technique only for reasoners that don't report that they can pre-compute the object-property hierarchy.

Reasoners that can pre-compute that hierarchy use a new simpler technique: computation of the object-property hierarchy, followed by checking of the bottom node for any named object-properties other than the OWL bottomObjectProperty - those are unsatisfiable.

Regardless of the technique used, the method returns the unsatisfiable properties to the main validate() method, where they are reported as before.

Testing

I've updated the tests for unsat properties (added as part of #133) to check behavior under the HermiT and Elk reasoners, as representative examples of reasoners that use each of the two main branches of getUnsatisfiableObjectProperties() (before, the tests only covered use of Elk).

…for reasoners that support that

 - also, factoring unsat object-property checking into a separate function
@jclerman jclerman marked this pull request as ready for review February 28, 2023 18:14
Copy link
Contributor

@cmungall cmungall left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I like how you dynamically test the reasoner capabilities in the switch statement rather than hardcoding lists of reasoners. This looks good to merge pending github actions tests

Copy link
Contributor

@matentzn matentzn left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good to me too!

if (unsatPs.size() > 0) {
logger.error("There are {} unsatisfiable properties in the ontology.", unsatPs.size());
for (OWLObjectProperty p : unsatPs) {
logger.error(" unsatisfiable property: " + p.getIRI());
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Isnt this log output redundant with the one in the end of getUnsatisfiableObjectProperties?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks @matentzn - yes indeed. Fixed in a new commit.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice :)

@jamesaoverton
Copy link
Member

Sorry for the long delay with this. The code looks good and I got major speed improvements in my tests. Thanks!

@jamesaoverton jamesaoverton merged commit ec9c562 into ontodev:master May 3, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Consider more-performant alternatives to ROBOT's "Checking for unsatisfiable [classes/object properties]"?
4 participants