Merge branch 'approximation'v0.2.0

9 files changed, 886 insertions, 415 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 b949ccb..ca54054 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala
@@ -92,8 +92,8 @@ class CanonicalModel(val ontology: RSAOntology) {
   val (facts, rules): (List[TupleTableAtom], List[Rule]) = {
     // Compute rules from ontology axioms
     val (facts, rules) = {
-      val term = RSAOntology.genFreshVariable()
-      val unsafe = ontology.unsafeRoles
+      val term = RSAUtil.genFreshVariable()
+      val unsafe = ontology.unsafe
       ontology.axioms
         .map(a =>
           CanonicalModelConverter.convert(a, term, unsafe, Constant(a), Empty)
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 231d2b8..258c226 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/Main.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/Main.scala
@@ -26,6 +26,10 @@ import tech.oxfordsemantic.jrdfox.logic.sparql.statement.SelectQuery
 import util.{Logger, RDFoxUtil, RSA}
 import sparql.ConjunctiveQuery
 
+import uk.ac.ox.cs.rsacomb.ontology.Ontology
+import uk.ac.ox.cs.rsacomb.converter.Normalizer
+import uk.ac.ox.cs.rsacomb.approximation.LowerBound
+
 case class RSAOption[+T](opt: T) {
   def get[T]: T = opt.asInstanceOf[T]
 }
@@ -122,12 +126,15 @@ object RSAComb extends App {
   /* Command-line options */
   val config = RSAConfig.parse(args.toList)
 
-  val ontology = RSAOntology(
+  /* Load original ontology and normalize it */
+  val ontology = Ontology(
     config('ontology).get[File],
-    config('data).get[List[File]]: _*
-  )
-  val rsa = ontology.toRSA()
-  ontology.statistics()
+    config('data).get[List[File]]
+  ).normalize(new Normalizer)
+
+  /* Approximate the ontology to RSA */
+  val toRSA = new LowerBound
+  val rsa = ontology approximate toRSA
 
   if (config contains 'query) {
     val query =
@@ -140,18 +147,18 @@ object RSAComb extends App {
         Logger.print(s"$answers", Logger.VERBOSE)
         Logger print s"Number of answers: ${answers.length} (${answers.lengthWithMultiplicity})"
         // Retrieve unfiltered answers
-        val unfiltered = rsa.queryDataStore(
-          """
-            SELECT (count(?K) as ?COUNT)
-            WHERE {
-                ?K a rsa:QM .
-            }
-          """,
-          RSA.Prefixes
-        )
-        unfiltered.foreach((u) =>
-          Logger print s"Number of unfiltered answers: ${u.head._2}"
-        )
+        // val unfiltered = rsa.queryDataStore(
+        //   """
+        //     SELECT (count(?K) as ?COUNT)
+        //     WHERE {
+        //         ?K a rsa:QM .
+        //     }
+        //   """,
+        //   RSA.Prefixes
+        // )
+        // unfiltered.foreach((u) =>
+        //   Logger print s"Number of unfiltered answers: ${u.head._2}"
+        // )
       }
       case None =>
         throw new RuntimeException("Submitted query is not conjunctive")
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 3e10697..30e1305 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
@@ -66,117 +66,159 @@ 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._
 import uk.ac.ox.cs.rsacomb.sparql._
 import uk.ac.ox.cs.rsacomb.util.{RDFoxUtil, RSA}
 import uk.ac.ox.cs.rsacomb.util.Logger
+import uk.ac.ox.cs.rsacomb.ontology.Ontology
 
-object RSAOntology {
+object RSAUtil {
 
-  /** Name of the RDFox data store used for CQ answering */
-  private val DataStore = "answer_computation"
+  // implicit def axiomsToOntology(axioms: Seq[OWLAxiom]) = {
+  //   val manager = OWLManager.createOWLOntologyManager()
+  //   manager.createOntology(axioms.asJava)
+  // }
 
-  /** Simple fresh variable generator */
+  /** Manager instance to interface with OWLAPI */
+  val manager = OWLManager.createOWLOntologyManager()
+  val factory = manager.getOWLDataFactory()
+
+  /** 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")
+  }
+
+}
+
+object RSAOntology {
+
+  import uk.ac.ox.cs.rsacomb.implicits.JavaCollections._
 
   /** Manager instance to interface with OWLAPI */
   val manager = OWLManager.createOWLOntologyManager()
 
-  def apply(ontology: File, data: File*): RSAOntology =
-    new RSAOntology(
-      manager.loadOntologyFromOntologyDocument(ontology),
-      data: _*
+  /** Name of the RDFox data store used for CQ answering */
+  private val DataStore = "answer_computation"
+
+  /** Filtering program for a given query
+    *
+    * @param query the query to derive the filtering program
+    * @return the filtering program for the given query
+    */
+  def filteringProgram(query: ConjunctiveQuery): FilteringProgram =
+    Logger.timed(
+      FilteringProgram(FilterType.REVISED)(query),
+      "Generating filtering program",
+      Logger.DEBUG
     )
 
-  def apply(ontology: OWLOntology, data: File*): RSAOntology =
-    new RSAOntology(ontology, data: _*)
+  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
+
+  //   new RSAOntology(
+  //     approx match {
+  //       case Some(a) => a.approximate(axioms, datafiles)
+  //       case None    => axioms
+  //     },
+  //     datafiles: _*
+  //   )
+  // }
+
 }
 
-/** Wrapper class for an ontology in RSA
+/** A wrapper for an RSA ontology
   *
   * @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(axioms: List[OWLLogicalAxiom], datafiles: List[File])
+    extends Ontology(axioms, datafiles) {
 
   /** 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
-  )
-
-  /** OWLAPI internal reasoner instantiated over the approximated ontology */
-  private val reasoner =
-    (new StructuralReasonerFactory()).createReasoner(ontology)
+  //private var removed: Seq[OWLAxiom] = Seq.empty
 
   /** Retrieve individuals/literals in the ontology */
-  val individuals: List[IRI] =
+  private val individuals: List[IRI] =
     ontology
       .getIndividualsInSignature()
       .asScala
       .map(_.getIRI)
       .map(implicits.RDFox.owlapiToRdfoxIri)
       .toList
-  val literals: List[Literal] =
+  private val literals: List[Literal] =
     axioms
       .collect { case a: OWLDataPropertyAssertionAxiom => a }
       .map(_.getObject)
@@ -186,7 +228,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
 
@@ -202,123 +244,36 @@ class RSAOntology(val original: OWLOntology, val datafiles: File*) {
     *    if there exists a role p2 appearing in an axiom of type T4 and
     *    p1 is a subproperty of either p2 or the inverse of p2.
     */
-  val unsafeRoles: List[OWLObjectPropertyExpression] = {
-
-    /* Checking for unsafety condition (1) */
-    val unsafe1 = for {
-      axiom <- tbox
-      if axiom.isT5
-      role1 <- axiom.objectPropertyExpressionsInSignature
-      roleSuper = role1 +: reasoner.superObjectProperties(role1)
-      roleSuperInv = roleSuper.map(_.getInverseProperty)
-      axiom <- tbox
-      if axiom.isT3 && !axiom.isT3top
-      role2 <- axiom.objectPropertyExpressionsInSignature
-      if roleSuperInv contains role2
-    } yield role1
-
-    /* Checking for unsafety condition (2) */
-    val unsafe2 = for {
-      axiom <- tbox
-      if axiom.isT5
-      role1 <- axiom.objectPropertyExpressionsInSignature
-      roleSuper = role1 +: reasoner.superObjectProperties(role1)
-      roleSuperInv = roleSuper.map(_.getInverseProperty)
-      axiom <- tbox
-      if axiom.isT4
-      role2 <- axiom.objectPropertyExpressionsInSignature
-      if roleSuper.contains(role2) || roleSuperInv.contains(role2)
-    } yield role1
-
-    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)
-  }
+  // val unsafeRoles: List[OWLObjectPropertyExpression] = {
+
+  //   /* Checking for unsafety condition (1) */
+  //   val unsafe1 = for {
+  //     axiom <- axioms
+  //     if axiom.isT5
+  //     role1 <- axiom.objectPropertyExpressionsInSignature
+  //     roleSuper = role1 +: reasoner.superObjectProperties(role1)
+  //     roleSuperInv = roleSuper.map(_.getInverseProperty)
+  //     axiom <- axioms
+  //     if axiom.isT3 && !axiom.isT3top
+  //     role2 <- axiom.objectPropertyExpressionsInSignature
+  //     if roleSuperInv contains role2
+  //   } yield role1
+
+  //   /* Checking for unsafety condition (2) */
+  //   val unsafe2 = for {
+  //     axiom <- axioms
+  //     if axiom.isT5
+  //     role1 <- axiom.objectPropertyExpressionsInSignature
+  //     roleSuper = role1 +: reasoner.superObjectProperties(role1)
+  //     roleSuperInv = roleSuper.map(_.getInverseProperty)
+  //     axiom <- axioms
+  //     if axiom.isT4
+  //     role2 <- axiom.objectPropertyExpressionsInSignature
+  //     if roleSuper.contains(role2) || roleSuperInv.contains(role2)
+  //   } yield role1
+
+  //   unsafe1 ++ unsafe2
+  // }
 
   /** Approximate a Horn-ALCHOIQ ontology to RSA
     *
@@ -329,61 +284,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)
@@ -462,31 +417,27 @@ class RSAOntology(val original: OWLOntology, val datafiles: File*) {
     )
   }
 
+  /** Canonical model of the ontology */
   lazy val canonicalModel = Logger.timed(
     new CanonicalModel(this),
     "Generating canonical model program",
     Logger.DEBUG
   )
 
-  def filteringProgram(query: ConjunctiveQuery): FilteringProgram =
-    Logger.timed(
-      FilteringProgram(FilterType.REVISED)(query),
-      "Generating filtering program",
-      Logger.DEBUG
-    )
-
+  /** Computes all roles conflicting with a given role
+    *
+    * @param role a role (object property expression).
+    * @return a set of roles conflicting with `role`.
+    */
   def confl(
       role: OWLObjectPropertyExpression
   ): Set[OWLObjectPropertyExpression] = {
-
-    val invSuperRoles = reasoner
+    reasoner
       .superObjectProperties(role)
       .collect(Collectors.toSet())
       .asScala
       .addOne(role)
       .map(_.getInverseProperty)
-
-    invSuperRoles
       .flatMap(x =>
         reasoner
           .subObjectProperties(x)
@@ -498,6 +449,77 @@ class RSAOntology(val original: OWLOntology, val datafiles: File*) {
       .filterNot(_.getInverseProperty.isOWLTopObjectProperty())
   }
 
+  /** Selfloop detection for a given axiom
+    *
+    * @param axiom an axiom of type [[OWLSubClassOfAxiom]]
+    * @return unfold set for the axiom
+    */
+  def self(axiom: OWLSubClassOfAxiom): Set[Term] = {
+    val role = axiom.objectPropertyExpressionsInSignature(0)
+    if (this.confl(role).contains(role)) {
+      Set(RSA("v0_" ++ axiom.hashed), RSA("v1_" ++ axiom.hashed))
+    } else {
+      Set()
+    }
+  }
+
+  /** Cycle detection for a give axiom
+    *
+    * @param axiom an axiom of type [[OWLSubClassOfAxiom]]
+    * @return unfold set for the axiom
+    *
+    * @todo we can actually use `toTriple` from `RSAAxiom` to get the
+    * classes and the role for a given axiom
+    */
+  def cycle(axiom: OWLSubClassOfAxiom): Set[Term] = {
+    val classes =
+      axiom.classesInSignature.collect(Collectors.toList()).asScala
+    val classA = classes(0)
+    val roleR = axiom
+      .objectPropertyExpressionsInSignature(0)
+      .asInstanceOf[OWLObjectProperty]
+    val classB = classes(1)
+    cycle_aux(classA, roleR, classB)
+  }
+
+  /** Auxiliary function for [[RSAOntology.cycle]] */
+  private def cycle_aux(
+      classA: OWLClass,
+      roleR: OWLObjectProperty,
+      classB: OWLClass
+  ): Set[Term] = {
+    val conflR = this.confl(roleR)
+    // TODO: technically we just need the TBox here
+    val terms = for {
+      axiom1 <- axioms
+      if axiom1.isT5
+      // We expect only one role coming out of a T5 axiom
+      roleS <- axiom1.objectPropertyExpressionsInSignature
+      // Triples ordering is among triples involving safe roles.
+      if !unsafe.contains(roleS)
+      if conflR.contains(roleS)
+      tripleARB = RSAAxiom.hashed(classA, roleR, classB)
+      tripleDSC = axiom1.hashed
+      individual =
+        if (tripleARB > tripleDSC) {
+          RSA("v1_" ++ tripleDSC)
+        } else {
+          // Note that this is also the case for
+          // `tripleARB == tripleDSC`
+          RSA("v0_" ++ tripleDSC)
+        }
+    } yield individual
+    terms to Set
+  }
+
+  /** Returns unfold set for self-loop and cycle for the input axiom
+    *
+    * @param axiom an axiom of type [[OWLSubClassOfAxiom]]
+    * @return unfold set for the axiom
+    */
+  def unfold(axiom: OWLSubClassOfAxiom): Set[Term] =
+    this.self(axiom) | this.cycle(axiom)
+
   /** Returns the answers to a query
     *
     *  @param query query to execute
@@ -505,10 +527,9 @@ class RSAOntology(val original: OWLOntology, val datafiles: File*) {
     */
   def ask(query: ConjunctiveQuery): ConjunctiveQueryAnswers = Logger.timed(
     {
-      import implicits.JavaCollections._
       val (server, data) = RDFoxUtil.openConnection(RSAOntology.DataStore)
       val canon = this.canonicalModel
-      val filter = this.filteringProgram(query)
+      val filter = RSAOntology.filteringProgram(query)
 
       /* Upload data from data file */
       RDFoxUtil.addData(data, datafiles: _*)
@@ -526,12 +547,15 @@ class RSAOntology(val original: OWLOntology, val datafiles: File*) {
         new java.util.HashMap[String, String]
       )
 
+      /* Add canonical model */
       Logger print s"Canonical model rules: ${canon.rules.length}"
       RDFoxUtil.addRules(data, canon.rules)
 
       Logger print s"Canonical model facts: ${canon.facts.length}"
       RDFoxUtil.addFacts(data, canon.facts)
 
+      RDFoxUtil printStatisticsFor data
+
       //{
       //  import java.io.{PrintStream, FileOutputStream, File}
       //  val rules1 = new FileOutputStream(new File("rules1-lubm200.dlog"))
@@ -541,16 +565,13 @@ class RSAOntology(val original: OWLOntology, val datafiles: File*) {
       //  rules2.print(filter.rules.mkString("\n"))
       //}
 
-      //canon.facts.foreach(println)
-      //filter.rules.foreach(println)
-
-      RDFoxUtil printStatisticsFor data
-
+      /* Add filtering program */
       Logger print s"Filtering program rules: ${filter.rules.length}"
       RDFoxUtil.addRules(data, filter.rules)
 
       RDFoxUtil printStatisticsFor data
 
+      /* Gather answers to the query */
       val answers = {
         val ans = filter.answerQuery
         RDFoxUtil
@@ -558,7 +579,9 @@ class RSAOntology(val original: OWLOntology, val datafiles: File*) {
           .map(new ConjunctiveQueryAnswers(query.bcq, query.variables, _))
           .get
       }
+
       RDFoxUtil.closeConnection(server, data)
+
       answers
     },
     "Answers computation",
@@ -569,14 +592,15 @@ class RSAOntology(val original: OWLOntology, val datafiles: File*) {
     *
     * @note This method does not add any facts or rules to the data
     * store. It is most useful after the execution of a query using
-    * [[uk.ac.ox.cs.rsacomb.RSAOntology.ask RSAOntology.ask]].
-    * @note This method has been introduced mostly for debugging purposes.
+    * [[RSAOntology.ask]].
     *
     * @param query query to be executed against the environment
     * @param prefixes additional prefixes for the query. It defaults to
     * an empty set.
     * @param opts additional options to RDFox.
     * @return a collection of answers to the input query.
+    *
+    * @note This method has been introduced mostly for debugging purposes.
     */
   def queryDataStore(
       query: String,
@@ -598,122 +622,11 @@ class RSAOntology(val original: OWLOntology, val datafiles: File*) {
     * [[uk.ac.ox.cs.rsacomb.RSAOntology.ask RSAOntology.ask]]
     * for the corresponding query has been called.
     */
-  def askUnfiltered(
-      cq: ConjunctiveQuery
-  ): Option[Seq[(Long, Seq[Resource])]] = {
-    val query = RDFoxUtil.buildDescriptionQuery("QM", cq.variables.length)
-    queryDataStore(query, RSA.Prefixes)
-  }
+  // def askUnfiltered(
+  //     cq: ConjunctiveQuery
+  // ): Option[Seq[(Long, Seq[Resource])]] = {
+  //   val query = RDFoxUtil.buildDescriptionQuery("QM", cq.variables.length)
+  //   queryDataStore(query, RSA.Prefixes)
+  // }
 
-  def self(axiom: OWLSubClassOfAxiom): Set[Term] = {
-    // Assuming just one role in the signature of a T5 axiom
-    val role = axiom.objectPropertyExpressionsInSignature(0)
-    if (this.confl(role).contains(role)) {
-      Set(
-        RSA("v0_" ++ axiom.hashed),
-        RSA("v1_" ++ axiom.hashed)
-      )
-    } else {
-      Set()
-    }
-  }
-
-  def cycle(axiom: OWLSubClassOfAxiom): Set[Term] = {
-    // TODO: we can actually use `toTriple` from `RSAAxiom`
-    val classes =
-      axiom.classesInSignature.collect(Collectors.toList()).asScala
-    val classA = classes(0)
-    val roleR = axiom
-      .objectPropertyExpressionsInSignature(0)
-      .asInstanceOf[OWLObjectProperty]
-    val classB = classes(1)
-    cycle_aux1(classA, roleR, classB)
-  }
-
-  def cycle_aux0(
-      classA: OWLClass,
-      roleR: OWLObjectProperty,
-      classB: OWLClass
-  ): Set[Term] = {
-    val conflR = this.confl(roleR)
-    val classes = ontology
-      .classesInSignature(Imports.INCLUDED)
-      .collect(Collectors.toSet())
-      .asScala
-    for {
-      classD <- classes
-      roleS <- conflR
-      classC <- classes
-      // Keeping this check for now
-      if !unsafeRoles.contains(roleS)
-      tripleARB = RSAAxiom.hashed(classA, roleR, classB)
-      tripleDSC = RSAAxiom.hashed(classD, roleS, classC)
-      individual =
-        if (tripleARB > tripleDSC) {
-          RSA("v1_" ++ tripleDSC)
-        } else {
-          // Note that this is also the case for
-          // `tripleARB == tripleDSC`
-          RSA("v0_" ++ tripleDSC)
-        }
-    } yield individual
-  }
-
-  def cycle_aux1(
-      classA: OWLClass,
-      roleR: OWLObjectProperty,
-      classB: OWLClass
-  ): Set[Term] = {
-    val conflR = this.confl(roleR)
-    // We just need the TBox to find
-    val terms = for {
-      axiom1 <- tbox
-      if axiom1.isT5
-      // We expect only one role coming out of a T5 axiom
-      roleS <- axiom1.objectPropertyExpressionsInSignature
-      // Triples ordering is among triples involving safe roles.
-      if !unsafeRoles.contains(roleS)
-      if conflR.contains(roleS)
-      tripleARB = RSAAxiom.hashed(classA, roleR, classB)
-      tripleDSC = axiom1.hashed
-      individual =
-        if (tripleARB > tripleDSC) {
-          RSA("v1_" ++ tripleDSC)
-        } else {
-          // Note that this is also the case for
-          // `tripleARB == tripleDSC`
-          RSA("v0_" ++ tripleDSC)
-        }
-    } yield individual
-    terms to Set
-  }
-
-  def unfold(axiom: OWLSubClassOfAxiom): Set[Term] =
-    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
-    )
-  }
-
-} // 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..344f0fe
--- /dev/null
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/approximation/Approximation.scala
@@ -0,0 +1,18 @@
+package uk.ac.ox.cs.rsacomb.approximation
+
+import java.io.File
+import org.semanticweb.owlapi.model.OWLLogicalAxiom
+
+import uk.ac.ox.cs.rsacomb.ontology.Ontology
+
+/** Ontology approximation technique. */
+trait Approximation[T] {
+
+  /** Approximate an ontology.
+    *
+    * @param ontology input ontology as a list of axioms
+    * @return the approximated ontology
+    */
+  def approximate(ontology: Ontology): T
+
+}
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..60a88fb
--- /dev/null
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/approximation/Lowerbound.scala
@@ -0,0 +1,232 @@
+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.ontology.Ontology
+
+object LowerBound {
+
+  private val manager = OWLManager.createOWLOntologyManager()
+  private val factory = manager.getOWLDataFactory()
+
+}
+
+/** 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[RSAOntology] {
+
+  /** 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._
+
+  /** Main entry point for the approximation algorithm */
+  def approximate(ontology: Ontology): RSAOntology =
+    toRSA(
+      new Ontology(
+        ontology.axioms filter inALCHOIQ flatMap shift,
+        ontology.datafiles
+      )
+    )
+
+  /** Discards all axioms outside ALCHOIQ */
+  private 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 n nB3 -> bot .
+    *   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.
+    *
+    * @note this method maintains the normal form of the input axiom.
+    */
+  private 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, RSAUtil.getFreshOWLClass())
+            )
+            val head = sup.asDisjunctSet.map((atom) =>
+              (atom, RSAUtil.getFreshOWLClass())
+            )
+
+            val r1 =
+              LowerBound.factory.getOWLSubClassOfAxiom(
+                LowerBound.factory.getOWLObjectIntersectionOf(
+                  (body.map(_._1) ++ head.map(_._2)): _*
+                ),
+                LowerBound.factory.getOWLNothing
+              )
+
+            val r2s =
+              for {
+                (a, na) <- head
+                hs = head.map(_._2).filterNot(_ equals na)
+              } yield LowerBound.factory.getOWLSubClassOfAxiom(
+                LowerBound.factory.getOWLObjectIntersectionOf(
+                  (body.map(_._1) ++ hs): _*
+                ),
+                a
+              )
+
+            val r3s =
+              for {
+                (a, na) <- body
+                bs = body.map(_._1).filterNot(_ equals a)
+              } yield LowerBound.factory.getOWLSubClassOfAxiom(
+                LowerBound.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 ontology the set of axioms to approximate.
+    * @return the approximated RSA ontology
+    */
+  private def toRSA(ontology: Ontology): RSAOntology = {
+    /* Compute the dependency graph for the ontology */
+    val (graph, nodemap) = ontology.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.collect { case (resource: IRI, ToDelete) =>
+      nodemap(resource.getIRI)
+    }.toList
+
+    /* Remove axioms from approximated ontology */
+    RSAOntology(ontology.axioms diff toDelete, ontology.datafiles)
+  }
+
+  // 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 254fd13..285040e 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
@@ -20,6 +20,8 @@ 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
+import uk.ac.ox.cs.rsacomb.RSAUtil
 
 object Normalizer {
 
@@ -41,12 +43,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
@@ -74,7 +70,7 @@ class Normalizer() {
             *   C c D -> { C c X, X c D }
             */
           case _ if !sub.isOWLClass && !sup.isOWLClass => {
-            val cls = freshOWLClass()
+            val cls = RSAUtil.getFreshOWLClass()
             Seq(
               factory.getOWLSubClassOfAxiom(sub, cls),
               factory.getOWLSubClassOfAxiom(cls, sup)
@@ -95,7 +91,7 @@ class Normalizer() {
                   if (conj.isOWLClass)
                     (acc1 :+ conj, acc2)
                   else {
-                    val cls = freshOWLClass()
+                    val cls = RSAUtil.getFreshOWLClass()
                     (
                       acc1 :+ cls,
                       acc2 :+ factory.getOWLSubClassOfAxiom(conj, cls)
@@ -154,7 +150,7 @@ class Normalizer() {
             */
           case (sub: OWLObjectSomeValuesFrom, _)
               if !sub.getFiller.isOWLClass => {
-            val cls = freshOWLClass()
+            val cls = RSAUtil.getFreshOWLClass()
             Seq(
               factory.getOWLSubClassOfAxiom(sub.getFiller, cls),
               factory.getOWLSubClassOfAxiom(
@@ -169,7 +165,7 @@ class Normalizer() {
             */
           case (_, sup: OWLObjectSomeValuesFrom)
               if !sup.getFiller.isOWLClass => {
-            val cls = freshOWLClass()
+            val cls = RSAUtil.getFreshOWLClass()
             Seq(
               factory.getOWLSubClassOfAxiom(cls, sup.getFiller),
               factory.getOWLSubClassOfAxiom(
@@ -314,7 +310,7 @@ class Normalizer() {
             )
           case (_, sup: OWLObjectMaxCardinality)
               if sup.getCardinality == 1 && !sup.getFiller.isOWLClass => {
-            val cls = freshOWLClass()
+            val cls = RSAUtil.getFreshOWLClass()
             Seq(
               factory.getOWLSubClassOfAxiom(cls, sup.getFiller),
               factory.getOWLSubClassOfAxiom(
@@ -504,7 +500,7 @@ class Normalizer() {
         * C(a) -> { X(a), X c C }
         */
       case a: OWLClassAssertionAxiom if !a.getClassExpression.isOWLClass => {
-        val cls = freshOWLClass()
+        val cls = RSAUtil.getFreshOWLClass()
         Seq(
           factory.getOWLClassAssertionAxiom(cls, a.getIndividual),
           factory.getOWLSubClassOfAxiom(cls, a.getClassExpression)
@@ -548,8 +544,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, RSAUtil.getFreshOWLClass()))
+    val head =
+      sup.asDisjunctSet.map((atom) => (atom, RSAUtil.getFreshOWLClass()))
 
     /* Update statistics */
     shifted += 1
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxConverter.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxConverter.scala
index b892ff5..3aa3c5f 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxConverter.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxConverter.scala
@@ -27,6 +27,7 @@ import tech.oxfordsemantic.jrdfox.logic.datalog.{
   TupleTableAtom
 }
 import tech.oxfordsemantic.jrdfox.logic.expression.{Term, IRI, FunctionCall}
+import uk.ac.ox.cs.rsacomb.RSAUtil
 import uk.ac.ox.cs.rsacomb.RSAOntology
 import uk.ac.ox.cs.rsacomb.suffix.{Empty, Inverse, RSASuffix}
 import uk.ac.ox.cs.rsacomb.util.{RSA, RDFoxUtil}
@@ -159,14 +160,14 @@ trait RDFoxConverter {
       }
 
       case a: OWLSubObjectPropertyOfAxiom => {
-        val term1 = RSAOntology.genFreshVariable()
+        val term1 = RSAUtil.genFreshVariable()
         val body = convert(a.getSubProperty, term, term1, suffix)
         val head = convert(a.getSuperProperty, term, term1, suffix)
         ResultR(List(Rule.create(head, body)))
       }
 
       case a: OWLSubDataPropertyOfAxiom => {
-        val term1 = RSAOntology.genFreshVariable()
+        val term1 = RSAUtil.genFreshVariable()
         val body = convert(a.getSubProperty, term, term1, suffix)
         val head = convert(a.getSuperProperty, term, term1, suffix)
         ResultR(List(Rule.create(head, body)))
@@ -176,7 +177,7 @@ trait RDFoxConverter {
         convert(a.asOWLSubClassOfAxiom, term, unsafe, skolem, suffix)
 
       case a: OWLObjectPropertyRangeAxiom => {
-        val term1 = RSAOntology.genFreshVariable()
+        val term1 = RSAUtil.genFreshVariable()
         val (res, ext) = convert(a.getRange, term, unsafe, skolem, suffix)
         val prop = convert(a.getProperty, term1, term, suffix)
         ResultR(List(Rule.create(res, prop :: ext)))
@@ -343,7 +344,7 @@ trait RDFoxConverter {
       case e: OWLObjectSomeValuesFrom => {
         val cls = e.getFiller()
         val role = e.getProperty()
-        val varX = RSAOntology.genFreshVariable
+        val varX = RSAUtil.genFreshVariable
         val (bind, term1) = skolem match {
           case NoSkolem    => (None, varX)
           case c: Constant => (None, c.iri)
@@ -370,7 +371,7 @@ trait RDFoxConverter {
         // Computes the result of rule skolemization. Depending on the used
         // technique it might involve the introduction of additional atoms,
         // and/or fresh constants and variables.
-        val varX = RSAOntology.genFreshVariable
+        val varX = RSAUtil.genFreshVariable
         val (bind, term1) = skolem match {
           case NoSkolem    => (None, varX)
           case c: Constant => (None, c.iri)
@@ -395,7 +396,7 @@ trait RDFoxConverter {
             s"Class expression '$e' has cardinality restriction != 1."
           )
         val vars @ (y :: z :: _) =
-          Seq(RSAOntology.genFreshVariable(), RSAOntology.genFreshVariable())
+          Seq(RSAUtil.genFreshVariable(), RSAUtil.genFreshVariable())
         val cls = e.getFiller
         val role = e.getProperty
         val (res, ext) = vars.map(convert(cls, _, unsafe, skolem, suffix)).unzip
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/implicits/RSAAtom.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/implicits/RSAAtom.scala
index ea87782..09bfa1e 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/implicits/RSAAtom.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/implicits/RSAAtom.scala
@@ -25,6 +25,7 @@ import tech.oxfordsemantic.jrdfox.logic.datalog.{
 }
 import tech.oxfordsemantic.jrdfox.logic.expression.{IRI}
 
+import uk.ac.ox.cs.rsacomb.RSAUtil
 import uk.ac.ox.cs.rsacomb.RSAOntology
 import uk.ac.ox.cs.rsacomb.suffix.{RSASuffix, Nth}
 import uk.ac.ox.cs.rsacomb.util.RDFoxUtil
@@ -94,7 +95,7 @@ object RSAAtom {
       if (isRDF) {
         (None, List(atom))
       } else {
-        val varS = RSAOntology.genFreshVariable()
+        val varS = RSAUtil.genFreshVariable()
         val skolem = RDFoxUtil.skolem(name, (args :+ varS): _*)
         val atom = TupleTableAtom.rdf(varS, IRI.RDF_TYPE, name)
         val atoms = args.zipWithIndex
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/ontology/Ontology.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/ontology/Ontology.scala
new file mode 100644
index 0000000..ba44605
--- /dev/null
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/ontology/Ontology.scala
@@ -0,0 +1,301 @@
+/*
+ * Copyright 2020, 2021 KRR Oxford
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+package uk.ac.ox.cs.rsacomb.ontology
+
+import java.io.File
+import java.util.stream.Collectors
+
+import scala.collection.mutable.Map
+import scala.collection.JavaConverters._
+import scalax.collection.Graph
+import scalax.collection.GraphPredef._, scalax.collection.GraphEdge._
+
+import org.semanticweb.owlapi.model.parameters.Imports
+import org.semanticweb.owlapi.apibinding.OWLManager
+import org.semanticweb.owlapi.model.{OWLOntology, OWLAxiom, OWLLogicalAxiom}
+import org.semanticweb.owlapi.model.{OWLObjectPropertyExpression}
+import org.semanticweb.owlapi.reasoner.structural.StructuralReasonerFactory
+import tech.oxfordsemantic.jrdfox.logic.datalog.Rule
+import tech.oxfordsemantic.jrdfox.logic.expression.{Resource, Term, Variable}
+
+import uk.ac.ox.cs.rsacomb.approximation.Approximation
+import uk.ac.ox.cs.rsacomb.converter._
+import uk.ac.ox.cs.rsacomb.suffix._
+import uk.ac.ox.cs.rsacomb.util.{RDFoxUtil, RSA}
+
+import uk.ac.ox.cs.rsacomb.RSAUtil
+
+object Ontology {
+
+  /** Simplify conversion between Java and Scala collections */
+  import uk.ac.ox.cs.rsacomb.implicits.JavaCollections._
+
+  /** Type wrapper representing a dependency graph for the ontology.
+    *
+    * The graph is returned along with a map associating each node (IRI
+    * string of the resource), with the corresponding axiom in the
+    * original TBox.
+    */
+  type DependencyGraph = (Graph[Resource, DiEdge], Map[String, OWLAxiom])
+
+  /** Manager instance to interface with OWLAPI
+    *
+    * TODO: turn this into an implicit class parameter.
+    */
+  val manager = OWLManager.createOWLOntologyManager()
+
+  /** Compute the RSA dependency graph for a set of axioms
+    *
+    * @param axioms set of input axioms (TBox) to build the dependency
+    * graph.
+    * @param datafiles data (ABox) to build the dependency graph.
+    * @param unsafe list of unsafe roles in the TBox.
+    *
+    * @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],
+      unsafe: List[OWLObjectPropertyExpression]
+  ): DependencyGraph = {
+
+    var nodemap = Map.empty[String, OWLAxiom]
+
+    /* Create custom converter */
+    object RSAConverter extends RDFoxConverter {
+
+      import org.semanticweb.owlapi.model.{
+        OWLClassExpression,
+        OWLObjectSomeValuesFrom,
+        OWLDataSomeValuesFrom
+      }
+
+      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 = RSAUtil.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)
+  }
+
+  def apply(axioms: List[OWLLogicalAxiom], datafiles: List[File]): Ontology =
+    new Ontology(axioms, datafiles)
+
+  def apply(ontology: OWLOntology, datafiles: List[File]): Ontology = {
+
+    /** TBox axioms */
+    var tbox: List[OWLLogicalAxiom] =
+      ontology
+        .tboxAxioms(Imports.INCLUDED)
+        .collect(Collectors.toList())
+        .collect { case a: OWLLogicalAxiom => a }
+
+    /** RBox axioms */
+    var rbox: List[OWLLogicalAxiom] =
+      ontology
+        .rboxAxioms(Imports.INCLUDED)
+        .collect(Collectors.toList())
+        .collect { case a: OWLLogicalAxiom => a }
+
+    /** 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 }
+
+    Ontology(abox ::: tbox ::: rbox, datafiles)
+  }
+
+  def apply(ontofile: File, datafiles: List[File]): Ontology = {
+    val ontology = manager.loadOntologyFromOntologyDocument(ontofile)
+    Ontology(ontology, datafiles)
+  }
+
+}
+
+/** A wrapper for a generic OWL2 ontology
+  *
+  * @param axioms list of axioms (roughly) corresponding to the TBox.
+  * @param datafiles files containing ABox data.
+  */
+class Ontology(val axioms: List[OWLLogicalAxiom], val datafiles: List[File]) {
+
+  /** Extend OWLAxiom functionalities */
+  import uk.ac.ox.cs.rsacomb.implicits.RSAAxiom._
+
+  /** Simplify conversion between Java and Scala collections */
+  import uk.ac.ox.cs.rsacomb.implicits.JavaCollections._
+
+  println(s"Axioms: ${axioms.length}")
+
+  /** OWLOntology based on input axioms
+    *
+    * This is mainly used to instantiate a new reasoner to be used in
+    * the computation of unsafe roles.
+    */
+  protected val ontology: OWLOntology =
+    Ontology.manager.createOntology((axioms: List[OWLAxiom]).asJava)
+
+  /** OWLAPI internal reasoner for ontology */
+  protected val reasoner =
+    (new StructuralReasonerFactory()).createReasoner(ontology)
+
+  /** Unsafe roles in the ontology
+    *
+    * Unsafety conditions are the following:
+    *
+    * 1) For all roles r1 appearing in an axiom of type T5, r1 is unsafe
+    *    if there exists a role r2 (different from top) appearing in an
+    *    axiom of type T3 and r1 is a subproperty of the inverse of r2.
+    *
+    * 2) For all roles p1 appearing in an axiom of type T5, p1 is unsafe
+    *    if there exists a role p2 appearing in an axiom of type T4 and
+    *    p1 is a subproperty of either p2 or the inverse of p2.
+    */
+  lazy val unsafe: List[OWLObjectPropertyExpression] = {
+
+    /* Checking for unsafety condition (1) */
+    val unsafe1 = for {
+      axiom <- axioms
+      if axiom.isT5
+      role1 <- axiom.objectPropertyExpressionsInSignature
+      roleSuper = role1 +: reasoner.superObjectProperties(role1)
+      axiom <- axioms
+      if axiom.isT3 && !axiom.isT3top
+      role2 <- axiom.objectPropertyExpressionsInSignature
+      if roleSuper contains role2.getInverseProperty
+    } yield role1
+
+    /* Checking for unsafety condition (2) */
+    val unsafe2 = for {
+      axiom <- axioms
+      if axiom.isT5
+      role1 <- axiom.objectPropertyExpressionsInSignature
+      roleSuper = role1 +: reasoner.superObjectProperties(role1)
+      axiom <- axioms
+      if axiom.isT4
+      role2 <- axiom.objectPropertyExpressionsInSignature
+      if roleSuper.contains(role2) ||
+        roleSuper.contains(role2.getInverseProperty)
+    } yield role1
+
+    unsafe1 ++ unsafe2
+  }
+
+  /** Compute the dependency graph for the ontology */
+  lazy val dependencyGraph: Ontology.DependencyGraph =
+    Ontology.dependencyGraph(axioms, datafiles, this.unsafe)
+
+  /** RSA check */
+  lazy val isRSA: Boolean = ???
+
+  /** Normalize the ontology according to the given normalizer
+    *
+    * @param normalizer the normalization technique to be used.
+    * @return a new normalized [[Ontology]].
+    */
+  def normalize(normalizer: Normalizer): Ontology =
+    new Ontology(
+      axioms flatMap normalizer.normalize,
+      datafiles
+    )
+
+  /** Approximate the ontology according to the given approximation
+    * technique.
+    *
+    * @param approximation the approximation to be used on the ontology.
+    * @return the result of the approximation.
+    */
+  def approximate[T](approximation: Approximation[T]): T =
+    approximation.approximate(this)
+}