Add unsafety check for ontology roles

The current implementation is still a first attempt and by far not the
most effective. It is still missing some corner cases and extensive
testing.

1 files changed, 39 insertions, 81 deletions

diff --git a/src/main/scala/rsacomb/RSAOntology.scala b/src/main/scala/rsacomb/RSAOntology.scala
index 7fc8781..474d316 100644
--- a/src/main/scala/rsacomb/RSAOntology.scala
+++ b/src/main/scala/rsacomb/RSAOntology.scala
@@ -1,14 +1,11 @@
 package rsacomb
 
 /* Java imports */
-// import java.io.File
 import java.util.stream.{Collectors,Stream}
 
 import org.semanticweb.owlapi.model.OWLOntology
 import org.semanticweb.owlapi.model.OWLObjectPropertyExpression
-// import org.semanticweb.owlapi.model.OWLAxiomVisitorEx
 import org.semanticweb.owlapi.model.parameters.Imports
-// import org.semanticweb.owlapi.reasoner.OWLReasoner
 import org.semanticweb.owlapi.reasoner.structural.StructuralReasonerFactory
 
 import tech.oxfordsemantic.jrdfox.logic.Variable
@@ -16,32 +13,16 @@ import tech.oxfordsemantic.jrdfox.logic.Variable
 /* Scala imports */
 import scala.collection.JavaConverters._
 
-/* Local imports */
-// import rsacomb.RSAAxiom 
-
 /* Debug only */
 import org.semanticweb.owlapi.dlsyntax.renderer.DLSyntaxObjectRenderer
 
