Add ontology normalizer

This also allows to define ontology approximations to RSA in a simple
way.

3 files changed, 541 insertions, 2 deletions

diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala
index 3777c6b..3da6c8a 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala
@@ -79,7 +79,9 @@ class CanonicalModel(val ontology: RSAOntology) {
       val term = RSAOntology.genFreshVariable()
       val unsafe = ontology.unsafeRoles
       ontology.axioms
-        .map(CanonicalModelConverter.convert(_, term, unsafe, NoSkolem, Empty))
+        .map(a =>
+          CanonicalModelConverter.convert(a, term, unsafe, Constant(a), Empty)
+        )
         .unzip
     }
     (
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
index 0f1552a..42a5b87 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
@@ -99,6 +99,8 @@ class RSAOntology(_ontology: File, val datafiles: File*) {
   private val reasoner =
     (new StructuralReasonerFactory()).createReasoner(ontology)
 
+  private val normalizer = new Normalizer()
+
   /** Imported knowledge base. */
   //lazy val kbase: OWLOntology = {
   //  val merger = new OWLOntologyMerger(manager)
@@ -112,6 +114,7 @@ class RSAOntology(_ontology: File, val datafiles: File*) {
       .tboxAxioms(Imports.INCLUDED)
       .collect(Collectors.toList())
       .collect { case a: OWLLogicalAxiom => a }
+      .flatMap(normalizer.normalize)
   Logger.print(s"Original TBox: ${tbox.length}", Logger.DEBUG)
 
   /** RBox axioms */
@@ -120,6 +123,7 @@ class RSAOntology(_ontology: File, val datafiles: File*) {
       .rboxAxioms(Imports.INCLUDED)
       .collect(Collectors.toList())
       .collect { case a: OWLLogicalAxiom => a }
+      .flatMap(normalizer.normalize)
   Logger.print(s"Original RBox: ${rbox.length}", Logger.DEBUG)
 
   /** ABox axioms
@@ -134,7 +138,8 @@ class RSAOntology(_ontology: File, val datafiles: File*) {
       .aboxAxioms(Imports.INCLUDED)
       .collect(Collectors.toList())
       .collect { case a: OWLLogicalAxiom => a }
-  Logger.print(s"Original RBox: ${abox.length}", Logger.DEBUG)
+      .flatMap(normalizer.normalize)
+  Logger.print(s"Original ABox: ${abox.length}", Logger.DEBUG)
 
   /** Collection of logical axioms in the input ontology */
   lazy val axioms: List[OWLLogicalAxiom] = abox ::: tbox ::: rbox
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/Normalizer.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/Normalizer.scala
new file mode 100644
index 0000000..3c4dd5c
--- /dev/null
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/Normalizer.scala
@@ -0,0 +1,532 @@
+package uk.ac.ox.cs.rsacomb.converter
+
+import org.semanticweb.owlapi.apibinding.OWLManager
+import org.semanticweb.owlapi.model._
+
+import uk.ac.ox.cs.rsacomb.util.Logger
+
+object Normalizer {
+
+  /** Factory used for converting expressions when needed.
+    *
+    * @note most of the time this is used to perform some kind of
+    * normalization on axioms. In later versions it might be worth
+    * moving the normalization code in its own independent step.
+    */
+  private val manager = OWLManager.createOWLOntologyManager()
+  val factory = manager.getOWLDataFactory()
+
+}
+
+class Normalizer() {
+
+  import Normalizer._
+
+  /** Simplify conversion between Java and Scala collections */
+  import uk.ac.ox.cs.rsacomb.implicits.JavaCollections._
+
+  private var counter = -1
+  def freshOWLClass(): OWLClass = factory.getOWLClass(s"X${counter += 1}")
+
+  /** Normalizes a
+    * [[org.semanticweb.owlapi.model.OWLLogicalAxiom OWLLogicalAxiom]]
+    *
+    * @note not all possible axioms are supported. Following is a list
+    * of all unhandled class expressions:
+    * - [[org.semanticweb.owlapi.model.OWLAsymmetricObjectPropertyAxiom OWLAsymmetricObjectPropertyAxiom]]
+    * - [[org.semanticweb.owlapi.model.OWLDatatypeDefinitionAxiom OWLDatatypeDefinitionAxiom]]
+    * - [[org.semanticweb.owlapi.model.OWLDisjointDataPropertiesAxiom OWLDisjointDataPropertiesAxiom]]
+    * - [[org.semanticweb.owlapi.model.OWLDisjointObjectPropertiesAxiom OWLDisjointObjectPropertiesAxiom]]
+    * - [[org.semanticweb.owlapi.model.OWLHasKeyAxiom OWLHasKeyAxiom]]
+    * - [[org.semanticweb.owlapi.model.SWRLRule SWRLRule]]
+    */
+  def normalize(axiom: OWLLogicalAxiom): Seq[OWLLogicalAxiom] =
+    axiom match {
+      case a: OWLSubClassOfAxiom => {
+        val sub = a.getSubClass.getNNF
+        val sup = a.getSuperClass.getNNF
+        (sub, sup) match {
+          /** Split complex subclass axioms
+            *
+            *   C c D -> { C c X, X c D }
+            */
+          case _ if !sub.isOWLClass && !sup.isOWLClass => {
+            val cls = freshOWLClass()
+            Seq(
+              factory.getOWLSubClassOfAxiom(sub, cls),
+              factory.getOWLSubClassOfAxiom(cls, sup)
+            ).flatMap(normalize)
+          }
+          /** Conjunction on the lhs
+            *
+            *   A1 n ... n C n ... n An c D -> { C c X, A1 n ... n X n ... n An c D }
+            */
+          case (sub: OWLObjectIntersectionOf, _)
+              if sub.asConjunctSet.exists(c => !c.isOWLClass) => {
+            var additional = Seq()
+            val conjuncts = sub.asConjunctSet
+            if (conjuncts.length > 0) {
+              val acc = (Seq[OWLClassExpression](), Seq[OWLLogicalAxiom]())
+              val (acc1, acc2) = conjuncts.foldLeft(acc)(
+                { case ((acc1, acc2), conj) =>
+                  if (conj.isOWLClass)
+                    (acc1 :+ conj, acc2)
+                  else {
+                    val cls = freshOWLClass()
+                    (
+                      acc1 :+ cls,
+                      acc2 :+ factory.getOWLSubClassOfAxiom(conj, cls)
+                    )
+                  }
+                }
+              )
+              (acc2 :+ factory.getOWLSubClassOfAxiom(
+                factory.getOWLObjectIntersectionOf(acc1: _*),
+                sup
+              ))
+                .flatMap(normalize)
+            } else {
+              normalize(factory.getOWLSubClassOfAxiom(factory.getOWLThing, sup))
+            }
+          }
+          /** Conjunction on the rhs
+            *
+            *   D c A1 n ... n An -> { D c A1, ... , D c An }
+            */
+          case (_, sup: OWLObjectIntersectionOf) => {
+            val conjuncts = sup.asConjunctSet
+            if (conjuncts.length > 0) {
+              conjuncts
+                .map(cls => factory.getOWLSubClassOfAxiom(sub, cls))
+                .flatMap(normalize)
+            } else {
+              normalize(factory.getOWLSubClassOfAxiom(sub, factory.getOWLThing))
+            }
+          }
+          /** Disjunction on the lhs
+            *
+            *   A1 u ... u An c D -> { A1 c D, ... , An c D }
+            */
+          case (sub: OWLObjectUnionOf, _) => {
+            val disjuncts = sub.asDisjunctSet
+            if (disjuncts.length > 0) {
+              disjuncts
+                .map(cls => factory.getOWLSubClassOfAxiom(cls, sup))
+                .flatMap(normalize)
+            } else {
+              normalize(
+                factory.getOWLSubClassOfAxiom(factory.getOWLNothing, sup)
+              )
+            }
+          }
+          /** Disjunction on the rhs is not supported */
+          case (_, sup: OWLObjectUnionOf) => notInHornALCHOIQ(a)
+          /** Complex class expression on existential restriction on the lhs
+            *
+            *   exists R . C c D -> { C c X, exists R . X c D }
+            */
+          case (sub: OWLObjectSomeValuesFrom, _)
+              if !sub.getFiller.isOWLClass => {
+            val cls = freshOWLClass()
+            Seq(
+              factory.getOWLSubClassOfAxiom(sub.getFiller, cls),
+              factory.getOWLSubClassOfAxiom(
+                factory.getOWLObjectSomeValuesFrom(sub.getProperty, cls),
+                sup
+              )
+            ).flatMap(normalize)
+          }
+          /** Complex class expression on existential restriction on the rhs
+            *
+            *   C c exists R . D -> { X c D, C c exists R . X }
+            */
+          case (_, sup: OWLObjectSomeValuesFrom)
+              if !sup.getFiller.isOWLClass => {
+            val cls = freshOWLClass()
+            Seq(
+              factory.getOWLSubClassOfAxiom(cls, sup.getFiller),
+              factory.getOWLSubClassOfAxiom(
+                sub,
+                factory.getOWLObjectSomeValuesFrom(sup.getProperty, cls)
+              )
+            ).flatMap(normalize)
+          }
+          /** Object/Data universal quantification on the lhs not supported */
+          case (sub: OWLObjectAllValuesFrom, _) => notInHornALCHOIQ(a)
+          case (sub: OWLDataAllValuesFrom, _)   => notInHornALCHOIQ(a)
+          /** Object universal quantification on the rhs
+            *
+            *   C c forall R . D -> exists R- . C c D
+            */
+          case (_, sup: OWLObjectAllValuesFrom) =>
+            normalize(
+              factory.getOWLSubClassOfAxiom(
+                factory
+                  .getOWLObjectSomeValuesFrom(
+                    sup.getProperty.getInverseProperty,
+                    sub
+                  ),
+                sup.getFiller
+              )
+            )
+          /** Object universal quantification on the rhs not supported */
+          case (_, sup: OWLDataAllValuesFrom) => notInHornALCHOIQ(a)
+          /** Exact object/data cardinality restriction on the lhs/rhs
+            *
+            *   = i R . C -> <= i R . C n >= i R . X
+            */
+          case (sub: OWLObjectExactCardinality, _) =>
+            normalize(
+              factory.getOWLSubClassOfAxiom(sub.asIntersectionOfMinMax, sup)
+            )
+          case (sub: OWLDataExactCardinality, _) =>
+            normalize(
+              factory.getOWLSubClassOfAxiom(sub.asIntersectionOfMinMax, sup)
+            )
+          case (_, sup: OWLObjectExactCardinality) =>
+            normalize(
+              factory.getOWLSubClassOfAxiom(sub, sup.asIntersectionOfMinMax)
+            )
+          case (_, sup: OWLDataExactCardinality) =>
+            normalize(
+              factory.getOWLSubClassOfAxiom(sub, sup.asIntersectionOfMinMax)
+            )
+          /** Min object/data cardinality restriction on the lhs/rhs
+            *
+            *   >= 0 R . C -> top
+            *   >= 1 R . C -> exists R . C
+            *
+            * @note not supported when restriction >= 2.
+            */
+          case (sub: OWLObjectMinCardinality, _) =>
+            sub.getCardinality match {
+              case 0 =>
+                normalize(
+                  factory.getOWLSubClassOfAxiom(factory.getOWLThing, sup)
+                )
+              case 1 =>
+                normalize(
+                  factory.getOWLSubClassOfAxiom(
+                    factory.getOWLObjectSomeValuesFrom(
+                      sub.getProperty,
+                      sub.getFiller
+                    ),
+                    sup
+                  )
+                )
+              case _ => notInHornALCHOIQ(a)
+            }
+          case (sub: OWLDataMinCardinality, _) =>
+            sub.getCardinality match {
+              case 0 =>
+                normalize(
+                  factory.getOWLSubClassOfAxiom(factory.getOWLThing, sup)
+                )
+              case 1 =>
+                normalize(
+                  factory.getOWLSubClassOfAxiom(
+                    factory.getOWLDataSomeValuesFrom(
+                      sub.getProperty,
+                      sub.getFiller
+                    ),
+                    sup
+                  )
+                )
+              case _ => notInHornALCHOIQ(a)
+            }
+          case (_, sup: OWLObjectMinCardinality) =>
+            sup.getCardinality match {
+              case 0 => Seq()
+              case 1 =>
+                normalize(
+                  factory.getOWLSubClassOfAxiom(
+                    sub,
+                    factory.getOWLObjectSomeValuesFrom(
+                      sup.getProperty,
+                      sup.getFiller
+                    )
+                  )
+                )
+              case _ => notInHornALCHOIQ(a)
+            }
+          case (_, sup: OWLDataMinCardinality) =>
+            sup.getCardinality match {
+              case 0 => Seq()
+              case 1 =>
+                normalize(
+                  factory.getOWLSubClassOfAxiom(
+                    sub,
+                    factory.getOWLDataSomeValuesFrom(
+                      sup.getProperty,
+                      sup.getFiller
+                    )
+                  )
+                )
+              case _ => notInHornALCHOIQ(a)
+            }
+          /** Max object/data cardinality restriction on the lhs not supported */
+          case (sub: OWLObjectMaxCardinality, _) => notInHornALCHOIQ(a)
+          case (sub: OWLDataMaxCardinality, _)   => notInHornALCHOIQ(a)
+          /** Max object/data cardinality restriction on the rhs
+            *
+            *   C c <= 0 R . D -> C n exists R . D -> bot
+            *   C c <= 1 R . D -> { X c D, C c <= 1 R . D }
+            *
+            * @note not supported when restriction >= 2.
+            */
+          case (_, sup: OWLObjectMaxCardinality) if sup.getCardinality == 0 =>
+            normalize(
+              factory.getOWLSubClassOfAxiom(
+                factory.getOWLObjectIntersectionOf(
+                  sub,
+                  factory
+                    .getOWLObjectSomeValuesFrom(sup.getProperty, sup.getFiller)
+                ),
+                factory.getOWLNothing
+              )
+            )
+          case (_, sup: OWLObjectMaxCardinality)
+              if sup.getCardinality == 1 && !sup.getFiller.isOWLClass => {
+            val cls = freshOWLClass()
+            Seq(
+              factory.getOWLSubClassOfAxiom(cls, sup.getFiller),
+              factory.getOWLSubClassOfAxiom(
+                sub,
+                factory.getOWLObjectMaxCardinality(1, sup.getProperty, cls)
+              )
+            ).flatMap(normalize)
+          }
+          case (_, sup: OWLObjectMaxCardinality) if sup.getCardinality >= 2 =>
+            notInHornALCHOIQ(a)
+          case (_, sup: OWLDataMaxCardinality) if sup.getCardinality == 0 =>
+            normalize(
+              factory.getOWLSubClassOfAxiom(
+                factory.getOWLObjectIntersectionOf(
+                  sub,
+                  factory
+                    .getOWLDataSomeValuesFrom(sup.getProperty, sup.getFiller)
+                ),
+                factory.getOWLNothing
+              )
+            )
+          case (_, sup: OWLDataMaxCardinality) if sup.getCardinality >= 1 =>
+            notInHornALCHOIQ(a)
+          /** HasValue expression on the lhs/rhs
+            *
+            * HasValue(R, a) -> exists R . {a}
+            */
+          case (sub: OWLObjectHasValue, _) =>
+            normalize(
+              factory.getOWLSubClassOfAxiom(
+                factory.getOWLObjectSomeValuesFrom(
+                  sub.getProperty,
+                  factory.getOWLObjectOneOf(sub.getFiller)
+                ),
+                sup
+              )
+            )
+          case (sub: OWLDataHasValue, _) =>
+            normalize(
+              factory.getOWLSubClassOfAxiom(
+                factory.getOWLDataSomeValuesFrom(
+                  sub.getProperty,
+                  factory.getOWLDataOneOf(sub.getFiller)
+                ),
+                sup
+              )
+            )
+          case (_, sup: OWLObjectHasValue) =>
+            normalize(
+              factory.getOWLSubClassOfAxiom(
+                sub,
+                factory.getOWLObjectSomeValuesFrom(
+                  sup.getProperty,
+                  factory.getOWLObjectOneOf(sup.getFiller)
+                )
+              )
+            )
+          case (_, sup: OWLDataHasValue) =>
+            normalize(
+              factory.getOWLSubClassOfAxiom(
+                sub,
+                factory.getOWLDataSomeValuesFrom(
+                  sup.getProperty,
+                  factory.getOWLDataOneOf(sup.getFiller)
+                )
+              )
+            )
+          /** Enumeration of individuals on the lhs
+            *
+            *   {a1, ... ,an} c D -> { D(a1), ..., D(an) }
+            */
+          case (sub: OWLObjectOneOf, _) =>
+            sub.getIndividuals.map(factory.getOWLClassAssertionAxiom(sup, _))
+          /** Enumeration of individuals on the rhs
+            * It's supported only when of cardinality < 2.
+            */
+          case (_, sup: OWLObjectOneOf) if sup.getIndividuals.length == 0 =>
+            normalize(factory.getOWLSubClassOfAxiom(sub, factory.getOWLNothing))
+          case (_, sup: OWLObjectOneOf) if sup.getIndividuals.length > 2 =>
+            notInHornALCHOIQ(a)
+          /** Class complement on the lhs
+            *
+            *   ~C c D -> top c C n D
+            */
+          case (sub: OWLObjectComplementOf, _) =>
+            normalize(
+              factory.getOWLSubClassOfAxiom(
+                factory.getOWLThing,
+                factory.getOWLObjectIntersectionOf(sub.getComplementNNF, sup)
+              )
+            )
+          /** Class complement on the rhs
+            *
+            *   C c ~D -> C n D c bot
+            */
+          case (_, sup: OWLObjectComplementOf) =>
+            normalize(
+              factory.getOWLSubClassOfAxiom(
+                factory.getOWLObjectIntersectionOf(sup.getComplementNNF, sub),
+                factory.getOWLNothing
+              )
+            )
+          /** Axiom is already normalized */
+          case _ => Seq(a)
+        }
+      }
+
+      case a: OWLEquivalentClassesAxiom => {
+        a.getAxiomWithoutAnnotations.asOWLSubClassOfAxioms.flatMap(normalize)
+      }
+
+      case a: OWLEquivalentObjectPropertiesAxiom => {
+        a.getAxiomWithoutAnnotations.asSubObjectPropertyOfAxioms.flatMap(
+          normalize
+        )
+      }
+
+      case a: OWLEquivalentDataPropertiesAxiom => {
+        a.getAxiomWithoutAnnotations.asSubDataPropertyOfAxioms.flatMap(
+          normalize
+        )
+      }
+
+      case a: OWLObjectPropertyDomainAxiom =>
+        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)
+
+      case a: OWLObjectPropertyRangeAxiom =>
+        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)
+
+      case a: OWLDataPropertyDomainAxiom =>
+        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)
+
+      case a: OWLDataPropertyRangeAxiom =>
+        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)
+
+      case a: OWLDisjointClassesAxiom =>
+        a.asPairwiseAxioms.map((a) => {
+          val classes = a.getAxiomWithoutAnnotations.getClassExpressions
+          factory.getOWLSubClassOfAxiom(
+            factory.getOWLObjectIntersectionOf(classes),
+            factory.getOWLNothing
+          )
+        })
+
+      case a: OWLInverseObjectPropertiesAxiom =>
+        a.getAxiomWithoutAnnotations.asSubObjectPropertyOfAxioms.flatMap(
+          normalize
+        )
+
+      case a: OWLFunctionalObjectPropertyAxiom =>
+        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)
+
+      case a: OWLFunctionalDataPropertyAxiom =>
+        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)
+
+      case a: OWLInverseFunctionalObjectPropertyAxiom =>
+        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)
+
+      case a: OWLSymmetricObjectPropertyAxiom =>
+        a.getAxiomWithoutAnnotations.asSubPropertyAxioms.flatMap(normalize)
+
+      case a: OWLDifferentIndividualsAxiom =>
+        a.asPairwiseAxioms.map((a) => {
+          val classes = a.getIndividuals.map(factory.getOWLObjectOneOf(_))
+          factory.getOWLSubClassOfAxiom(
+            factory.getOWLObjectIntersectionOf(classes),
+            factory.getOWLNothing
+          )
+        })
+
+      case a: OWLIrreflexiveObjectPropertyAxiom =>
+        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)
+
+      case a: OWLSameIndividualAxiom =>
+        a.getAxiomWithoutAnnotations.asOWLSubClassOfAxioms.flatMap(normalize)
+
+      case a: OWLDisjointUnionAxiom =>
+        Seq(a.getOWLDisjointClassesAxiom, a.getOWLEquivalentClassesAxiom)
+          .flatMap(normalize)
+
+      /** Complex class assertion
+        *
+        * C(a) -> { X(a), X c C }
+        */
+      case a: OWLClassAssertionAxiom if !a.getClassExpression.isOWLClass => {
+        val cls = freshOWLClass()
+        Seq(
+          factory.getOWLClassAssertionAxiom(cls, a.getIndividual),
+          factory.getOWLSubClassOfAxiom(cls, a.getClassExpression)
+        ).flatMap(normalize)
+      }
+
+      case a: OWLNegativeObjectPropertyAssertionAxiom =>
+        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)
+
+      case a: OWLNegativeDataPropertyAssertionAxiom =>
+        normalize(a.getAxiomWithoutAnnotations.asOWLSubClassOfAxiom)
+
+      /** Not in Horn-ALCHOIQ */
+
+      case a: OWLTransitiveObjectPropertyAxiom => notInHornALCHOIQ(a)
+
+      case a: OWLReflexiveObjectPropertyAxiom => notInHornALCHOIQ(a)
+
+      case a: OWLSubPropertyChainOfAxiom => notInHornALCHOIQ(a)
+
+      /** Unsupported */
+
+      case a: OWLAsymmetricObjectPropertyAxiom => notSupported(a)
+
+      case a: OWLDatatypeDefinitionAxiom => notSupported(a)
+
+      case a: OWLDisjointDataPropertiesAxiom => notSupported(a)
+
+      case a: OWLDisjointObjectPropertiesAxiom => notSupported(a)
+
+      case a: OWLHasKeyAxiom => notSupported(a)
+
+      case a: SWRLRule => notSupported(a)
+
+      /** Axiom is already normalized */
+      case a => Seq(a)
+    }
+
+  /** Approximation function for axioms out of Horn-ALCHOIQ
+    *
+    * By default discards the axiom, which guarantees a lower bound
+    * ontology w.r.t. CQ answering.
+    */
+  protected def notInHornALCHOIQ(
+      axiom: OWLLogicalAxiom
+  ): Seq[OWLLogicalAxiom] = {
+    Logger print s"'$axiom' has been ignored because it is not in Horn-ALCHOIQ"
+    Seq()
+  }
+
+  /** Non supported axioms */
+  private def notSupported(axiom: OWLLogicalAxiom): Seq[OWLLogicalAxiom] =
+    throw new RuntimeException(
+      s"'$axiom' is not currently supported."
+    )
+}