5 files changed, 532 insertions, 241 deletions

diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/Main.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/Main.scala
index f9de801..b749401 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/Main.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/Main.scala
@@ -106,12 +106,11 @@ object RSAComb extends App {
   /* Command-line options */
   val config = RSAConfig.parse(args.toList)
 
-  val ontology = RSAOntology(
+  val rsa = RSAOntology(
     config('ontology).get[File],
-    config('data).get[List[File]]: _*
+    config('data).get[List[File]],
+    None
   )
-  val rsa = ontology.toRSA()
-  ontology.statistics()
 
   if (config contains 'query) {
     val query =
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 0e10f89..bbbbcf3 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
@@ -50,13 +50,13 @@ import scala.collection.JavaConverters._
 import scala.collection.mutable.{Set, Map}
 import scalax.collection.Graph
 import scalax.collection.GraphPredef._, scalax.collection.GraphEdge._
-import scalax.collection.GraphTraversal._
 
 /* Debug only */
 import org.semanticweb.owlapi.dlsyntax.renderer.DLSyntaxObjectRenderer
 import tech.oxfordsemantic.jrdfox.logic._
 import org.semanticweb.owlapi.model.OWLObjectInverseOf
 
+import uk.ac.ox.cs.rsacomb.approximation.Approximation
 import uk.ac.ox.cs.rsacomb.converter._
 import uk.ac.ox.cs.rsacomb.filtering.{FilteringProgram, FilterType}
 import uk.ac.ox.cs.rsacomb.suffix._
@@ -64,29 +64,189 @@ import uk.ac.ox.cs.rsacomb.sparql._
 import uk.ac.ox.cs.rsacomb.util.{RDFoxUtil, RSA}
 import uk.ac.ox.cs.rsacomb.util.Logger
 
+object RSAUtil {
+
+  // implicit def axiomsToOntology(axioms: Seq[OWLAxiom]) = {
+  //   val manager = OWLManager.createOWLOntologyManager()
+  //   manager.createOntology(axioms.asJava)
+  // }
+
+  /** Compute the RSA dependency graph for a set of axioms
+    *
+    * @return a tuple containing the dependency graph and a map between
+    * the newly introduced constants and the corresponding input axioms.
+    *
+    * @note no check on the ontology language is performed since the
+    * construction of the dependency graph is computed regardless. The
+    * input axioms are assumed to be normalized.
+    */
+  def dependencyGraph(
+      axioms: List[OWLLogicalAxiom],
+      datafiles: List[File]
+  ): (Graph[Resource, DiEdge], Map[String, OWLAxiom]) = {
+    val unsafe = RSAOntology(axioms, datafiles).unsafeRoles
+    var nodemap = Map.empty[String, OWLAxiom]
+
+    object RSAConverter extends RDFoxConverter {
+
+      override def convert(
+          expr: OWLClassExpression,
+          term: Term,
+          unsafe: List[OWLObjectPropertyExpression],
+          skolem: SkolemStrategy,
+          suffix: RSASuffix
+      ): Shards =
+        (expr, skolem) match {
+
+          case (e: OWLObjectSomeValuesFrom, c: Constant) => {
+            nodemap.update(c.iri.getIRI, c.axiom)
+            val (res, ext) = super.convert(e, term, unsafe, skolem, suffix)
+            if (unsafe contains e.getProperty)
+              (RSA.PE(term, c.iri) :: RSA.U(c.iri) :: res, ext)
+            else
+              (RSA.PE(term, c.iri) :: res, ext)
+          }
+
+          case (e: OWLDataSomeValuesFrom, c: Constant) => {
+            nodemap.update(c.iri.getIRI, c.axiom)
+            val (res, ext) = super.convert(e, term, unsafe, skolem, suffix)
+            if (unsafe contains e.getProperty)
+              (RSA.PE(term, c.iri) :: RSA.U(c.iri) :: res, ext)
+            else
+              (RSA.PE(term, c.iri) :: res, ext)
+          }
+
+          case _ => super.convert(expr, term, unsafe, skolem, suffix)
+        }
+    }
+
+    /* Ontology convertion into LP rules */
+    val term = RSAOntology.genFreshVariable()
+    val result = axioms.map(a =>
+      RSAConverter.convert(a, term, unsafe, new Constant(a), Empty)
+    )
+
+    val datalog = result.unzip
+    val facts = datalog._1.flatten
+    var rules = datalog._2.flatten
+
+    /* Open connection with RDFox */
+    val (server, data) = RDFoxUtil.openConnection("rsa_dependency_graph")
+
+    /* Add additional built-in rules */
+    val varX = Variable.create("X")
+    val varY = Variable.create("Y")
+    rules = Rule.create(
+      RSA.E(varX, varY),
+      RSA.PE(varX, varY),
+      RSA.U(varX),
+      RSA.U(varY)
+    ) :: rules
+    /* Load facts and rules from ontology */
+    RDFoxUtil.addFacts(data, facts)
+    RDFoxUtil.addRules(data, rules)
+    /* Load data files */
+    RDFoxUtil.addData(data, datafiles: _*)
+
+    /* Build the graph */
+    val query = "SELECT ?X ?Y WHERE { ?X rsa:E ?Y }"
+    val answers = RDFoxUtil.submitQuery(data, query, RSA.Prefixes).get
+    var edges: Seq[DiEdge[Resource]] =
+      answers.collect { case (_, Seq(n1, n2)) => n1 ~> n2 }
+    val graph = Graph(edges: _*)
+
+    /* Close connection to RDFox */
+    RDFoxUtil.closeConnection(server, data)
+
+    (graph, nodemap)
+  }
+}
+
 object RSAOntology {
 
+  import uk.ac.ox.cs.rsacomb.implicits.JavaCollections._
+
+  /** Manager instance to interface with OWLAPI */
+  val manager = OWLManager.createOWLOntologyManager()
+  val factory = manager.getOWLDataFactory()
+
   /** Name of the RDFox data store used for CQ answering */
   private val DataStore = "answer_computation"
 
-  /** Simple fresh variable generator */
+  /** Simple fresh variable/class generator */
   private var counter = -1;
   def genFreshVariable(): Variable = {
     counter += 1
     Variable.create(f"I$counter%05d")
   }
+  def getFreshOWLClass(): OWLClass = {
+    counter += 1
+    factory.getOWLClass(s"X$counter")
+  }
 
-  /** Manager instance to interface with OWLAPI */
-  val manager = OWLManager.createOWLOntologyManager()
+  def apply(
+      axioms: List[OWLLogicalAxiom],
+      datafiles: List[File]
+  ): RSAOntology = new RSAOntology(axioms, datafiles: _*)
+
+  def apply(
+      ontofile: File,
+      datafiles: List[File],
+      approx: Option[Approximation]
+  ): RSAOntology = {
+    val ontology = manager.loadOntologyFromOntologyDocument(ontofile)
+    RSAOntology(ontology, datafiles, approx)
+  }
+
+  def apply(
+      ontology: OWLOntology,
+      datafiles: List[File],
+      approx: Option[Approximation]
+  ): RSAOntology = {
+    val normalizer = new Normalizer()
+
+    /** TBox axioms */
+    var tbox: List[OWLLogicalAxiom] =
+      ontology
+        .tboxAxioms(Imports.INCLUDED)
+        .collect(Collectors.toList())
+        .collect { case a: OWLLogicalAxiom => a }
+        .flatMap(normalizer.normalize)
+
+    /** RBox axioms */
+    var rbox: List[OWLLogicalAxiom] =
+      ontology
+        .rboxAxioms(Imports.INCLUDED)
+        .collect(Collectors.toList())
+        .collect { case a: OWLLogicalAxiom => a }
+        .flatMap(normalizer.normalize)
+
+    /** ABox axioms
+      *
+      * @note this represents only the set of assertions contained in the
+      * ontology file. Data files specified in `datafiles` are directly
+      * imported in RDFox due to performance issues when trying to import
+      * large data files via OWLAPI.
+      */
+    var abox: List[OWLLogicalAxiom] =
+      ontology
+        .aboxAxioms(Imports.INCLUDED)
+        .collect(Collectors.toList())
+        .collect { case a: OWLLogicalAxiom => a }
+        .flatMap(normalizer.normalize)
+
+    /** Collection of logical axioms in the input ontology */
+    var axioms: List[OWLLogicalAxiom] = abox ::: tbox ::: rbox
 
-  def apply(ontology: File, data: File*): RSAOntology =
     new RSAOntology(
-      manager.loadOntologyFromOntologyDocument(ontology),
-      data: _*
+      approx match {
+        case Some(a) => a.approximate(axioms, datafiles)
+        case None    => axioms
+      },
+      datafiles: _*
     )
+  }
 
-  def apply(ontology: OWLOntology, data: File*): RSAOntology =
-    new RSAOntology(ontology, data: _*)
 }
 
 /** Wrapper class for an ontology in RSA
@@ -94,59 +254,21 @@ object RSAOntology {
   * @param ontology the input OWL2 ontology.
   * @param datafiles additinal data (treated as part of the ABox)
   */
-class RSAOntology(val original: OWLOntology, val datafiles: File*) {
+class RSAOntology(val axioms: List[OWLLogicalAxiom], val datafiles: File*) {
 
   /** Simplify conversion between OWLAPI and RDFox concepts */
   import implicits.RDFox._
   import uk.ac.ox.cs.rsacomb.implicits.RSAAxiom._
+
+  /** Simplify conversion between Java and Scala collections */
   import uk.ac.ox.cs.rsacomb.implicits.JavaCollections._
 
   /** Set of axioms removed during the approximation to RSA */
   private var removed: Seq[OWLAxiom] = Seq.empty
 
-  /** The normalizer normalizes the ontology and approximate it to
-    * Horn-ALCHOIQ. A further step is needed to obtain an RSA
-    * approximation of the input ontology `original`.
-    */
-  private val normalizer = new Normalizer()
-
-  /** TBox axioms */
-  var tbox: List[OWLLogicalAxiom] =
-    original
-      .tboxAxioms(Imports.INCLUDED)
-      .collect(Collectors.toList())
-      .collect { case a: OWLLogicalAxiom => a }
-      .flatMap(normalizer.normalize)
-
-  /** RBox axioms */
-  var rbox: List[OWLLogicalAxiom] =
-    original
-      .rboxAxioms(Imports.INCLUDED)
-      .collect(Collectors.toList())
-      .collect { case a: OWLLogicalAxiom => a }
-      .flatMap(normalizer.normalize)
-
-  /** ABox axioms
-    *
-    * @note this represents only the set of assertions contained in the
-    * ontology file. Data files specified in `datafiles` are directly
-    * imported in RDFox due to performance issues when trying to import
-    * large data files via OWLAPI.
-    */
-  var abox: List[OWLLogicalAxiom] =
-    original
-      .aboxAxioms(Imports.INCLUDED)
-      .collect(Collectors.toList())
-      .collect { case a: OWLLogicalAxiom => a }
-      .flatMap(normalizer.normalize)
-
-  /** Collection of logical axioms in the input ontology */
-  var axioms: List[OWLLogicalAxiom] = abox ::: tbox ::: rbox
-
   /** Normalized Horn-ALCHOIQ ontology */
-  val ontology = RSAOntology.manager.createOntology(
-    axioms.asInstanceOf[List[OWLAxiom]].asJava
-  )
+  val ontology =
+    RSAOntology.manager.createOntology((axioms: List[OWLAxiom]).asJava)
 
   /** OWLAPI internal reasoner instantiated over the approximated ontology */
   private val reasoner =
@@ -170,7 +292,7 @@ class RSAOntology(val original: OWLOntology, val datafiles: File*) {
   val concepts: List[OWLClass] =
     ontology.getClassesInSignature().asScala.toList
   val roles: List[OWLObjectPropertyExpression] =
-    (tbox ++ rbox)
+    axioms
       .flatMap(_.objectPropertyExpressionsInSignature)
       .distinct
 
@@ -190,12 +312,12 @@ class RSAOntology(val original: OWLOntology, val datafiles: File*) {
 
     /* Checking for unsafety condition (1) */
     val unsafe1 = for {
-      axiom <- tbox
+      axiom <- axioms
       if axiom.isT5
       role1 <- axiom.objectPropertyExpressionsInSignature
       roleSuper = role1 +: reasoner.superObjectProperties(role1)
       roleSuperInv = roleSuper.map(_.getInverseProperty)
-      axiom <- tbox
+      axiom <- axioms
       if axiom.isT3 && !axiom.isT3top
       role2 <- axiom.objectPropertyExpressionsInSignature
       if roleSuperInv contains role2
@@ -203,12 +325,12 @@ class RSAOntology(val original: OWLOntology, val datafiles: File*) {
 
     /* Checking for unsafety condition (2) */
     val unsafe2 = for {
-      axiom <- tbox
+      axiom <- axioms
       if axiom.isT5
       role1 <- axiom.objectPropertyExpressionsInSignature
       roleSuper = role1 +: reasoner.superObjectProperties(role1)
       roleSuperInv = roleSuper.map(_.getInverseProperty)
-      axiom <- tbox
+      axiom <- axioms
       if axiom.isT4
       role2 <- axiom.objectPropertyExpressionsInSignature
       if roleSuper.contains(role2) || roleSuperInv.contains(role2)
@@ -217,93 +339,6 @@ class RSAOntology(val original: OWLOntology, val datafiles: File*) {
     unsafe1 ++ unsafe2
   }
 
-  /** Compute the RSA dependency graph
-    *
-    * This is used to approximate the input ontology to RSA.
-    *
-    * @return a tuple containing the dependency graph and a map between
-    * the constants newly introduced and the corresponding axioms in the
-    * ontology.
-    */
-  private def dependencyGraph()
-      : (Graph[Resource, DiEdge], Map[String, OWLAxiom]) = {
-    val unsafe = this.unsafeRoles
-    var nodemap = Map.empty[String, OWLAxiom]
-
-    object RSAConverter extends RDFoxConverter {
-
-      override def convert(
-          expr: OWLClassExpression,
-          term: Term,
-          unsafe: List[OWLObjectPropertyExpression],
-          skolem: SkolemStrategy,
-          suffix: RSASuffix
-      ): Shards =
-        (expr, skolem) match {
-
-          case (e: OWLObjectSomeValuesFrom, c: Constant) => {
-            nodemap.update(c.iri.getIRI, c.axiom)
-            val (res, ext) = super.convert(e, term, unsafe, skolem, suffix)
-            if (unsafe contains e.getProperty)
-              (RSA.PE(term, c.iri) :: RSA.U(c.iri) :: res, ext)
-            else
-              (RSA.PE(term, c.iri) :: res, ext)
-          }
-
-          case (e: OWLDataSomeValuesFrom, c: Constant) => {
-            nodemap.update(c.iri.getIRI, c.axiom)
-            val (res, ext) = super.convert(e, term, unsafe, skolem, suffix)
-            if (unsafe contains e.getProperty)
-              (RSA.PE(term, c.iri) :: RSA.U(c.iri) :: res, ext)
-            else
-              (RSA.PE(term, c.iri) :: res, ext)
-          }
-
-          case _ => super.convert(expr, term, unsafe, skolem, suffix)
-        }
-    }
-
-    /* Ontology convertion into LP rules */
-    val term = RSAOntology.genFreshVariable()
-    val result = axioms.map(a =>
-      RSAConverter.convert(a, term, unsafe, new Constant(a), Empty)
-    )
-
-    val datalog = result.unzip
-    val facts = datalog._1.flatten
-    var rules = datalog._2.flatten
-
-    /* Open connection with RDFox */
-    val (server, data) = RDFoxUtil.openConnection("rsa_dependency_graph")
-
-    /* Add additional built-in rules */
-    val varX = Variable.create("X")
-    val varY = Variable.create("Y")
-    rules = Rule.create(
-      RSA.E(varX, varY),
-      RSA.PE(varX, varY),
-      RSA.U(varX),
-      RSA.U(varY)
-    ) :: rules
-    /* Load facts and rules from ontology */
-    RDFoxUtil.addFacts(data, facts)
-    RDFoxUtil.addRules(data, rules)
-    /* Load data files */
-    RDFoxUtil.addData(data, datafiles: _*)
-
-    /* Build the graph */
-    val query = "SELECT ?X ?Y WHERE { ?X rsa:E ?Y }"
-    val answers = RDFoxUtil.submitQuery(data, query, RSA.Prefixes).get
-    var edges: Seq[DiEdge[Resource]] =
-      answers.collect { case (_, Seq(n1, n2)) => n1 ~> n2 }
-    val graph = Graph(edges: _*)
-
-    /* Close connection to RDFox */
-    RDFoxUtil.closeConnection(server, data)
-
-    (graph, nodemap)
-  }
-
   /** Approximate a Horn-ALCHOIQ ontology to RSA
     *
     * This is done by gathering those axioms that prevent the ontology
@@ -313,61 +348,61 @@ class RSAOntology(val original: OWLOntology, val datafiles: File*) {
     * @param graph the graph used to compute the axioms to remove.
     * @param nodemap map from graph nodes to ontology axioms.
     */
-  def toRSA(): RSAOntology = Logger.timed(
-    {
-
-      /* Compute the dependency graph for the ontology */
-      val (graph, nodemap) = this.dependencyGraph()
-
-      /* Define node colors for the graph visit */
-      sealed trait NodeColor
-      case object Unvisited extends NodeColor
-      case object Visited extends NodeColor
-      case object ToDelete extends NodeColor
-
-      /* Keep track of node colors during graph visit */
-      var color = Map.from[Resource, NodeColor](
-        graph.nodes.toOuter.map(k => (k, Unvisited))
-      )
-
-      for {
-        component <- graph.componentTraverser().map(_ to Graph)
-        edge <- component
-          .outerEdgeTraverser(component.nodes.head)
-          .withKind(BreadthFirst)
-      } yield {
-        val source = edge._1
-        val target = edge._2
-        color(source) match {
-          case Unvisited | Visited => {
-            color(target) match {
-              case Unvisited =>
-                color(source) = Visited;
-                color(target) = Visited
-              case Visited =>
-                color(source) = ToDelete
-              case ToDelete =>
-                color(source) = Visited
-            }
-          }
-          case ToDelete =>
-        }
-      }
-
-      val toDelete = color.iterator.collect { case (resource: IRI, ToDelete) =>
-        nodemap(resource.getIRI)
-      }.toSeq
-
-      /* Remove axioms from approximated ontology */
-      ontology.removeAxioms(toDelete: _*)
-      this.removed = toDelete
-
-      /* Return RSA ontology */
-      RSAOntology(ontology, datafiles: _*)
-    },
-    "Horn-ALCHOIQ to RSA approximation:",
-    Logger.DEBUG
-  )
+  // def toRSA(): RSAOntology = Logger.timed(
+  //   {
+
+  //     /* Compute the dependency graph for the ontology */
+  //     val (graph, nodemap) = this.dependencyGraph()
+
+  //     /* Define node colors for the graph visit */
+  //     sealed trait NodeColor
+  //     case object Unvisited extends NodeColor
+  //     case object Visited extends NodeColor
+  //     case object ToDelete extends NodeColor
+
+  //     /* Keep track of node colors during graph visit */
+  //     var color = Map.from[Resource, NodeColor](
+  //       graph.nodes.toOuter.map(k => (k, Unvisited))
+  //     )
+
+  //     for {
+  //       component <- graph.componentTraverser().map(_ to Graph)
+  //       edge <- component
+  //         .outerEdgeTraverser(component.nodes.head)
+  //         .withKind(BreadthFirst)
+  //     } yield {
+  //       val source = edge._1
+  //       val target = edge._2
+  //       color(source) match {
+  //         case Unvisited | Visited => {
+  //           color(target) match {
+  //             case Unvisited =>
+  //               color(source) = Visited;
+  //               color(target) = Visited
+  //             case Visited =>
+  //               color(source) = ToDelete
+  //             case ToDelete =>
+  //               color(source) = Visited
+  //           }
+  //         }
+  //         case ToDelete =>
+  //       }
+  //     }
+
+  //     val toDelete = color.iterator.collect { case (resource: IRI, ToDelete) =>
+  //       nodemap(resource.getIRI)
+  //     }.toSeq
+
+  //     /* Remove axioms from approximated ontology */
+  //     ontology.removeAxioms(toDelete: _*)
+  //     this.removed = toDelete
+
+  //     /* Return RSA ontology */
+  //     RSAOntology(ontology, datafiles: _*)
+  //   },
+  //   "Horn-ALCHOIQ to RSA approximation:",
+  //   Logger.DEBUG
+  // )
   // val edges1 = Seq('A ~> 'B, 'B ~> 'C, 'C ~> 'D, 'D ~> 'H, 'H ~>
   // 'G, 'G ~> 'F, 'E ~> 'A, 'E ~> 'F, 'B ~> 'E, 'F ~> 'G, 'B ~> 'F,
   // 'C ~> 'G, 'D ~> 'C, 'H ~> 'D)
@@ -651,7 +686,7 @@ class RSAOntology(val original: OWLOntology, val datafiles: File*) {
     val conflR = this.confl(roleR)
     // We just need the TBox to find
     val terms = for {
-      axiom1 <- tbox
+      axiom1 <- axioms
       if axiom1.isT5
       // We expect only one role coming out of a T5 axiom
       roleS <- axiom1.objectPropertyExpressionsInSignature
@@ -676,28 +711,28 @@ class RSAOntology(val original: OWLOntology, val datafiles: File*) {
     this.self(axiom) | this.cycle(axiom)
 
   /** Log normalization/approximation statistics */
-  def statistics(level: Logger.Level = Logger.DEBUG): Unit = {
-    Logger.print(
-      s"Logical axioms in original input ontology: ${original.getLogicalAxiomCount(true)}",
-      level
-    )
-    Logger.print(
-      s"Logical axioms discarded in Horn-ALCHOIQ approximation: ${normalizer.discarded}",
-      level
-    )
-    Logger.print(
-      s"Logical axioms shifted in Horn-ALCHOIQ approximation: ${normalizer.shifted}",
-      level
-    )
-    Logger.print(
-      s"Logical axioms in Horn-ALCHOIQ ontology: ${ontology
-        .getLogicalAxiomCount(true)} (${tbox.length}/${rbox.length}/${abox.length})",
-      level
-    )
-    Logger.print(
-      s"Logical axioms discarded in RSA approximation: ${removed.length}",
-      level
-    )
-  }
+  // def statistics(level: Logger.Level = Logger.DEBUG): Unit = {
+  //   Logger.print(
+  //     s"Logical axioms in original input ontology: ${original.getLogicalAxiomCount(true)}",
+  //     level
+  //   )
+  //   Logger.print(
+  //     s"Logical axioms discarded in Horn-ALCHOIQ approximation: ${normalizer.discarded}",
+  //     level
+  //   )
+  //   Logger.print(
+  //     s"Logical axioms shifted in Horn-ALCHOIQ approximation: ${normalizer.shifted}",
+  //     level
+  //   )
+  //   Logger.print(
+  //     s"Logical axioms in Horn-ALCHOIQ ontology: ${ontology
+  //       .getLogicalAxiomCount(true)} (${axioms.length}/${axioms.length}/${axioms.length})",
+  //     level
+  //   )
+  //   Logger.print(
+  //     s"Logical axioms discarded in RSA approximation: ${removed.length}",
+  //     level
+  //   )
+  // }
 
 } // class RSAOntology
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/approximation/approximation.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/approximation/approximation.scala
new file mode 100644
index 0000000..1b49413
--- /dev/null
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/approximation/approximation.scala
@@ -0,0 +1,19 @@
+package uk.ac.ox.cs.rsacomb.approximation
+
+import java.io.File
+import org.semanticweb.owlapi.model.OWLLogicalAxiom
+
+/** Ontology approximation technique. */
+trait Approximation {
+
+  /** Approximate an ontology.
+    *
+    * @param ontology input ontology
+    * @return a new approximated ontology
+    */
+  def approximate(
+      ontology: List[OWLLogicalAxiom],
+      datafiles: List[File]
+  ): List[OWLLogicalAxiom]
+
+}
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/approximation/lowerbound.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/approximation/lowerbound.scala
new file mode 100644
index 0000000..8a86d19
--- /dev/null
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/approximation/lowerbound.scala
@@ -0,0 +1,241 @@
+package uk.ac.ox.cs.rsacomb.approximation
+
+import java.io.File
+
+import org.semanticweb.owlapi.apibinding.OWLManager
+import org.semanticweb.owlapi.model.{IRI => _, _}
+
+import tech.oxfordsemantic.jrdfox.logic.expression.{Resource, IRI}
+
+import scala.collection.mutable.{Set, Map}
+import scalax.collection.Graph
+import scalax.collection.GraphPredef._, scalax.collection.GraphEdge._
+import scalax.collection.GraphTraversal._
+
+import uk.ac.ox.cs.rsacomb.RSAOntology
+import uk.ac.ox.cs.rsacomb.RSAUtil
+import uk.ac.ox.cs.rsacomb.converter.Normalizer
+
+/** Approximation algorithm that mantains soundness for CQ answering.
+  *
+  * The input OWL 2 ontology is assumed to be normalized and the output
+  * ontology is guaranteed to be in RSA.
+  *
+  * The algorithm is performed in three steps:
+  * 1. the ontology is reduced to ALCHOIQ by discarding any axiom
+  *    that is not in the language;
+  * 2. the ontology is further reduced to Horn-ALCHOIQ by shifting
+  *    axioms with disjunction on the rhs;
+  * 3. the ontology is approximated to RSA by manipulating its
+  *    dependency graph.
+  *
+  * @see [[uk.ac.ox.cs.rsacomb.converter.Normalizer]]
+  */
+class LowerBound extends Approximation {
+
+  /** Simplify conversion between Java and Scala collections */
+  import uk.ac.ox.cs.rsacomb.implicits.JavaCollections._
+
+  /** Simplify conversion between OWLAPI and RDFox concepts */
+  import uk.ac.ox.cs.rsacomb.implicits.RDFox._
+
+  /** Manager instance to interface with OWLAPI */
+  val manager = OWLManager.createOWLOntologyManager()
+  val factory = manager.getOWLDataFactory()
+
+  val normalizer = new Normalizer()
+
+  /** Main entry point for the approximation algorithm */
+  def approximate(
+      ontology: List[OWLLogicalAxiom],
+      datafiles: List[File]
+  ): List[OWLLogicalAxiom] = {
+    /* Normalize axioms */
+    val axioms1 = ontology flatMap normalizer.normalize
+    /* Delete any axiom outside of ALCHOIQ */
+    val axioms2 = axioms1 filterNot inALCHOIQ
+    /* Shift any axiom with disjunction on the rhs */
+    val axioms3 = for {
+      a1 <- axioms1
+      a2 <- shift(a1)
+      a3 <- normalizer.normalize(a2)
+    } yield a3
+    /* Approximate to RSA */
+    toRSA(axioms3, datafiles)
+  }
+
+  /** Discards all axioms outside ALCHOIQ */
+  def inALCHOIQ(axiom: OWLLogicalAxiom): Boolean =
+    axiom match {
+      case a: OWLSubClassOfAxiom => {
+        val sub = a.getSubClass.getNNF
+        val sup = a.getSuperClass.getNNF
+        (sub, sup) match {
+          case (sub: OWLObjectAllValuesFrom, _) => false
+          case (sub: OWLDataAllValuesFrom, _)   => false
+          case (_, sup: OWLDataAllValuesFrom)   => false
+          case (sub: OWLObjectMinCardinality, _) if sub.getCardinality >= 2 =>
+            false
+          case (sub: OWLDataMinCardinality, _) if sub.getCardinality >= 2 =>
+            false
+          case (_, sup: OWLObjectMinCardinality) if sup.getCardinality >= 2 =>
+            false
+          case (_, sup: OWLDataMinCardinality) if sup.getCardinality >= 2 =>
+            false
+          case (sub: OWLObjectMaxCardinality, _) => false
+          case (sub: OWLDataMaxCardinality, _)   => false
+          case (_, sup: OWLObjectMaxCardinality) if sup.getCardinality >= 2 =>
+            false
+          case (_, sup: OWLDataMaxCardinality) if sup.getCardinality >= 1 =>
+            false
+          case (_, sup: OWLObjectOneOf) if sup.getIndividuals.length > 2 =>
+            false
+          case (sub: OWLObjectHasSelf, _) => false
+          case (_, sup: OWLObjectHasSelf) => false
+          case _                          => true
+        }
+      }
+      case a: OWLTransitiveObjectPropertyAxiom => false
+      case a: OWLReflexiveObjectPropertyAxiom  => false
+      case a: OWLSubPropertyChainOfAxiom       => false
+      case a: OWLAsymmetricObjectPropertyAxiom => false
+      case a                                   => true
+    }
+
+  /** Shifting axioms with disjunction on the rhs.
+    *
+    * The process of shifting presenves soundness but completenes w.r.t.
+    * CQ answering is lost.
+    *
+    * @example
+    *
+    *   A -> B1 u B2 u B3 .
+    *
+    *   becomes
+    *
+    *   A n nB1 n nB2 -> B3 .
+    *   A n nB1 n nB3 -> B2 .
+    *   A n nB2 n nB3 -> B1 .
+    *   nB1 n nB2 n nB3 -> nA .
+    *
+    *   where nA, nB1, nB2, nB3 are fresh predicates "corresponding" to
+    *   the negation of A, B1, B2, B3 respectively.
+    */
+  def shift(axiom: OWLLogicalAxiom): List[OWLLogicalAxiom] =
+    axiom match {
+      case a: OWLSubClassOfAxiom => {
+        val sub = a.getSubClass.getNNF
+        val sup = a.getSuperClass.getNNF
+        sup match {
+          case sup: OWLObjectUnionOf => {
+            val body = sub.asConjunctSet.map((atom) =>
+              (atom, RSAOntology.getFreshOWLClass())
+            )
+            val head = sup.asDisjunctSet.map((atom) =>
+              (atom, RSAOntology.getFreshOWLClass())
+            )
+
+            val r1 =
+              factory.getOWLSubClassOfAxiom(
+                factory.getOWLObjectIntersectionOf(
+                  (body.map(_._1) ++ head.map(_._2)): _*
+                ),
+                factory.getOWLNothing
+              )
+
+            val r2s =
+              for {
+                (a, na) <- head
+                hs = head.map(_._2).filterNot(_ equals na)
+              } yield factory.getOWLSubClassOfAxiom(
+                factory.getOWLObjectIntersectionOf(
+                  (body.map(_._1) ++ hs): _*
+                ),
+                a
+              )
+
+            val r3s =
+              for {
+                (a, na) <- body
+                bs = body.map(_._1).filterNot(_ equals a)
+              } yield factory.getOWLSubClassOfAxiom(
+                factory.getOWLObjectIntersectionOf(
+                  (bs ++ head.map(_._2)): _*
+                ),
+                na
+              )
+
+            List(r1) ++ r2s ++ r3s
+          }
+          case _ => List(axiom)
+        }
+      }
+      case _ => List(axiom)
+    }
+
+  /** Approximate a Horn-ALCHOIQ ontology to RSA
+    *
+    * This is done by gathering those axioms that prevent the ontology
+    * dependency graph from being tree-shaped, and removing them.
+    *
+    * @param axioms the set of axioms to approximate.
+    * @return the approximated set of axioms.
+    */
+  def toRSA(
+      axioms: List[OWLLogicalAxiom],
+      datafiles: List[File]
+  ): List[OWLLogicalAxiom] = {
+    /* Compute the dependency graph for the ontology */
+    val (graph, nodemap) = RSAUtil.dependencyGraph(axioms, datafiles)
+
+    /* Define node colors for the graph visit */
+    sealed trait NodeColor
+    case object Unvisited extends NodeColor
+    case object Visited extends NodeColor
+    case object ToDelete extends NodeColor
+
+    /* Keep track of node colors during graph visit */
+    var color = Map.from[Resource, NodeColor](
+      graph.nodes.toOuter.map(k => (k, Unvisited))
+    )
+
+    for {
+      component <- graph.componentTraverser().map(_ to Graph)
+      edge <- component
+        .outerEdgeTraverser(component.nodes.head)
+        .withKind(BreadthFirst)
+    } yield {
+      val source = edge._1
+      val target = edge._2
+      color(source) match {
+        case Unvisited | Visited => {
+          color(target) match {
+            case Unvisited =>
+              color(source) = Visited;
+              color(target) = Visited
+            case Visited =>
+              color(source) = ToDelete
+            case ToDelete =>
+              color(source) = Visited
+          }
+        }
+        case ToDelete =>
+      }
+    }
+
+    val toDelete = color.iterator.collect { case (resource: IRI, ToDelete) =>
+      nodemap(resource.getIRI)
+    }.toList
+
+    /* Remove axioms from approximated ontology */
+    axioms diff toDelete
+  }
+
+  // val edges1 = Seq('A ~> 'B, 'B ~> 'C, 'C ~> 'D, 'D ~> 'H, 'H ~>
+  // 'G, 'G ~> 'F, 'E ~> 'A, 'E ~> 'F, 'B ~> 'E, 'F ~> 'G, 'B ~> 'F,
+  // 'C ~> 'G, 'D ~> 'C, 'H ~> 'D)
+  // val edges2 = Seq('I ~> 'M, 'I ~> 'L, 'L ~> 'N, 'M ~> 'N)
+  // val edges3 = Seq('P ~> 'O)
+  // val graph = Graph.from(edges = edges1 ++ edges2 ++ edges3)
+  //
+}
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
index 5329f26..4b298f4 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/Normalizer.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/Normalizer.scala
@@ -4,6 +4,7 @@ import org.semanticweb.owlapi.apibinding.OWLManager
 import org.semanticweb.owlapi.model._
 
 import uk.ac.ox.cs.rsacomb.util.Logger
+import uk.ac.ox.cs.rsacomb.RSAOntology
 
 object Normalizer {
 
@@ -25,12 +26,6 @@ class Normalizer() {
   /** Simplify conversion between Java and Scala collections */
   import uk.ac.ox.cs.rsacomb.implicits.JavaCollections._
 
-  private var counter = -1
-  def freshOWLClass(): OWLClass = {
-    counter += 1
-    factory.getOWLClass(s"X$counter")
-  }
-
   /** Statistics */
   var discarded = 0
   var shifted = 0
@@ -58,7 +53,7 @@ class Normalizer() {
             *   C c D -> { C c X, X c D }
             */
           case _ if !sub.isOWLClass && !sup.isOWLClass => {
-            val cls = freshOWLClass()
+            val cls = RSAOntology.getFreshOWLClass()
             Seq(
               factory.getOWLSubClassOfAxiom(sub, cls),
               factory.getOWLSubClassOfAxiom(cls, sup)
@@ -79,7 +74,7 @@ class Normalizer() {
                   if (conj.isOWLClass)
                     (acc1 :+ conj, acc2)
                   else {
-                    val cls = freshOWLClass()
+                    val cls = RSAOntology.getFreshOWLClass()
                     (
                       acc1 :+ cls,
                       acc2 :+ factory.getOWLSubClassOfAxiom(conj, cls)
@@ -138,7 +133,7 @@ class Normalizer() {
             */
           case (sub: OWLObjectSomeValuesFrom, _)
               if !sub.getFiller.isOWLClass => {
-            val cls = freshOWLClass()
+            val cls = RSAOntology.getFreshOWLClass()
             Seq(
               factory.getOWLSubClassOfAxiom(sub.getFiller, cls),
               factory.getOWLSubClassOfAxiom(
@@ -153,7 +148,7 @@ class Normalizer() {
             */
           case (_, sup: OWLObjectSomeValuesFrom)
               if !sup.getFiller.isOWLClass => {
-            val cls = freshOWLClass()
+            val cls = RSAOntology.getFreshOWLClass()
             Seq(
               factory.getOWLSubClassOfAxiom(cls, sup.getFiller),
               factory.getOWLSubClassOfAxiom(
@@ -298,7 +293,7 @@ class Normalizer() {
             )
           case (_, sup: OWLObjectMaxCardinality)
               if sup.getCardinality == 1 && !sup.getFiller.isOWLClass => {
-            val cls = freshOWLClass()
+            val cls = RSAOntology.getFreshOWLClass()
             Seq(
               factory.getOWLSubClassOfAxiom(cls, sup.getFiller),
               factory.getOWLSubClassOfAxiom(
@@ -488,7 +483,7 @@ class Normalizer() {
         * C(a) -> { X(a), X c C }
         */
       case a: OWLClassAssertionAxiom if !a.getClassExpression.isOWLClass => {
-        val cls = freshOWLClass()
+        val cls = RSAOntology.getFreshOWLClass()
         Seq(
           factory.getOWLClassAssertionAxiom(cls, a.getIndividual),
           factory.getOWLSubClassOfAxiom(cls, a.getClassExpression)
@@ -532,8 +527,10 @@ class Normalizer() {
       sub: OWLClassExpression,
       sup: OWLObjectUnionOf
   ): Seq[OWLLogicalAxiom] = {
-    val body = sub.asConjunctSet.map((atom) => (atom, freshOWLClass()))
-    val head = sup.asDisjunctSet.map((atom) => (atom, freshOWLClass()))
+    val body =
+      sub.asConjunctSet.map((atom) => (atom, RSAOntology.getFreshOWLClass()))
+    val head =
+      sup.asDisjunctSet.map((atom) => (atom, RSAOntology.getFreshOWLClass()))
 
     /* Update statistics */
     shifted += 1