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.

2 files changed, 142 insertions, 132 deletions

diff --git a/src/main/scala/rsacomb/RSAAxiom.scala b/src/main/scala/rsacomb/RSAAxiom.scala
index 032b7f9..588c72a 100644
--- a/src/main/scala/rsacomb/RSAAxiom.scala
+++ b/src/main/scala/rsacomb/RSAAxiom.scala
@@ -1,76 +1,64 @@
 package rsacomb
 
 /* Java imports */
-// import java.io.File
-// import java.util.stream.{Collectors,Stream}
-
-// import org.semanticweb.owlapi.apibinding.OWLManager
-// import org.semanticweb.owlapi.model.{OWLOntologyManager,OWLOntology}
-// import org.semanticweb.owlapi.model.{OWLAxiom,OWLObjectPropertyExpression}
 import org.semanticweb.owlapi.model.{OWLAxiom,OWLSubClassOfAxiom, OWLEquivalentClassesAxiom}
-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
-
-/* 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.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
-//import org.semanticweb.owlapi.model.{OWLAxiom,OWLObjectPropertyExpression}
+import org.semanticweb.owlapi.model.{OWLObjectPropertyExpression,OWLClass,OWLClassExpression,OWLObjectSomeValuesFrom,OWLObjectMaxCardinality}
+import org.semanticweb.owlapi.model.ClassExpressionType
+import org.semanticweb.owlapi.model.{OWLAxiomVisitorEx,OWLClassExpressionVisitorEx}
 
+/* Wrapper trait for the implicit class `RSAAxiom`.
+ */
 trait RSAAxiom {
 
-  sealed trait RSAAxiomType
-  object RSAAxiomType {
-    case object T3 extends RSAAxiomType
-    case object T4 extends RSAAxiomType
-    case object T5 extends RSAAxiomType
+  /* Identifies some of the axiom types in a Horn-ALCHOIQ ontology
+   * in normal form. Refer to the paper for more details on the
+   * chosen names.
+   */
+  private sealed trait RSAAxiomType
+  private object RSAAxiomType {
+    case object T3 extends RSAAxiomType // ∃R.A ⊑ B
+    case object T4 extends RSAAxiomType // A ⊑ ≤1R.B
+    case object T5 extends RSAAxiomType // A ⊑ ∃R.B
   }
 
+  /* Implements additional features on top of `OWLAxiom` from
+   * the OWLAPI.
+   */
   implicit class RSAAxiom(axiom: OWLAxiom) {
 
+    /* Detecting axiom types:
+     *
+     * In order to reason about role unsafety in Horn-ALCHOIQ
+     * ontologies we need to detect and filter axioms by their
+     * "type".
+     * 
+     * This is a simple implementation following the Visitor
+     * pattern imposed by the OWLAPI.
+     */
     private class RSAAxiomTypeDetector(t: RSAAxiomType)
       extends OWLAxiomVisitorEx[Boolean]
     {
-
       override
       def visit(axiom: OWLSubClassOfAxiom): Boolean = {
-        true
+        val sub = axiom.getSubClass().getClassExpressionType()
+        val sup = axiom.getSuperClass().getClassExpressionType()
+        t match {
+          case RSAAxiomType.T3 => // ∃R.A ⊑ B
+            sub == ClassExpressionType.OBJECT_SOME_VALUES_FROM && sup == ClassExpressionType.OWL_CLASS
+          case RSAAxiomType.T4 => // A ⊑ ≤1R.B
+            sub == ClassExpressionType.OWL_CLASS && sup == ClassExpressionType.OBJECT_MAX_CARDINALITY
+          case RSAAxiomType.T5 => // A ⊑ ∃R.B
+            sub == ClassExpressionType.OWL_CLASS && sup == ClassExpressionType.OBJECT_SOME_VALUES_FROM
+        }
       }
 
       override
       def visit(axiom: OWLEquivalentClassesAxiom): Boolean = {
-        true
+        // TODO
+        false
       }
 
       def doDefault(axiom : OWLAxiom): Boolean = false
-
     }
 
     private def isOfType(t: RSAAxiomType): Boolean = {
@@ -78,9 +66,73 @@ trait RSAAxiom {
       axiom.accept(visitor)
     }
 
+    /* Exposed methods */
     def isT3: Boolean = isOfType(RSAAxiomType.T3)
     def isT4: Boolean = isOfType(RSAAxiomType.T4)
     def isT5: Boolean = isOfType(RSAAxiomType.T5)
+    
+    /* Extracting ObjectPropertyExpressions from axioms
+     *
+     * This extracts all ObjectPropertyExpressions from a given
+     * axiom. While the implementation is generic we use it on axioms
+     * of specific types (see above).
+     * 
+     * NOTE: it is not possible to use the `objectPropertyInSignature`
+     * method of `OWLAxiom` because it returns all "role names" involved
+     * in the signature of an axiom. In particular we won't get the inverse
+     * of a role if this appears in the axiom (but we will get the role
+     * itself instead).
+     */
+    private class RSAAxiomRoleExtractor()
+      extends OWLAxiomVisitorEx[List[OWLObjectPropertyExpression]]
+    {
+
+      private class RSAExprRoleExtractor()
+        extends OWLClassExpressionVisitorEx[List[OWLObjectPropertyExpression]]
+      {
+        override
+        def visit(expr: OWLObjectSomeValuesFrom): List[OWLObjectPropertyExpression] =
+          List(expr.getProperty)
+
+        override
+        def visit(expr: OWLObjectMaxCardinality): List[OWLObjectPropertyExpression] =
+          List(expr.getProperty)
+
+        /* NOTE: this instance of `visit` for `OWLClass` shouldn't be necessary. However
+         * if missing, the code throws a `NullPointerException`. It seems like, for some
+         * reason, `OWLClass` is not really a subinterface of `OWLClassExpression`, as 
+         * stated in the JavaDocs.
+         */
+        override
+        def visit(expr: OWLClass): List[OWLObjectPropertyExpression] =
+          List()
+
+        def doDefault(expr: OWLClassExpression): List[OWLObjectPropertyExpression] =
+          List()
+      }
+
+      override
+      def visit(axiom: OWLSubClassOfAxiom): List[OWLObjectPropertyExpression] = {
+        val visitor = new RSAExprRoleExtractor()
+        val sub = axiom.getSubClass.accept(visitor)
+        val sup = axiom.getSuperClass.accept(visitor)
+        sub ++ sup
+      }
+
+      override
+      def visit(axiom: OWLEquivalentClassesAxiom): List[OWLObjectPropertyExpression] = {
+        // TODO
+        List()
+      }
+
+      def doDefault(axiom : OWLAxiom): List[OWLObjectPropertyExpression] = List()
+    }
+
+    /* Exposed methods */
+    def objectPropertyExpressionsInSignature: List[OWLObjectPropertyExpression] = {
+      val visitor = new RSAAxiomRoleExtractor()
+      axiom.accept(visitor)
+    }
   }
 
-}
+} // trait RSAAxiom
\ No newline at end of file
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