-// import java.util.HashMap
-// import java.util.stream.{Stream,Collectors}
-
-// import org.semanticweb.owlapi.model.{AxiomType, ClassExpressionType, OWLObjectSomeValuesFrom}
-// import org.semanticweb.owlapi.model.{OWLSubClassOfAxiom, OWLEquivalentClassesAxiom}
-// import org.semanticweb.owlapi.model.OWLClassExpression
-// import org.semanticweb.owlapi.model.IRI
-// import org.semanticweb.owlapi.reasoner.{OWLReasonerFactory, OWLReasoner}
-// import uk.ac.manchester.cs.owl.owlapi.OWLObjectPropertyImpl
-
-// import tech.oxfordsemantic.jrdfox.Prefixes
-// import tech.oxfordsemantic.jrdfox.client.{ConnectionFactory, ServerConnection, DataStoreConnection}
-// import tech.oxfordsemantic.jrdfox.client.UpdateType
-// import tech.oxfordsemantic.jrdfox.logic.{Rule, Atom, Literal, Term, Variable}
-// import tech.oxfordsemantic.jrdfox.logic.{BuiltinFunctionCall, TupleTableName}
-// import tech.oxfordsemantic.jrdfox.logic.{LogicFormat}
-// import rsacomb.SkolemStrategy
-
+/* Wrapper trait for the implicit class `RSAOntology`.
+ */
 trait RSAOntology {
 
+  /* Implements additional features to reason about RSA ontologies
+   * on top of `OWLOntology` from the OWLAPI.
+   */
   implicit class RSAOntology(ontology: OWLOntology) extends RSAAxiom {
 
     def isRSA: Boolean = {
@@ -79,68 +60,45 @@ trait RSAOntology {
     }
 
     def getUnsafeRoles: List[OWLObjectPropertyExpression] = {
-
+      // The reasoner is used to check unsafety condition for the ontology roles
       val factory = new StructuralReasonerFactory()
       val reasoner = factory.createReasoner(ontology)
-      val tbox = ontology.tboxAxioms(Imports.INCLUDED).collect(Collectors.toList()).asScala
-      val rbox = ontology.rboxAxioms(Imports.INCLUDED).collect(Collectors.toList()).asScala
 
-      /* DEBUG: print rules in DL syntax */
-      val renderer = new DLSyntaxObjectRenderer()
-      println("\nT5 axioms:")
-      for {
-        axiom <- tbox
-        if axiom.isT5
-      } yield println(renderer.render(axiom))
-
-            // def isT3(axiom : OWLAxiom) : Boolean = {
-            // println(axiom)
-            // axiom.getAxiomType match {
-            //     case AxiomType.SUBCLASS_OF => 
-            //     val axiom1 = axiom.asInstanceOf[OWLSubClassOfAxiom]
-            //     axiom1.getSubClass().getClassExpressionType() == ClassExpressionType.OBJECT_SOME_VALUES_FROM &&
-            //         axiom1.getSuperClass().getClassExpressionType() == ClassExpressionType.OWL_CLASS
-            //     case AxiomType.EQUIVALENT_CLASSES => false // TODO
-            // }
-            // }
-
-            // def isT4(axiom : OWLAxiom) : Boolean = {
-            // axiom.getAxiomType match {
-            //     case AxiomType.SUBCLASS_OF => 
-            //     val axiom1 = axiom.asInstanceOf[OWLSubClassOfAxiom]
-            //     axiom1.getSubClass().getClassExpressionType() == ClassExpressionType.OWL_CLASS &&
-            //         axiom1.getSuperClass().getClassExpressionType() == ClassExpressionType.OBJECT_MAX_CARDINALITY
-            //     case AxiomType.EQUIVALENT_CLASSES => false // TODO
-            // }
-            // }
-
-            // def isT5(axiom : OWLAxiom) : Boolean = {
-            // axiom.getAxiomType match {
-            //     case AxiomType.SUBCLASS_OF => {
-            //     val axiom1 = axiom.asInstanceOf[OWLSubClassOfAxiom]
-            //     axiom1.getSubClass().getClassExpressionType() == ClassExpressionType.OWL_CLASS &&
-            //         axiom1.getSuperClass().getClassExpressionType() == ClassExpressionType.OBJECT_SOME_VALUES_FROM
-            //     }
-            //     case AxiomType.EQUIVALENT_CLASSES => false // TODO
-            // }
-            // } 
-
-
-            // println("T3")
-            // for {
-            // axiom <- ontology.tboxAxioms(Imports.INCLUDED)
-            // //role <- axiom.objectPropertiesInSignature()
-            // } yield println(axiom)
-
-            // println("T4")
-            // for {
-            // axiom <- ontology.tboxAxioms(Imports.INCLUDED).filter(isT4)
-            // //role <- axiom.objectPropertiesInSignature()
-            // } yield println(axiom)
+      val tbox = ontology.tboxAxioms(Imports.INCLUDED).collect(Collectors.toSet()).asScala
 
+      /* DEBUG: print rules in DL syntax */
+      //val renderer = new DLSyntaxObjectRenderer()
+
+      /* Checking for (1) unsafety condition:
+       * 
+       *    For all roles p1 appearing in an axiom of type T5, p1 is unsafe
+       *    if there exists a role p2 (different from top) appearing in an axiom
+       *    of type T3 and p1 is a subproperty of the inverse of p2.
+       * 
+       * TODO: We are not checking whether the class expression on the right in T3
+       * is top. For now we can assume it is always the case.
+       */
+      val unsafe = for {
+        ax1 <- tbox
+        if ax1.isT5
+        p1 <- ax1.objectPropertyExpressionsInSignature
+        sup = p1.getInverseProperty +: reasoner.superObjectProperties(p1).map(_.getInverseProperty).collect(Collectors.toList()).asScala
+        ax2 <- tbox
+        if ax2.isT3
+        p2 <- ax2.objectPropertyExpressionsInSignature 
+        if sup.contains(p2)
+      } yield p1
+
+      /* Checking for (2) unsafety condition:
+       *
+       *    TODO
+       */
 
-      /* DEBUG */
-      List()
+      /* TODO: We should be able to avoid this last conversion to List.
+       * Maybe we should just move everything to Sets instead of Lists, since
+       * they have a more straightforward conversion from Java collections.
+       */
+      unsafe.toList
     }
 
   } // implicit class RSAOntology