Reorganize project with Java-like folder structure

16 files changed, 2169 insertions, 0 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
new file mode 100644
index 0000000..f0f1bf8
--- /dev/null
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala
@@ -0,0 +1,284 @@
+package uk.ac.ox.cs.rsacomb
+
+import org.semanticweb.owlapi.model.{OWLObjectInverseOf, OWLObjectProperty}
+import org.semanticweb.owlapi.model.{
+  OWLClass,
+  // OWLObjectProperty,
+  OWLSubObjectPropertyOfAxiom,
+  // OWLObjectPropertyExpression,
+  OWLObjectSomeValuesFrom,
+  OWLSubClassOfAxiom
+}
+
+import tech.oxfordsemantic.jrdfox.logic.datalog.{
+  Rule,
+  BodyFormula,
+  TupleTableAtom,
+  Negation
+}
+import tech.oxfordsemantic.jrdfox.logic.expression.{
+  Term,
+  Variable,
+  // Resource,
+  IRI
+}
+
+import uk.ac.ox.cs.rsacomb.converter.{
+  SkolemStrategy,
+  RDFoxAxiomConverter,
+  RDFoxPropertyExprConverter
+}
+import uk.ac.ox.cs.rsacomb.implicits.RSAAxiom
+import uk.ac.ox.cs.rsacomb.suffix.{Empty, Forward, Backward, Inverse}
+import uk.ac.ox.cs.rsacomb.util.RSA
+
+class CanonicalModel(val ontology: RSAOntology) extends RSAAxiom {
+
+  import implicits.RDFox._
+  import implicits.JavaCollections._
+
+  val named: List[Rule] =
+    ontology.individuals.map(a => Rule.create(RSA.Named(a)))
+
+  val rolesAdditionalRules: List[Rule] = {
+    // Given a role (predicate) compute additional logic rules
+    def additional(pred: String): Seq[Rule] = {
+      val varX = Variable.create("X")
+      val varY = Variable.create("Y")
+      for (
+        (hSuffix, bSuffix) <- List(
+          (Empty, Forward),
+          (Empty, Backward),
+          (Inverse, Forward + Inverse),
+          (Inverse, Backward + Inverse),
+          (Backward + Inverse, Forward),
+          (Forward + Inverse, Backward),
+          (Backward, Forward + Inverse),
+          (Forward, Backward + Inverse)
+        )
+      )
+        yield Rule.create(
+          TupleTableAtom.rdf(varX, pred :: hSuffix, varY),
+          TupleTableAtom.rdf(varX, pred :: bSuffix, varY)
+        )
+    }
+    // Compute additional rules per role
+    ontology.roles
+      .collect { case prop: OWLObjectProperty => prop }
+      .map(_.getIRI.getIRIString)
+      .flatMap(additional)
+  }
+
+  private lazy val topAxioms: List[Rule] = {
+    val varX = Variable.create("X")
+    val varY = Variable.create("Y")
+    val concepts = ontology.concepts.map(c => {
+      Rule.create(
+        RSA.Thing(varX),
+        TupleTableAtom.rdf(varX, IRI.RDF_TYPE, c.getIRI)
+      )
+    })
+    val roles = ontology.roles.map(r => {
+      val name = r match {
+        case x: OWLObjectProperty => x.getIRI.getIRIString
+        case x: OWLObjectInverseOf =>
+          x.getInverse.getNamedProperty.getIRI.getIRIString :: Inverse
+      }
+      Rule.create(
+        List(RSA.Thing(varX), RSA.Thing(varY)),
+        List(TupleTableAtom.rdf(varX, name, varY))
+      )
+    })
+    concepts ::: roles
+  }
+
+  private val equalityAxioms: List[Rule] = {
+    val varX = Variable.create("X")
+    val varY = Variable.create("Y")
+    val varZ = Variable.create("Z")
+    List(
+      // Reflexivity
+      Rule.create(RSA.congruent(varX, varX), RSA.Thing(varX)),
+      // Simmetry
+      Rule.create(RSA.congruent(varY, varX), RSA.congruent(varX, varY)),
+      // Transitivity
+      Rule.create(
+        RSA.congruent(varX, varZ),
+        RSA.congruent(varX, varY),
+        RSA.congruent(varY, varZ)
+      )
+    )
+  }
+
+  val rules: List[Rule] = {
+    // Compute rules from ontology axioms
+    val rules = ontology.axioms.flatMap(_.accept(RuleGenerator))
+    // Return full set of rules
+    rules ::: rolesAdditionalRules ::: topAxioms ::: equalityAxioms ::: named
+  }
+
+  object RuleGenerator
+      extends RDFoxAxiomConverter(
+        Variable.create("X"),
+        ontology.unsafeRoles,
+        SkolemStrategy.None,
+        Empty
+      ) {
+
+    private def rules1(axiom: OWLSubClassOfAxiom): List[Rule] = {
+      val unfold = ontology.unfold(axiom).toList
+      // Fresh Variables
+      val v0 = RSA("v0_" ++ axiom.hashed)
+      val varX = Variable.create("X")
+      implicit val unfoldTerm = RSA(unfold.hashCode.toString)
+      // TODO: use axiom.toTriple instead
+      val atomA: TupleTableAtom = {
+        val cls = axiom.getSubClass.asInstanceOf[OWLClass].getIRI
+        TupleTableAtom.rdf(varX, IRI.RDF_TYPE, cls)
+      }
+      val roleRf: TupleTableAtom = {
+        val visitor =
+          new RDFoxPropertyExprConverter(varX, v0, Forward)
+        axiom.getSuperClass
+          .asInstanceOf[OWLObjectSomeValuesFrom]
+          .getProperty
+          .accept(visitor)
+          .head
+      }
+      val atomB: TupleTableAtom = {
+        val cls = axiom.getSuperClass
+          .asInstanceOf[OWLObjectSomeValuesFrom]
+          .getFiller
+          .asInstanceOf[OWLClass]
+          .getIRI
+        TupleTableAtom.rdf(v0, IRI.RDF_TYPE, cls)
+      }
+      // TODO: To be consistent with the specifics of the visitor we are
+      // returning facts as `Rule`s with true body. While this is correct
+      // there is an easier way to import facts into RDFox. Are we able to
+      // do that?
+      val facts = unfold.map(x => Rule.create(RSA.In(x)))
+      val rules = List(
+        Rule.create(roleRf, atomA, RSA.notIn(varX)),
+        Rule.create(atomB, atomA, RSA.notIn(varX))
+      )
+      facts ++ rules
+    }
+
+    private def rules2(axiom: OWLSubClassOfAxiom): List[Rule] = {
+      val roleR =
+        axiom.getSuperClass
+          .asInstanceOf[OWLObjectSomeValuesFrom]
+          .getProperty
+      if (ontology.confl(roleR) contains roleR) {
+        // Fresh Variables
+        val v0 = RSA("v0_" ++ axiom.hashed)
+        val v1 = RSA("v1_" ++ axiom.hashed)
+        val v2 = RSA("v2_" ++ axiom.hashed)
+        // Predicates
+        def atomA(t: Term): TupleTableAtom = {
+          val cls = axiom.getSubClass.asInstanceOf[OWLClass].getIRI
+          TupleTableAtom.rdf(t, IRI.RDF_TYPE, cls)
+        }
+        def roleRf(t1: Term, t2: Term): TupleTableAtom = {
+          val visitor =
+            new RDFoxPropertyExprConverter(t1, t2, Forward)
+          roleR.accept(visitor).head
+        }
+        def atomB(t: Term): TupleTableAtom = {
+          val cls = axiom.getSuperClass
+            .asInstanceOf[OWLObjectSomeValuesFrom]
+            .getFiller
+            .asInstanceOf[OWLClass]
+            .getIRI
+          TupleTableAtom.rdf(t, IRI.RDF_TYPE, cls)
+        }
+        //Rules
+        List(
+          Rule.create(roleRf(v0, v1), atomA(v0)),
+          Rule.create(atomB(v1), atomA(v0)),
+          Rule.create(roleRf(v1, v2), atomA(v1)),
+          Rule.create(atomB(v2), atomA(v1))
+        )
+      } else {
+        List()
+      }
+    }
+
+    private def rules3(axiom: OWLSubClassOfAxiom): List[Rule] = {
+      val cycle = ontology.cycle(axiom).toList
+      val roleR =
+        axiom.getSuperClass
+          .asInstanceOf[OWLObjectSomeValuesFrom]
+          .getProperty
+      // Fresh Variables
+      val v1 = RSA("v1_" ++ axiom.hashed)
+      // Predicates
+      def atomA(t: Term): TupleTableAtom = {
+        val cls = axiom.getSubClass.asInstanceOf[OWLClass].getIRI
+        TupleTableAtom.rdf(t, IRI.RDF_TYPE, cls)
+      }
+      def roleRf(t: Term): TupleTableAtom = {
+        val visitor =
+          new RDFoxPropertyExprConverter(t, v1, Forward)
+        roleR.accept(visitor).head
+      }
+      val atomB: TupleTableAtom = {
+        val cls = axiom.getSuperClass
+          .asInstanceOf[OWLObjectSomeValuesFrom]
+          .getFiller
+          .asInstanceOf[OWLClass]
+          .getIRI
+        TupleTableAtom.rdf(v1, IRI.RDF_TYPE, cls)
+      }
+      cycle.flatMap { x =>
+        List(
+          Rule.create(roleRf(x), atomA(x)),
+          Rule.create(atomB, atomA(x))
+        )
+      }
+    }
+
+    override def visit(axiom: OWLSubClassOfAxiom): List[Rule] = {
+      if (axiom.isT5) {
+        // TODO: get role in T5 axiom
+        // Assuming one role here
+        val role = axiom.objectPropertyExpressionsInSignature(0)
+        if (ontology.unsafeRoles contains role) {
+          val visitor =
+            new RDFoxAxiomConverter(
+              Variable.create("X"),
+              ontology.unsafeRoles,
+              SkolemStrategy.Standard(axiom.toString),
+              Forward
+            )
+          axiom.accept(visitor)
+        } else {
+          rules1(axiom) ::: rules2(axiom) ::: rules3(axiom)
+        }
+      } else {
+        // Fallback to standard OWL to LP translation
+        super.visit(axiom)
+      }
+    }
+
+    override def visit(axiom: OWLSubObjectPropertyOfAxiom): List[Rule] = {
+      val varX = Variable.create("X")
+      val visitorF = new RDFoxAxiomConverter(
+        varX,
+        ontology.unsafeRoles,
+        SkolemStrategy.None,
+        Forward
+      )
+      val visitorB = new RDFoxAxiomConverter(
+        varX,
+        ontology.unsafeRoles,
+        SkolemStrategy.None,
+        Backward
+      )
+      axiom.accept(visitorB) ::: axiom.accept(visitorF)
+    }
+
+  }
+
+}
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/FilteringProgram.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/FilteringProgram.scala
new file mode 100644
index 0000000..b154575
--- /dev/null
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/FilteringProgram.scala
@@ -0,0 +1,366 @@
+package uk.ac.ox.cs.rsacomb
+
+import tech.oxfordsemantic.jrdfox.logic.Datatype
+import tech.oxfordsemantic.jrdfox.logic.expression.{
+  Term,
+  IRI,
+  Variable,
+  Literal,
+  FunctionCall
+}
+import tech.oxfordsemantic.jrdfox.logic.datalog.{
+  Rule,
+  TupleTableAtom,
+  BindAtom,
+  TupleTableName,
+  Atom,
+  BodyFormula,
+  Negation
+}
+import tech.oxfordsemantic.jrdfox.logic.sparql.statement.{SelectQuery}
+import tech.oxfordsemantic.jrdfox.logic.sparql.pattern.{
+  GroupGraphPattern,
+  ConjunctionPattern,
+  TriplePattern,
+  QueryPattern
+}
+
+import scala.collection.JavaConverters._
+
+import uk.ac.ox.cs.rsacomb.implicits.RSAAtom
+import uk.ac.ox.cs.rsacomb.suffix.{RSASuffix, Forward, Backward}
+import uk.ac.ox.cs.rsacomb.util.RSA
+
+class FilteringProgram(query: SelectQuery, constants: List[Term])
+    extends RSAAtom {
+
+  /* Makes mplicit conversion OWLAPI IRI <-> RDFox IRI available */
+  // import implicits.RDFox._
+
+  implicit val variables: (List[Term], List[Term]) = {
+    val all: Set[Variable] = query.getQueryBody.getWherePattern match {
+      case b: ConjunctionPattern => {
+        b.getConjuncts.asScala.toSet.flatMap { conj: QueryPattern =>
+          conj match {
+            case c: TriplePattern =>
+              Set(c.getSubject, c.getPredicate, c.getObject).collect {
+                case v: Variable => v
+              }
+            case _ => Set()
+          }
+        }
+      }
+      case _ => Set()
+    }
+    if (query.getAllPossibleVariables) {
+      (all.toList, List())
+    } else {
+      val answer = query.getSelection.asScala.map(_.getVariable).toSet
+      (answer.toList, (all &~ answer).toList)
+    }
+  }
+
+  val (answer, bounded) = variables
+
+  val facts: List[Rule] = constants.map(c => Rule.create(RSA.NI(c)))
+  val rules: List[Rule] =
+    this.generateFilteringProgram().map(reifyRule) ++ facts
+
+  /* NOTE: we are restricting to queries that contain conjunctions of
+   * atoms for the time being. This might need to be reviewed in the
+   * future.
+   */
+  private def queryToBody(body: GroupGraphPattern): List[TupleTableAtom] =
+    body match {
+      case b: ConjunctionPattern => {
+        val conjuncts = b.getConjuncts.asScala.toList
+        conjuncts flatMap { conj =>
+          conj match {
+            case c: TriplePattern =>
+              List(
+                TupleTableAtom.rdf(c.getSubject, c.getPredicate, c.getObject)
+              )
+            case _ => List()
+          }
+        }
+      }
+      case _ => List()
+    }
+
+  private def generateFilteringProgram(): List[Rule] = {
+    // General purpose variables
+    val varU = Variable.create("U")
+    val varV = Variable.create("V")
+    val varW = Variable.create("W")
+    // Query formula as a rule body
+    val body = queryToBody(query.getQueryBody.getWherePattern)
+    // Auxiliar predicates/helpers
+    def not(atom: TupleTableAtom): BodyFormula = Negation.create(atom)
+    // val predQM =
+    //   TupleTableAtom.create(
+    //     TupleTableName.create(RSA.Qm.getIRI),
+    //     (answer ++ bounded): _*
+    //   )
+    // def predID(t1: Term, t2: Term) =
+    //   TupleTableAtom.create(
+    //     TupleTableName.create(RSA.rsa("ID").getIRI),
+    //     (answer ++ bounded).appended(t1).appended(t2): _*
+    //   )
+    // def predNAMED(t1: Term): TupleTableAtom =
+    //   TupleTableAtom.rdf(t1, IRI.RDF_TYPE, RSA.rsa("NAMED"))
+    // def predTQ(t1: Term, t2: Term, sx: RSASuffix) =
+    //   TupleTableAtom.create(
+    //     TupleTableName.create(RSA.rsa("TQ" :: sx).getIRI),
+    //     (answer ++ bounded).appended(t1).appended(t2): _*
+    //   )
+    // def predAQ(t1: Term, t2: Term, sx: RSASuffix) =
+    //   TupleTableAtom.create(
+    //     TupleTableName.create(RSA.rsa("AQ" :: sx).getIRI),
+    //     (answer ++ bounded).appended(t1).appended(t2): _*
+    //   )
+    // val predFK =
+    //   TupleTableAtom.create(
+    //     TupleTableName.create(RSA.rsa("FK").getIRI),
+    //     (answer ++ bounded): _*
+    //   )
+    // val predSP =
+    //   TupleTableAtom.create(
+    //     TupleTableName.create(RSA.rsa("SP").getIRI),
+    //     (answer ++ bounded): _*
+    //   )
+    // val predANS =
+    //   TupleTableAtom.create(
+    //     TupleTableName.create(RSA.rsa("ANS").getIRI),
+    //     answer: _*
+    //   )
+
+    /* Rule 1 */
+    val r1 = Rule.create(RSA.QM, body: _*)
+
+    /* Rules 3x */
+    val r3a =
+      for ((v, i) <- bounded.zipWithIndex)
+        yield Rule.create(RSA.ID(RSA(i), RSA(i)), RSA.QM, not(RSA.NI(v)))
+    val r3b = Rule.create(RSA.ID(varV, varU), RSA.ID(varU, varV))
+    val r3c =
+      Rule.create(RSA.ID(varU, varW), RSA.ID(varU, varV), RSA.ID(varV, varW))
+
+    /* Rules 4x */
+    val r4a = for {
+      role1 <- body.filter(_.isRoleAssertion)
+      if bounded contains (role1.getArguments.get(2))
+      role2 <- body.filter(_.isRoleAssertion)
+      if bounded contains (role2.getArguments.get(2))
+    } yield Rule.create(
+      RSA.FK,
+      role1 << Forward,
+      role2 << Forward,
+      RSA.ID(
+        RSA(bounded.indexOf(role1.getArguments.get(2))),
+        RSA(bounded.indexOf(role2.getArguments.get(2)))
+      ),
+      not(RSA.congruent(role1.getArguments.get(0), role2.getArguments.get(0)))
+    )
+    val r4b = for {
+      role1 <- body.filter(_.isRoleAssertion)
+      if bounded contains (role1.getArguments.get(2))
+      role2 <- body.filter(_.isRoleAssertion)
+      if bounded contains (role2.getArguments.get(0))
+    } yield Rule.create(
+      RSA.FK,
+      role1 << Forward,
+      role2 << Backward,
+      RSA.ID(
+        RSA(bounded.indexOf(role1.getArguments.get(2))),
+        RSA(bounded.indexOf(role2.getArguments.get(0)))
+      ),
+      not(RSA.congruent(role1.getArguments.get(0), role2.getArguments.get(2)))
+    )
+    val r4c = for {
+      role1 <- body.filter(_.isRoleAssertion)
+      if bounded contains (role1.getArguments.get(0))
+      role2 <- body.filter(_.isRoleAssertion)
+      if bounded contains (role2.getArguments.get(0))
+    } yield Rule.create(
+      RSA.FK,
+      role1 << Backward,
+      role2 << Backward,
+      RSA.ID(
+        RSA(bounded.indexOf(role1.getArguments.get(0))),
+        RSA(bounded.indexOf(role2.getArguments.get(0)))
+      ),
+      not(RSA.congruent(role1.getArguments.get(2), role2.getArguments.get(2)))
+    )
+
+    /* Rules 5x */
+    val r5a = for {
+      role1 <- body.filter(_.isRoleAssertion)
+      role1arg0 = role1.getArguments.get(0)
+      role1arg2 = role1.getArguments.get(2)
+      if bounded contains role1arg0
+      if bounded contains role1arg2
+      role2 <- body.filter(_.isRoleAssertion)
+      role2arg0 = role2.getArguments.get(0)
+      role2arg2 = role2.getArguments.get(2)
+      if bounded contains role2arg0
+      if bounded contains role2arg2
+    } yield Rule.create(
+      RSA.ID(
+        RSA(bounded indexOf role1arg0),
+        RSA(bounded indexOf role2arg0)
+      ),
+      role1 << Forward,
+      role2 << Forward,
+      RSA.ID(
+        RSA(bounded indexOf role1arg2),
+        RSA(bounded indexOf role2arg2)
+      ),
+      RSA.congruent(role1arg0, role2arg0),
+      not(RSA.NI(role1arg0))
+    )
+    val r5b = for {
+      role1 <- body.filter(_.isRoleAssertion)
+      role1arg0 = role1.getArguments.get(0)
+      role1arg2 = role1.getArguments.get(2)
+      if bounded contains role1arg0
+      if bounded contains role1arg2
+      role2 <- body.filter(_.isRoleAssertion)
+      role2arg0 = role2.getArguments.get(0)
+      role2arg2 = role2.getArguments.get(2)
+      if bounded contains role2arg0
+      if bounded contains role2arg2
+    } yield Rule.create(
+      RSA.ID(
+        RSA(bounded indexOf role1arg0),
+        RSA(bounded indexOf role2arg2)
+      ),
+      role1 << Forward,
+      role2 << Backward,
+      RSA.ID(
+        RSA(bounded indexOf role1arg2),
+        RSA(bounded indexOf role2arg0)
+      ),
+      RSA.congruent(role1arg0, role2arg2),
+      not(RSA.NI(role1arg0))
+    )
+    val r5c = for {
+      role1 <- body.filter(_.isRoleAssertion)
+      role1arg0 = role1.getArguments.get(0)
+      role1arg2 = role1.getArguments.get(2)
+      if bounded contains role1arg0
+      if bounded contains role1arg2
+      role2 <- body.filter(_.isRoleAssertion)
+      role2arg0 = role2.getArguments.get(0)
+      role2arg2 = role2.getArguments.get(2)
+      if bounded contains role2arg0
+      if bounded contains role2arg2
+    } yield Rule.create(
+      RSA.ID(
+        RSA(bounded indexOf role1arg2),
+        RSA(bounded indexOf role2arg2)
+      ),
+      role1 << Backward,
+      role2 << Backward,
+      RSA.ID(
+        RSA(bounded indexOf role1arg0),
+        RSA(bounded indexOf role2arg0)
+      ),
+      RSA.congruent(role1arg2, role2arg2),
+      not(RSA.NI(role1arg2))
+    )
+
+    /* Rules 6 */
+    val r6 = {
+      for {
+        role <- body.filter(_.isRoleAssertion)
+        arg0 = role.getArguments.get(0)
+        arg2 = role.getArguments.get(2)
+        if bounded contains arg0
+        if bounded contains arg2
+        suffix <- Seq(Forward, Backward)
+      } yield Rule.create(
+        RSA.AQ(varV, varW, suffix),
+        role << suffix,
+        RSA.ID(RSA(bounded indexOf arg0), varV),
+        RSA.ID(RSA(bounded indexOf arg2), varW)
+      )
+    }
+
+    /* Rules 7x */
+    val r7a = {
+      for (suffix <- List(Forward, Backward))
+        yield Rule.create(
+          RSA.TQ(varU, varV, suffix),
+          RSA.AQ(varU, varV, suffix)
+        )
+    }
+    val r7b = {
+      for (suffix <- List(Forward, Backward))
+        yield Rule.create(
+          RSA.TQ(varU, varW, suffix),
+          RSA.AQ(varU, varV, suffix),
+          RSA.TQ(varV, varW, suffix)
+        )
+    }
+
+    /* Rules 8x */
+    val r8a =
+      for (v <- answer) yield Rule.create(RSA.SP, RSA.QM, not(RSA.Named(v)))
+    val r8b =
+      Rule.create(RSA.SP, RSA.FK)
+    val r8c =
+      for (suffix <- List(Forward, Backward))
+        yield Rule.create(
+          RSA.SP,
+          RSA.TQ(varV, varV, suffix)
+        )
+
+    /* Rule 9 */
+    val r9 = Rule.create(RSA.Ans, RSA.QM, not(RSA.SP))
+
+    r1 ::
+      r3a ::: r3b :: r3c ::
+      r4c ::: r4b ::: r4a :::
+      r5c ::: r5b ::: r5a :::
+      r6 :::
+      r7b ::: r7a :::
+      r8a ::: r8b :: r8c :::
+      r9 ::
+      List()
+  }
+
+  private def reifyAtom(atom: Atom): (Option[BindAtom], List[Atom]) = {
+    atom match {
+      case atom: TupleTableAtom => atom.reified
+      case other                => (None, List(other))
+    }
+  }
+
+  private def reifyBodyFormula(formula: BodyFormula): List[BodyFormula] = {
+    formula match {
+      case atom: TupleTableAtom => atom.reified._2
+      case neg: Negation => {
+        val (bs, as) = neg.getNegatedAtoms.asScala.toList.map(reifyAtom).unzip
+        val bind = bs.flatten.map(_.getBoundVariable).asJava
+        val atoms = as.flatten.asJava
+        List(Negation.create(bind, atoms))
+      }
+      case other => List(other)
+    }
+  }
+
+  private def reifyRule(rule: Rule): Rule = {
+    val (bs, hs) = rule.getHead.asScala.toList.map(_.reified).unzip
+    val head: List[TupleTableAtom] = hs.flatten
+    val bind: List[BodyFormula] = bs.flatten
+    val body: List[BodyFormula] =
+      rule.getBody.asScala.toList.map(reifyBodyFormula).flatten
+    Rule.create(head.asJava, (body ++ bind).asJava)
+  }
+
+} // class FilteringProgram
+
+object FilteringProgram {
+  def apply(query: SelectQuery, constants: List[Term]): FilteringProgram =
+    new FilteringProgram(query, constants)
+} // object FilteringProgram
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/Main.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/Main.scala
new file mode 100644
index 0000000..c3db99d
--- /dev/null
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/Main.scala
@@ -0,0 +1,249 @@
+package uk.ac.ox.cs.rsacomb
+
+/* Java imports */
+import java.io.File
+import java.util.HashMap
+import scala.collection.JavaConverters._
+
+import tech.oxfordsemantic.jrdfox.client.UpdateType
+import tech.oxfordsemantic.jrdfox.logic.sparql.statement.SelectQuery
+import tech.oxfordsemantic.jrdfox.logic.expression.{IRI, Term}
+
+/* Local imports */
+import util.{RDFoxHelpers, RSA}
+
+object RSAComb extends App {
+
+  val help: String = """
+  rsacomb - combined approach for CQ answering for RSA ontologies.
+
+  USAGE
+    rsacomb <path/to/ontology.owl> <path/to/query.sparql>
+
+  where
+    the ontology is expected to be an OWL file and the (single)
+    query a SPARQL query file.
+
+  """
+
+  /* Simple arguments handling
+   *
+   * TODO: use something better later on
+   */
+
+  if (args.length < 2) {
+    println(help)
+    sys.exit;
+  }
+
+  val ontoPath = new File(args(0))
+  val queryPath = new File(args(1))
+
+  if (!ontoPath.isFile || !queryPath.isFile) {
+    println("The provided arguments are not regular files.\n\n")
+    println(help)
+    sys.exit;
+  }
+
+  /* Create RSA object from generic OWLOntology
+   *
+   * TODO: It might be required to check if the ontology in input is
+   * Horn-ALCHOIQ. At the moment we are assuming this is always the
+   * case.
+   */
+
+  val ontology = RSAOntology(ontoPath)
+  if (ontology.isRSA) {
+
+    /* Load query */
+    val query = RDFoxHelpers.parseSelectQuery(
+      """
+        PREFIX  :  <http://example.com/rsa_example.owl#>
+
+        SELECT ?X
+        WHERE {
+          ?X a  :D ;
+             :R ?Y .
+          ?Y :S ?Z .
+          ?Z a  :D .
+        }
+      """
+    )
+
+    /* Compute answers to query */
+    query match {
+      case Some(query) => {
+
+        import implicits.JavaCollections._
+
+        // Open connection to RDFox
+        val (server, data) = RDFoxHelpers.openConnection("AnswerComputation")
+
+        {
+          println("\nQuery")
+          println(query)
+        }
+
+        // Step 1. Computing the canonical model
+        val canon = ontology.canonicalModel
+        data.addRules(canon.rules)
+
+        {
+          println("\nCanonical Model rules:")
+          canon.rules.foreach(println)
+        }
+
+        // Step 2. Computing the canonical model
+        val nis = {
+          val query = "SELECT ?Y WHERE { ?X rsa:EquivTo ?Y ; a rsa:Named . }"
+          RDFoxHelpers.submitSelectQuery(data, query, RSA.Prefixes).flatten
+        }
+        val filter = ontology.filteringProgram(query, nis)
+        data.addRules(filter.rules)
+
+        {
+          println("\nFiltering rules")
+          filter.rules.foreach(println)
+        }
+
+        // Retrieve answers
+        println("\nAnswers:")
+        val ans =
+          RDFoxHelpers.queryInternalPredicate(data, "Ans", filter.answer.length)
+        println(ans)
+
+        /* DEBUG: adding additional checks
+         */
+        {
+          import suffix.{Forward, Backward}
+
+          val arity = filter.answer.length + filter.bounded.length
+
+          println("\nIndividuals:")
+          ontology.individuals.foreach(println)
+
+          println("\nThings:")
+          val things = RDFoxHelpers.submitSelectQuery(
+            data,
+            """
+             PREFIX  owl:  <http://www.w3.org/2002/07/owl#>
+
+             SELECT ?X {
+               ?X a owl:Thing
+             }
+             """
+          )
+          println(things)
+
+          println("\nNAMEDs:")
+          val named = RDFoxHelpers.submitSelectQuery(
+            data,
+            """
+             SELECT ?X {
+               ?X a rsa:Named
+             }
+             """,
+            RSA.Prefixes
+          )
+          println(named)
+
+          println("\nNIs:")
+          val nis = RDFoxHelpers.submitSelectQuery(
+            data,
+            """
+             SELECT ?X {
+               ?X a rsa:NI
+             }
+             """,
+            RSA.Prefixes
+          )
+          println(nis)
+
+          // ID instances
+          println("\nIDs:")
+          val ids = RDFoxHelpers.queryInternalPredicate(
+            data,
+            "ID",
+            arity + 2
+          )
+          println(ids)
+
+          println("\nEquivTo:")
+          val equivs = RDFoxHelpers.submitSelectQuery(
+            data,
+            """
+              SELECT ?X ?Y {
+                ?X rsa:EquivTo ?Y
+              }
+            """,
+            RSA.Prefixes
+          )
+          println(equivs)
+
+          // Unfiltered answers
+          println("\nPossible answers:")
+          val qms = RDFoxHelpers.queryInternalPredicate(
+            data,
+            "QM",
+            arity
+          )
+          println(qms)
+
+          // Cycle detected
+          println("\nCycle detection:")
+          val aqf = RDFoxHelpers.queryInternalPredicate(
+            data,
+            "AQ" :: Forward,
+            arity + 2
+          )
+          val aqb = RDFoxHelpers.queryInternalPredicate(
+            data,
+            "AQ" :: Backward,
+            arity + 2
+          )
+          println(aqf)
+          println(aqb)
+
+          // Forks detected
+          println("\nForks:")
+          val fk = RDFoxHelpers.queryInternalPredicate(
+            data,
+            "FK",
+            arity
+          )
+          println(fk)
+
+          // Spurious answers
+          println("\nSpurious answers")
+          val sp = RDFoxHelpers.queryInternalPredicate(
+            data,
+            "SP",
+            arity
+          )
+          println(sp)
+        }
+
+        // Close connection to RDFox
+        RDFoxHelpers.closeConnection(server, data)
+      }
+      case None => {}
+    }
+  }
+}
+
+/* Notes:
+ *
+ * To establish a connection with a local RDFox instance, do the
+ * following:
+ *
+ * ```
+ * val serverConnection : ServerConnection = ConnectionFactory.newServerConnection("rdfox:local", "", "")
+ * serverConnection.createDataStore("test","seq",new HashMap())
+ * val dataStoreConnection : DataStoreConnection = serverConnection.newDataStoreConnection("test")
+ * dataStoreConnection.importData(
+ *    UpdateType.ADDITION,
+ *    Prefixes.s_emptyPrefixes,
+ *    new File("./path/to/file")
+ * )
+ * ```
+ */
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
new file mode 100644
index 0000000..ac86e3d
--- /dev/null
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
@@ -0,0 +1,380 @@
+package uk.ac.ox.cs.rsacomb
+
+/* Java imports */
+import java.util.HashMap
+import java.util.stream.{Collectors, Stream}
+import java.io.File
+import org.semanticweb.owlapi.apibinding.OWLManager
+
+import org.semanticweb.owlapi.model.{OWLOntology, OWLAxiom}
+import org.semanticweb.owlapi.model.{
+  OWLClass,
+  OWLObjectProperty,
+  OWLSubObjectPropertyOfAxiom,
+  OWLObjectPropertyExpression,
+  OWLObjectSomeValuesFrom,
+  OWLSubClassOfAxiom
+}
+import org.semanticweb.owlapi.model.parameters.Imports
+import org.semanticweb.owlapi.reasoner.structural.StructuralReasonerFactory
+import org.semanticweb.owlapi.model.{IRI => OWLIRI}
+import uk.ac.manchester.cs.owl.owlapi.OWLObjectPropertyImpl
+
+import tech.oxfordsemantic.jrdfox.client.{UpdateType, DataStoreConnection}
+import tech.oxfordsemantic.jrdfox.logic.datalog.{
+  Rule,
+  TupleTableAtom,
+  Negation,
+  BodyFormula
+}
+import tech.oxfordsemantic.jrdfox.logic.expression.{
+  Term,
+  Variable,
+  IRI,
+  Resource
+}
+import tech.oxfordsemantic.jrdfox.logic.sparql.statement.SelectQuery
+
+/* Scala imports */
+import scala.collection.JavaConverters._
+import scala.collection.mutable.Set
+import scalax.collection.immutable.Graph
+import scalax.collection.GraphEdge.UnDiEdge
+
+/* 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.converter.{RDFoxAxiomConverter, SkolemStrategy}
+import uk.ac.ox.cs.rsacomb.implicits.RSAAxiom
+import uk.ac.ox.cs.rsacomb.suffix.{Empty, Forward, Backward, Inverse}
+import uk.ac.ox.cs.rsacomb.util.{RDFoxHelpers, RSA}
+
+object RSAOntology {
+
+  // Counter used to implement a simple fresh variable generator
+  private var counter = -1;
+
+  def apply(ontology: OWLOntology): RSAOntology = new RSAOntology(ontology)
+
+  def apply(ontology: File): RSAOntology =
+    new RSAOntology(loadOntology(ontology))
+
+  def genFreshVariable(): Variable = {
+    counter += 1
+    Variable.create(f"I$counter%03d")
+  }
+
+  private def loadOntology(onto: File): OWLOntology = {
+    val manager = OWLManager.createOWLOntologyManager()
+    manager.loadOntologyFromOntologyDocument(onto)
+  }
+}
+
+class RSAOntology(val ontology: OWLOntology) extends RSAAxiom {
+
+  // Gather TBox/RBox/ABox from original ontology
+  val tbox: List[OWLAxiom] =
+    ontology
+      .tboxAxioms(Imports.INCLUDED)
+      .collect(Collectors.toList())
+      .asScala
+      .toList
+
+  val rbox: List[OWLAxiom] =
+    ontology
+      .rboxAxioms(Imports.INCLUDED)
+      .collect(Collectors.toList())
+      .asScala
+      .toList
+
+  val abox: List[OWLAxiom] =
+    ontology
+      .aboxAxioms(Imports.INCLUDED)
+      .collect(Collectors.toList())
+      .asScala
+      .toList
+
+  val axioms: List[OWLAxiom] = abox ::: tbox ::: rbox
+
+  /* Retrieve individuals in the original ontology
+   */
+  val individuals: List[IRI] =
+    ontology
+      .getIndividualsInSignature()
+      .asScala
+      .map(_.getIRI)
+      .map(implicits.RDFox.owlapiToRdfoxIri)
+      .toList
+
+  val concepts: List[OWLClass] =
+    ontology.getClassesInSignature().asScala.toList
+
+  val roles: List[OWLObjectPropertyExpression] =
+    axioms
+      .flatMap(_.objectPropertyExpressionsInSignature)
+      .distinct
+
+  // OWLAPI reasoner for same easier tasks
+  private val reasoner =
+    (new StructuralReasonerFactory()).createReasoner(ontology)
+
+  /* Steps for RSA check
+   * 1) convert ontology axioms into LP rules
+   * 2) call RDFox on the onto and compute materialization
+   * 3) build graph from E(x,y) facts
+   * 4) check if the graph is tree-like
+   *    ideally this annotates the graph with info about the reasons
+   *    why the ontology might not be RSA. This could help a second
+   *    step of approximation of an Horn-ALCHOIQ to RSA
+   */
+  lazy val isRSA: Boolean = {
+
+    val unsafe = this.unsafeRoles
+
+    /* DEBUG: print rules in DL syntax and unsafe roles */
+    //val renderer = new DLSyntaxObjectRenderer()
+    //println("\nDL rules:")
+    //axioms.foreach(x => println(renderer.render(x)))
+    //println("\nUnsafe roles:")
+    //println(unsafe)
+
+    /* Ontology convertion into LP rules */
+    val datalog = for {
+      axiom <- axioms
+      visitor = new RDFoxAxiomConverter(
+        RSAOntology.genFreshVariable(),
+        unsafe,
+        SkolemStrategy.ConstantRSA(axiom.toString),
+        Empty
+      )
+      rule <- axiom.accept(visitor)
+    } yield rule
+
+    /* DEBUG: print datalog rules */
+    //println("\nDatalog roles:")
+    //datalog.foreach(println)
+
+    // Open connection with RDFox
+    val (server, data) = RDFoxHelpers.openConnection("RSACheck")
+    // Add Data (hardcoded for now)
+    //data.importData(UpdateType.ADDITION, RSA.Prefixes, ":a a :A .")
+
+    /* Add built-in rules
+     */
+    data.importData(
+      UpdateType.ADDITION,
+      RSA.Prefixes,
+      "rsa:E[?X,?Y] :- rsa:PE[?X,?Y], rsa:U[?X], rsa:U[?Y] ."
+    )
+
+    /* Add built-in rules
+     */
+    // data.importData(
+    //   UpdateType.ADDITION,
+    //   RSA.Prefixes,
+    //   "[?entity, a, ?superClass] :- [?entity, a, ?class], [?class, rdfs:subClassOf, ?superClass] ."
+    // )
+
+    /* Add ontology rules
+     */
+    data.addRules(datalog.asJava)
+
+    /* Build graph
+     */
+    val graph = this.rsaGraph(data);
+    //println(graph)
+
+    // Close connection to RDFox
+    RDFoxHelpers.closeConnection(server, data)
+
+    /* To check if the graph is tree-like we check for acyclicity in a
+     * undirected graph.
+     *
+     * TODO: Implement additional checks (taking into account equality)
+     */
+    graph.isAcyclic
+  }
+
+  lazy val unsafeRoles: List[OWLObjectPropertyExpression] = {
+
+    /* DEBUG: print rules in DL syntax */
+    //val renderer = new DLSyntaxObjectRenderer()
+
+    /* Checking for (1) unsafety condition:
+     *
+     *    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.
+     */
+    val unsafe1 = for {
+      axiom <- tbox
+      if axiom.isT5
+      role1 <- axiom.objectPropertyExpressionsInSignature
+      roleSuper =
+        role1 +: reasoner
+          .superObjectProperties(role1)
+          .collect(Collectors.toList())
+          .asScala
+      roleSuperInv = roleSuper.map(_.getInverseProperty)
+      axiom <- tbox
+      if axiom.isT3 && !axiom.isT3top
+      role2 <- axiom.objectPropertyExpressionsInSignature
+      if roleSuperInv.contains(role2)
+    } yield role1
+
+    /* Checking for (2) unsafety condition:
+     *
+     *    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.
+     *
+     */
+    val unsafe2 = for {
+      axiom <- tbox
+      if axiom.isT5
+      role1 <- axiom.objectPropertyExpressionsInSignature
+      roleSuper =
+        role1 +: reasoner
+          .superObjectProperties(role1)
+          .collect(Collectors.toList())
+          .asScala
+      roleSuperInv = roleSuper.map(_.getInverseProperty)
+      axiom <- tbox
+      if axiom.isT4
+      role2 <- axiom.objectPropertyExpressionsInSignature
+      if roleSuper.contains(role2) || roleSuperInv.contains(role2)
+    } yield role1
+
+    (unsafe1 ++ unsafe2).toList
+  }
+
+  private def rsaGraph(
+      data: DataStoreConnection
+  ): Graph[Resource, UnDiEdge] = {
+    val query = "SELECT ?X ?Y WHERE { ?X rsa:E ?Y }"
+    val answers = RDFoxHelpers.submitSelectQuery(data, query, RSA.Prefixes)
+    var edges: List[UnDiEdge[Resource]] = answers.map {
+      case n1 :: n2 :: _ => UnDiEdge(n1, n2)
+    }
+    Graph(edges: _*)
+  }
+
+  def filteringProgram(
+      query: SelectQuery,
+      nis: List[Term]
+  ): FilteringProgram =
+    new FilteringProgram(query, nis)
+
+  lazy val canonicalModel = new CanonicalModel(this)
+
+  // TODO: the following functions needs testing
+  def confl(
+      role: OWLObjectPropertyExpression
+  ): Set[OWLObjectPropertyExpression] = {
+
+    val invSuperRoles = reasoner
+      .superObjectProperties(role)
+      .collect(Collectors.toSet())
+      .asScala
+      .addOne(role)
+      .map(_.getInverseProperty)
+
+    invSuperRoles
+      .flatMap(x =>
+        reasoner
+          .subObjectProperties(x)
+          .collect(Collectors.toSet())
+          .asScala
+          .addOne(x)
+      )
+      .filterNot(_.isOWLBottomObjectProperty())
+      .filterNot(_.getInverseProperty.isOWLTopObjectProperty())
+  }
+
+  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] = {
+  //   // Assuming just one role in the signature of a T5 axiom
+  //   val roleR = axiom.objectPropertyExpressionsInSignature(0)
+  //   val conflR = this.confl(roleR)
+  //   // We just need the TBox to find
+  //   val tbox = ontology
+  //     .tboxAxioms(Imports.INCLUDED)
+  //     .collect(Collectors.toSet())
+  //     .asScala
+  //   for {
+  //     axiom1 <- tbox
+  //     // TODO: is this an optimization or an error?
+  //     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)
+  //     individual =
+  //       if (axiom.hashCode < axiom1.hashCode) {
+  //         RSA.rsa("v0_" ++ axiom1.hashCode.toString())
+  //       } else {
+  //         RSA.rsa("v1_" ++ axiom1.hashCode.toString())
+  //       }
+  //   } yield individual
+  // }
+
+  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_aux(classA, roleR, classB)
+  }
+
+  def cycle_aux(
+      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 unfold(axiom: OWLSubClassOfAxiom): Set[Term] =
+    this.self(axiom) | this.cycle(axiom)
+
+} // implicit class RSAOntology
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxAxiomConverter.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxAxiomConverter.scala
new file mode 100644
index 0000000..a8d1ffd
--- /dev/null
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxAxiomConverter.scala
@@ -0,0 +1,105 @@
+package uk.ac.ox.cs.rsacomb.converter
+
+import org.semanticweb.owlapi.model.{
+  OWLAxiom,
+  OWLSubClassOfAxiom,
+  OWLEquivalentClassesAxiom,
+  OWLObjectPropertyExpression
+}
+import org.semanticweb.owlapi.model.OWLAxiomVisitorEx
+
+import tech.oxfordsemantic.jrdfox.logic.datalog.{
+  Rule,
+  BodyFormula,
+  TupleTableAtom,
+  TupleTableName
+}
+import tech.oxfordsemantic.jrdfox.logic.expression.{
+  Term,
+  IRI,
+  Variable,
+  Literal
+}
+
+import scala.collection.JavaConverters._
+
+import org.semanticweb.owlapi.model.OWLSubObjectPropertyOfAxiom
+import org.semanticweb.owlapi.model.OWLObjectProperty
+import org.semanticweb.owlapi.model.OWLClassAssertionAxiom
+
+import uk.ac.ox.cs.rsacomb.RSAOntology
+import uk.ac.ox.cs.rsacomb.suffix.{RSASuffix, Empty}
+
+object RDFoxAxiomConverter {
+
+  def apply(
+      term: Term,
+      unsafe: List[OWLObjectPropertyExpression],
+      skolem: SkolemStrategy = SkolemStrategy.None,
+      suffix: RSASuffix = Empty
+  ): RDFoxAxiomConverter =
+    new RDFoxAxiomConverter(term, unsafe, skolem, suffix)
+
+} // object RDFoxAxiomConverter
+
+class RDFoxAxiomConverter(
+    term: Term,
+    unsafe: List[OWLObjectPropertyExpression],
+    skolem: SkolemStrategy,
+    suffix: RSASuffix
+) extends OWLAxiomVisitorEx[List[Rule]] {
+
+  override def visit(axiom: OWLSubClassOfAxiom): List[Rule] = {
+    // Skolemization is needed only for the head of an axiom
+    val subVisitor =
+      new RDFoxClassExprConverter(term, unsafe, SkolemStrategy.None, suffix)
+    val superVisitor = new RDFoxClassExprConverter(term, unsafe, skolem, suffix)
+    // Each visitor returns a `RDFoxRuleShards`, a tuple (res,ext):
+    // - the `res` List is a list of atoms resulting from the conversion
+    //   of the axiom.
+    // - for some Class Expressions appearing in the head of an Axiom,
+    //   the conversion might produce atoms that need to appear in the
+    //   body (and not in the head) of the rule. This is what the `ext`
+    //   List is for.
+    val sub = axiom.getSubClass.accept(subVisitor)
+    val sup = axiom.getSuperClass.accept(superVisitor)
+    val head = sup.res.asJava
+    val body = (sub.res ++ sup.ext).asJava
+    List(Rule.create(head, body))
+  }
+
+  override def visit(axiom: OWLEquivalentClassesAxiom): List[Rule] = {
+    for {
+      axiom1 <- axiom.asPairwiseAxioms.asScala.toList
+      axiom2 <- axiom1.asOWLSubClassOfAxioms.asScala.toList
+      rule <- axiom2.accept(this)
+    } yield rule
+  }
+
+  override def visit(axiom: OWLSubObjectPropertyOfAxiom): List[Rule] = {
+    val term1 = RSAOntology.genFreshVariable()
+    val subVisitor =
+      new RDFoxPropertyExprConverter(term, term1, suffix)
+    val superVisitor = new RDFoxPropertyExprConverter(term, term1, suffix)
+    val body: List[BodyFormula] = axiom.getSubProperty.accept(subVisitor)
+    val head: List[TupleTableAtom] = axiom.getSuperProperty.accept(superVisitor)
+    List(Rule.create(head.asJava, body.asJava))
+  }
+
+  override def visit(axiom: OWLClassAssertionAxiom): List[Rule] = {
+    val ind = axiom.getIndividual
+    if (ind.isNamed) {
+      val term = IRI.create(ind.asOWLNamedIndividual().getIRI.getIRIString)
+      val cls = axiom.getClassExpression
+      val visitor =
+        new RDFoxClassExprConverter(term, unsafe, SkolemStrategy.None, suffix)
+      val shard = cls.accept(visitor)
+      List(Rule.create(shard.res.asJava, shard.ext.asJava))
+    } else {
+      List()
+    }
+  }
+
+  def doDefault(axiom: OWLAxiom): List[Rule] = List()
+
+} // class RDFoxAxiomConverter
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxClassExprConverter.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxClassExprConverter.scala
new file mode 100644
index 0000000..c151c9a
--- /dev/null
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxClassExprConverter.scala
@@ -0,0 +1,160 @@
+package uk.ac.ox.cs.rsacomb.converter
+
+import scala.collection.JavaConverters._
+import java.util.stream.{Stream, Collectors}
+
+import org.semanticweb.owlapi.model.{
+  OWLClassExpression,
+  OWLClass,
+  OWLObjectSomeValuesFrom,
+  OWLObjectIntersectionOf,
+  OWLObjectOneOf,
+  OWLObjectMaxCardinality
+}
+import org.semanticweb.owlapi.model.OWLClassExpressionVisitorEx
+import tech.oxfordsemantic.jrdfox.logic.Datatype
+import tech.oxfordsemantic.jrdfox.logic.datalog.{
+  BindAtom,
+  TupleTableName,
+  TupleTableAtom
+}
+import tech.oxfordsemantic.jrdfox.logic.expression.{
+  Term,
+  Literal,
+  Variable,
+  FunctionCall,
+  IRI
+}
+
+import org.semanticweb.owlapi.model.OWLObjectPropertyExpression
+import org.semanticweb.owlapi.model.OWLObjectProperty
+
+import uk.ac.ox.cs.rsacomb.RSAOntology
+import uk.ac.ox.cs.rsacomb.suffix.{RSASuffix, Empty}
+import uk.ac.ox.cs.rsacomb.util.RSA
+
+object RDFoxClassExprConverter {
+
+  def apply(
+      term: Term,
+      unsafe: List[OWLObjectPropertyExpression] = List(),
+      skolem: SkolemStrategy = SkolemStrategy.None,
+      suffix: RSASuffix = Empty
+  ): RDFoxClassExprConverter =
+    new RDFoxClassExprConverter(term, unsafe, skolem, suffix)
+
+  def merge(rules: List[RDFoxRuleShards]): RDFoxRuleShards = {
+    rules.foldLeft(RDFoxRuleShards(List(), List())) { (r1, r2) =>
+      RDFoxRuleShards(
+        r1.res ++ r2.res,
+        r1.ext ++ r2.ext
+      )
+    }
+  }
+
+} // object RDFoxClassExprConverter
+
+class RDFoxClassExprConverter(
+    term: Term,
+    unsafe: List[OWLObjectPropertyExpression],
+    skolem: SkolemStrategy,
+    suffix: RSASuffix
+) extends OWLClassExpressionVisitorEx[RDFoxRuleShards] {
+
+  import uk.ac.ox.cs.rsacomb.implicits.RDFox._
+
+  // OWLClass
+  override def visit(expr: OWLClass): RDFoxRuleShards = {
+    val iri: IRI = if (expr.isTopEntity()) IRI.THING else expr.getIRI()
+    val atom = List(TupleTableAtom.rdf(term, IRI.RDF_TYPE, iri))
+    RDFoxRuleShards(atom, List())
+  }
+
+  // OWLObjectIntersectionOf
+  override def visit(expr: OWLObjectIntersectionOf): RDFoxRuleShards = {
+    val visitor = new RDFoxClassExprConverter(term, unsafe, skolem, suffix)
+    // TODO: maybe using `flatMap` instead of `merge` + `map` works as well
+    RDFoxClassExprConverter.merge(
+      expr.asConjunctSet.asScala.toList
+        .map((e: OWLClassExpression) => e.accept(visitor))
+    )
+  }
+
+  // OWLObjectOneOf
+  override def visit(expr: OWLObjectOneOf): RDFoxRuleShards = {
+    val visitor = RDFoxClassExprConverter(term, unsafe, skolem, suffix)
+    // TODO: review nominal handling. Here we are taking "just" one
+    val ind = expr.individuals
+      .collect(Collectors.toList())
+      .asScala
+      .filter(_.isOWLNamedIndividual)
+      .head // restricts to proper "nominals"
+      .asOWLNamedIndividual
+      .getIRI
+    val atom = List(
+      TupleTableAtom.rdf(term, IRI.SAME_AS, ind)
+    )
+    RDFoxRuleShards(atom, List())
+  }
+
+  // OWLObjectSomeValuesFrom
+  override def visit(expr: OWLObjectSomeValuesFrom): RDFoxRuleShards = {
+    val y = RSAOntology.genFreshVariable()
+    // Here we are assuming a role name
+    val prop = expr.getProperty()
+    // 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 (head, body, term1) = skolem match {
+      case SkolemStrategy.None        => (List(), List(), y)
+      case SkolemStrategy.Constant(c) => (List(), List(), c)
+      case SkolemStrategy.ConstantRSA(c) => {
+        if (unsafe.contains(prop))
+          (List(RSA.PE(term, c), RSA.U(c)), List(), c)
+        else
+          (List(), List(), c)
+      }
+      case SkolemStrategy.Standard(f) => {
+        (
+          List(),
+          List(BindAtom.create(FunctionCall.create("SKOLEM", f, term), y)),
+          y
+        )
+      }
+    }
+    val classVisitor =
+      new RDFoxClassExprConverter(term1, unsafe, skolem, suffix)
+    val classResult = expr.getFiller.accept(classVisitor)
+    val propertyVisitor = new RDFoxPropertyExprConverter(term, term1, suffix)
+    val propertyResult = expr.getProperty.accept(propertyVisitor)
+    RDFoxRuleShards(
+      classResult.res ++ propertyResult ++ head,
+      classResult.ext ++ body
+    )
+  }
+
+  // OWLObjectMaxCardinality
+  override def visit(expr: OWLObjectMaxCardinality): RDFoxRuleShards = {
+    // TODO: again, no hardcoded variables
+    val vars =
+      List(RSAOntology.genFreshVariable(), RSAOntology.genFreshVariable())
+    val classResult = RDFoxClassExprConverter.merge(
+      vars
+        .map(new RDFoxClassExprConverter(_, unsafe, skolem, suffix))
+        .map(expr.getFiller.accept(_))
+    )
+    val propertyResult =
+      vars
+        .map(new RDFoxPropertyExprConverter(term, _, suffix))
+        .map(expr.getProperty.accept(_))
+        .flatten
+    RDFoxRuleShards(
+      List(TupleTableAtom.rdf(vars(0), IRI.SAME_AS, vars(1))),
+      classResult.res ++ propertyResult
+    )
+  }
+
+  def doDefault(expr: OWLClassExpression): RDFoxRuleShards =
+    RDFoxRuleShards(List(), List())
+
+} // class RDFoxClassExprConverter
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxPropertyExprConverter.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxPropertyExprConverter.scala
new file mode 100644
index 0000000..94c7887
--- /dev/null
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxPropertyExprConverter.scala
@@ -0,0 +1,35 @@
+package uk.ac.ox.cs.rsacomb.converter
+
+import org.semanticweb.owlapi.model.{OWLPropertyExpression, OWLObjectProperty}
+import org.semanticweb.owlapi.model.OWLPropertyExpressionVisitorEx
+
+import tech.oxfordsemantic.jrdfox.logic.datalog.TupleTableAtom
+import tech.oxfordsemantic.jrdfox.logic.expression.{Term, IRI, Literal}
+
+import org.semanticweb.owlapi.model.OWLObjectInverseOf
+
+import uk.ac.ox.cs.rsacomb.suffix.{RSASuffix, Inverse}
+
+class RDFoxPropertyExprConverter(
+    term1: Term,
+    term2: Term,
+    suffix: RSASuffix
+) extends OWLPropertyExpressionVisitorEx[List[TupleTableAtom]] {
+
+  // Automatically converts OWLAPI types into RDFox equivalent types.
+  import uk.ac.ox.cs.rsacomb.implicits.RDFox._
+
+  override def visit(expr: OWLObjectProperty): List[TupleTableAtom] = {
+    val base = expr.getIRI.getIRIString
+    val pred = IRI.create(base :: suffix)
+    List(TupleTableAtom.rdf(term1, pred, term2))
+  }
+
+  override def visit(expr: OWLObjectInverseOf): List[TupleTableAtom] = {
+    val visitor = new RDFoxPropertyExprConverter(term1, term2, suffix + Inverse)
+    expr.getInverse.accept(visitor)
+  }
+
+  def doDefault(expr: OWLPropertyExpression): List[TupleTableAtom] = List()
+
+} // class RDFoxPropertyExprConverter
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxRuleShards.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxRuleShards.scala
new file mode 100644
index 0000000..c88cf3c
--- /dev/null
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxRuleShards.scala
@@ -0,0 +1,5 @@
+package uk.ac.ox.cs.rsacomb.converter
+
+import tech.oxfordsemantic.jrdfox.logic.datalog.{TupleTableAtom, BodyFormula}
+
+case class RDFoxRuleShards(res: List[TupleTableAtom], ext: List[BodyFormula])
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/SkolemStrategy.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/SkolemStrategy.scala
new file mode 100644
index 0000000..0d72226
--- /dev/null
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/SkolemStrategy.scala
@@ -0,0 +1,78 @@
+package uk.ac.ox.cs.rsacomb.converter
+
+import tech.oxfordsemantic.jrdfox.logic.Datatype
+import tech.oxfordsemantic.jrdfox.logic.expression.{Literal, IRI}
+
+sealed trait SkolemStrategy
+
+object SkolemStrategy {
+  // TODO: might want to use something else other than `hashCode` as a
+  // function to generate a fresh function/constant
+
+  /* No skolemization at all.
+   *
+   * From
+   *    ∃R.A ⊑ B
+   * to
+   *    R(x,y), B(y) -> B(x)
+   */
+  case object None extends SkolemStrategy
+
+  /* Functional skolemization
+   *
+   * From
+   *    A ⊑ ∃R.B
+   * to
+   *    A(x) -> R(x,f(x)), B(f(x))
+   * for f, fresh function associated with the input axiom
+   *
+   * In RDFox this can represented combining the BIND operator with the
+   * SKOLEM operator as such:
+   *    A(x), BIND(y, SKOLEM("f", x)) -> R(x,y), B(y)
+   * The first argument of a SKOLEM call is a literal string (ideally
+   * identifing the simulated function name).
+   *
+   * NOTE: this requirement for the SKOLEM operator is not enforced by
+   * RDFox, that will fail silently if omitted.
+   */
+  case class Standard(func: Literal) extends SkolemStrategy
+  object Standard {
+    def apply(axiom: String) =
+      new Standard(
+        Literal.create(genFunctionString(axiom), Datatype.XSD_STRING)
+      )
+    def genFunctionString(str: String) = "f_" ++ str.hashCode.toString
+  }
+
+  /* Constant skolemization
+   *
+   * From
+   *    A ⊑ ∃R.B
+   * to
+   *    A(y) -> R(x,c), B(c)
+   * for c, fresh constant associated with the input axiom
+   */
+  case class Constant(const: IRI) extends SkolemStrategy
+  object Constant {
+    def apply(axiom: String) =
+      new Constant(IRI.create(genConstantString(axiom)))
+    def genConstantString(str: String) = "c_" ++ str.hashCode.toString
+  }
+
+  /* (RSA) Constant skolemization
+   * This is a special skolemization option to introduce additional atoms for RSA
+   * checking algorithm.
+   *
+   * From
+   *    A ⊑ ∃R.B
+   * to
+   *    A(y) -> R(x,c), PE(x,c), B(c)
+   * for c, fresh constant associated with the input axiom and PE an internal predicate.
+   */
+  case class ConstantRSA(const: IRI) extends SkolemStrategy
+  object ConstantRSA {
+    def apply(axiom: String) =
+      new ConstantRSA(IRI.create(genConstantString(axiom)))
+    def genConstantString(str: String) = "c_" ++ str.hashCode.toString
+  }
+}
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/implicits/JavaCollections.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/implicits/JavaCollections.scala
new file mode 100644
index 0000000..3b621f4
--- /dev/null
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/implicits/JavaCollections.scala
@@ -0,0 +1,13 @@
+package uk.ac.ox.cs.rsacomb.implicits
+
+import scala.collection.JavaConverters._
+
+object JavaCollections {
+
+  implicit def javaToScalaList[A](list: java.util.List[A]): List[A] =
+    list.asScala.toList
+
+  implicit def scalaToJavaList[A](list: List[A]): java.util.List[A] =
+    list.asJava
+
+}
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/implicits/RDFox.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/implicits/RDFox.scala
new file mode 100644
index 0000000..0462a47
--- /dev/null
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/implicits/RDFox.scala
@@ -0,0 +1,20 @@
+package uk.ac.ox.cs.rsacomb.implicits
+
+import tech.oxfordsemantic.jrdfox.logic.expression.{IRI => RDFoxIRI}
+import org.semanticweb.owlapi.model.{IRI => OWLIRI}
+
+object RDFox {
+
+  implicit def rdfoxToOwlapiIri(iri: RDFoxIRI): OWLIRI = {
+    OWLIRI.create(iri.getIRI)
+  }
+
+  implicit def owlapiToRdfoxIri(iri: OWLIRI): RDFoxIRI = {
+    RDFoxIRI.create(iri.getIRIString())
+  }
+
+  implicit def stringToRdfoxIri(iri: String): RDFoxIRI = {
+    RDFoxIRI.create(iri)
+  }
+
+}
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
new file mode 100644
index 0000000..a8afc72
--- /dev/null
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/implicits/RSAAtom.scala
@@ -0,0 +1,88 @@
+package uk.ac.ox.cs.rsacomb.implicits
+
+import tech.oxfordsemantic.jrdfox.logic.Datatype
+import tech.oxfordsemantic.jrdfox.logic.expression.{Literal, FunctionCall}
+import tech.oxfordsemantic.jrdfox.logic.datalog.{
+  BindAtom,
+  TupleTableAtom,
+  TupleTableName
+}
+import tech.oxfordsemantic.jrdfox.logic.expression.{IRI}
+import scala.collection.JavaConverters._
+
+import uk.ac.ox.cs.rsacomb.suffix.{RSASuffix, Nth}
+import uk.ac.ox.cs.rsacomb.RSAOntology
+
+/* Is this the best way to determine if an atom is an RDF triple?
+ * Note that we can't use `getNumberOfArguments()` because is not
+ * "consistent":
+ * - for an atom created with `rdf(<term1>, <term2>, <term3>)`,
+ * `getNumberOfArguments` returns 3
+ * - for an atom created with `Atom.create(<tupletablename>, <term1>,
+ * <term2>, <term3>)`, `getNumberOfArguments()` returns 3
+ *
+ * This is probably because `Atom.rdf(...) is implemented as:
+ * ```scala
+ *  def rdf(term1: Term, term2: Term, term3: Term): Atom =
+ *    Atom.create(TupleTableName.create("internal:triple"), term1, term2, term3)
+ * ```
+ */
+
+trait RSAAtom {
+
+  implicit class RSAAtom(val atom: TupleTableAtom) {
+
+    import RDFox._
+
+    val name: String = atom.getTupleTableName.getName
+
+    val isRDF: Boolean = name == "internal:triple"
+
+    val isClassAssertion: Boolean = {
+      isRDF && {
+        val pred = atom.getArguments.get(1)
+        pred == IRI.RDF_TYPE
+      }
+    }
+
+    val isRoleAssertion: Boolean = isRDF && !isClassAssertion
+
+    def <<(suffix: RSASuffix): TupleTableAtom =
+      if (isRDF) {
+        val subj = atom.getArguments.get(0)
+        val pred = atom.getArguments.get(1)
+        val obj = atom.getArguments.get(2)
+        if (isClassAssertion) {
+          val obj1 = obj match {
+            case iri: IRI => IRI.create(iri.getIRI :: suffix)
+            case other    => other
+          }
+          TupleTableAtom.rdf(subj, pred, obj1)
+        } else {
+          val pred1 = pred match {
+            case iri: IRI => IRI.create(iri.getIRI :: suffix)
+            case other    => other
+          }
+          TupleTableAtom.rdf(subj, pred1, obj)
+        }
+      } else {
+        val ttname = TupleTableName.create(name :: suffix)
+        TupleTableAtom.create(ttname, atom.getArguments())
+      }
+
+    lazy val reified: (Option[BindAtom], List[TupleTableAtom]) =
+      if (isRDF) {
+        (None, List(atom))
+      } else {
+        val bvar = RSAOntology.genFreshVariable()
+        val str = Literal.create(name, Datatype.XSD_STRING)
+        val args = atom.getArguments.asScala.toList
+        val skolem = FunctionCall.create("SKOLEM", str :: args: _*)
+        val bind = BindAtom.create(skolem, bvar)
+        val atoms = args.zipWithIndex
+          .map { case (t, i) => TupleTableAtom.rdf(bvar, name :: Nth(i), t) }
+        (Some(bind), atoms)
+      }
+  }
+
+}
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/implicits/RSAAxiom.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/implicits/RSAAxiom.scala
new file mode 100644
index 0000000..e39d5b2
--- /dev/null
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/implicits/RSAAxiom.scala
@@ -0,0 +1,155 @@
+package uk.ac.ox.cs.rsacomb.implicits
+
+/* Java imports */
+import org.semanticweb.owlapi.model.{
+  OWLAxiom,
+  OWLSubClassOfAxiom,
+  OWLEquivalentClassesAxiom
+}
+import org.semanticweb.owlapi.model.{
+  OWLObjectPropertyExpression,
+  OWLSubObjectPropertyOfAxiom,
+  OWLClass,
+  OWLClassExpression,
+  OWLObjectSomeValuesFrom,
+  OWLObjectMaxCardinality
+}
+import org.semanticweb.owlapi.model.ClassExpressionType
+import org.semanticweb.owlapi.model.{
+  OWLAxiomVisitorEx,
+  OWLClassExpressionVisitorEx
+}
+import org.semanticweb.owlapi.model.OWLObjectProperty
+import scala.collection.JavaConverters._
+
+/* Wrapper trait for the implicit class `RSAAxiom`.
+ */
+trait RSAAxiom {
+
+  /* Identifies some of the axiom types in a Horn-ALCHOIQ ontology
+   * in normal form. Refer to the paper for more details on the
+   * chosen names.
+   */
+  private sealed trait RSAAxiomType
+  private object RSAAxiomType {
+    case object T3 extends RSAAxiomType // ∃R.A ⊑ B
+    case object T3top extends RSAAxiomType // ∃R.⊤ ⊑ B
+    case object T4 extends RSAAxiomType // A ⊑ ≤1R.B
+    case object T5 extends RSAAxiomType // A ⊑ ∃R.B
+  }
+
+  object RSAAxiom {
+
+    def hashed(
+        cls1: OWLClass,
+        prop: OWLObjectPropertyExpression,
+        cls2: OWLClass
+    ): String =
+      (cls1, prop, cls2).hashCode.toString
+
+  }
+
+  /* Implements additional features on top of `OWLAxiom` from
+   * the OWLAPI.
+   */
+  implicit class RSAAxiom(axiom: OWLAxiom) {
+
+    /* Detecting axiom types:
+     *
+     * In order to reason about role unsafety in Horn-ALCHOIQ
+     * ontologies we need to detect and filter axioms by their
+     * "type".
+     *
+     * This is a simple implementation following the Visitor
+     * pattern imposed by the OWLAPI.
+     */
+    private class RSAAxiomTypeDetector(t: RSAAxiomType)
+        extends OWLAxiomVisitorEx[Boolean] {
+      override def visit(axiom: OWLSubClassOfAxiom): Boolean = {
+        val sub = axiom.getSubClass().getClassExpressionType()
+        val sup = axiom.getSuperClass().getClassExpressionType()
+        t match {
+          case RSAAxiomType.T3top => // ∃R.⊤ ⊑ B
+            axiom.isT3 && axiom
+              .getSubClass()
+              .asInstanceOf[OWLObjectSomeValuesFrom]
+              .getFiller
+              .isOWLThing
+          case RSAAxiomType.T3 => // ∃R.A ⊑ B
+            sub == ClassExpressionType.OBJECT_SOME_VALUES_FROM && sup == ClassExpressionType.OWL_CLASS
+          case RSAAxiomType.T4 => // A ⊑ ≤1R.B
+            sub == ClassExpressionType.OWL_CLASS && sup == ClassExpressionType.OBJECT_MAX_CARDINALITY
+          case RSAAxiomType.T5 => // A ⊑ ∃R.B
+            sub == ClassExpressionType.OWL_CLASS && sup == ClassExpressionType.OBJECT_SOME_VALUES_FROM
+        }
+      }
+
+      override def visit(axiom: OWLEquivalentClassesAxiom): Boolean = {
+        // TODO
+        false
+      }
+
+      def doDefault(axiom: OWLAxiom): Boolean = false
+    }
+
+    private def isOfType(t: RSAAxiomType): Boolean = {
+      val visitor = new RSAAxiomTypeDetector(t)
+      axiom.accept(visitor)
+    }
+
+    /* Exposed methods */
+    def isT3top: Boolean = isOfType(RSAAxiomType.T3top)
+    def isT3: Boolean = isOfType(RSAAxiomType.T3)
+    def isT4: Boolean = isOfType(RSAAxiomType.T4)
+    def isT5: Boolean = isOfType(RSAAxiomType.T5)
+
+    /* Extracting ObjectPropertyExpressions from axioms
+     *
+     * This extracts all ObjectPropertyExpressions from a given
+     * axiom. While the implementation is generic we use it on axioms
+     * of specific types (see above).
+     *
+     * NOTE: it is not possible to use the `objectPropertyInSignature`
+     * method of `OWLAxiom` because it returns all "role names" involved
+     * in the signature of an axiom. In particular we won't get the inverse
+     * of a role if this appears in the axiom (but we will get the role
+     * itself instead).
+     */
+    lazy val objectPropertyExpressionsInSignature
+        : List[OWLObjectPropertyExpression] =
+      axiom match {
+        case a: OWLSubClassOfAxiom =>
+          rolesInExpr(a.getSubClass) ++ rolesInExpr(a.getSuperClass)
+        case a: OWLEquivalentClassesAxiom =>
+          a.getClassExpressions.asScala.toList.flatMap(rolesInExpr(_))
+        case a: OWLSubObjectPropertyOfAxiom =>
+          List(a.getSubProperty, a.getSuperProperty)
+        case _ => List()
+      }
+
+    private def rolesInExpr(
+        expr: OWLClassExpression
+    ): List[OWLObjectPropertyExpression] =
+      expr match {
+        case e: OWLObjectSomeValuesFrom => List(e.getProperty)
+        case e: OWLObjectMaxCardinality => List(e.getProperty)
+        case _                          => List()
+      }
+
+    lazy val toTriple: Option[(OWLClass, OWLObjectProperty, OWLClass)] =
+      for {
+        subClass <- Some(axiom) collect { case a: OWLSubClassOfAxiom => a }
+        cls1 <- Some(subClass.getSubClass) collect { case a: OWLClass => a }
+        someValues <- Some(subClass.getSuperClass) collect {
+          case a: OWLObjectSomeValuesFrom => a
+        }
+        prop <- Some(someValues.getProperty) collect {
+          case a: OWLObjectProperty => a
+        }
+        cls2 <- Some(someValues.getFiller) collect { case a: OWLClass => a }
+      } yield (cls1, prop, cls2)
+
+    lazy val hashed: String = (RSAAxiom.hashed _) tupled toTriple.get
+  }
+
+} // trait RSAAxiom
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/suffix/RSASuffix.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/suffix/RSASuffix.scala
new file mode 100644
index 0000000..b22910b
--- /dev/null
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/suffix/RSASuffix.scala
@@ -0,0 +1,31 @@
+package uk.ac.ox.cs.rsacomb.suffix
+
+import org.semanticweb.owlapi.model.{
+  OWLPropertyExpression,
+  OWLObjectInverseOf,
+  OWLObjectProperty
+}
+
+import tech.oxfordsemantic.jrdfox.logic.expression.{IRI}
+import tech.oxfordsemantic.jrdfox.logic.datalog.{TupleTableAtom, TupleTableName}
+
+object RSASuffix {
+
+  def apply(suffix: String => String): RSASuffix = new RSASuffix(suffix)
+
+}
+
+class RSASuffix(val suffix: String => String) {
+
+  def +(that: RSASuffix): RSASuffix =
+    new RSASuffix(this.suffix andThen that.suffix)
+
+  def ::(str: String): String = this suffix str
+
+}
+
+case object Empty extends RSASuffix(identity)
+case object Forward extends RSASuffix((s) => s"${s}_f")
+case object Backward extends RSASuffix((s) => s"${s}_b")
+case object Inverse extends RSASuffix((s) => s"${s}_inv")
+case class Nth(n: Int) extends RSASuffix((s) => s"${s}_$n")
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/util/RDFoxHelpers.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/util/RDFoxHelpers.scala
new file mode 100644
index 0000000..fd9e1c5
--- /dev/null
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/util/RDFoxHelpers.scala
@@ -0,0 +1,100 @@
+package uk.ac.ox.cs.rsacomb.util
+
+import java.util.{Map => JMap, HashMap => JHashMap}
+import java.io.StringReader
+import tech.oxfordsemantic.jrdfox.Prefixes
+import tech.oxfordsemantic.jrdfox.client.{
+  ConnectionFactory,
+  ServerConnection,
+  DataStoreConnection
+}
+import tech.oxfordsemantic.jrdfox.formats.SPARQLParser
+import tech.oxfordsemantic.jrdfox.logic.expression.Resource
+import tech.oxfordsemantic.jrdfox.logic.sparql.statement.SelectQuery
+
+import uk.ac.ox.cs.rsacomb.suffix.Nth
+
+object RDFoxHelpers {
+
+  def openConnection(
+      dataStore: String,
+      opts: JMap[String, String] = new JHashMap[String, String]()
+  ): (ServerConnection, DataStoreConnection) = {
+    /* Create local server connection
+     */
+    val serverUrl = "rdfox:local"
+    val role = ""
+    val password = ""
+    val server =
+      ConnectionFactory.newServerConnection(serverUrl, role, password)
+
+    /* Create datastore connection
+     */
+    // parameters.put("owl-in-rdf-support", "relaxed")
+    // parameters.put("equality", "noUNA")
+    server.createDataStore(dataStore, "par-complex-nn", opts)
+    val data = server.newDataStoreConnection(dataStore)
+
+    (server, data)
+  }
+
+  def parseSelectQuery(
+      query: String,
+      prefixes: Prefixes = new Prefixes()
+  ): Option[SelectQuery] = {
+    val parser = new SPARQLParser(
+      prefixes,
+      new StringReader(query)
+    )
+    parser.parseSingleQuery() match {
+      case q: SelectQuery => Some(q)
+      case _              => None
+    }
+  }
+
+  def submitSelectQuery(
+      data: DataStoreConnection,
+      query: String,
+      prefixes: Prefixes = new Prefixes(),
+      opts: JMap[String, String] = new JHashMap[String, String]()
+  ): List[List[Resource]] = {
+    val cursor = data.createCursor(prefixes, query, opts)
+    var answers: List[List[Resource]] = List()
+    var mul = cursor.open()
+    while (mul > 0) {
+      val answer =
+        (0 until cursor.getArity).map(cursor.getResource(_)).toList
+      answers = answer :: answers
+      mul = cursor.advance()
+    }
+    cursor.close();
+    answers
+  }
+
+  def queryInternalPredicate(
+      data: DataStoreConnection,
+      pred: String,
+      arity: Int,
+      opts: JMap[String, String] = new JHashMap[String, String]()
+  ): List[List[Resource]] = {
+    var query = "SELECT"
+    for (i <- 0 until arity) {
+      query ++= s" ?X$i"
+    }
+    query ++= " WHERE {"
+    for (i <- 0 until arity) {
+      query ++= s" ?S rsa:${pred :: Nth(i)} ?X$i ."
+    }
+    query ++= " }"
+    submitSelectQuery(data, query, RSA.Prefixes, opts)
+  }
+
+  def closeConnection(
+      server: ServerConnection,
+      data: DataStoreConnection
+  ): Unit = {
+    server.close();
+    data.close();
+  }
+
+}
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/util/RSA.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/util/RSA.scala
new file mode 100644
index 0000000..f9ff59b
--- /dev/null
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/util/RSA.scala
@@ -0,0 +1,100 @@
+package uk.ac.ox.cs.rsacomb.util
+
+/* Java imports */
+import java.util.Map
+
+import tech.oxfordsemantic.jrdfox.formats.SPARQLParser
+import tech.oxfordsemantic.jrdfox.Prefixes
+import tech.oxfordsemantic.jrdfox.logic.datalog.{
+  TupleTableAtom,
+  TupleTableName,
+  Negation
+}
+import tech.oxfordsemantic.jrdfox.logic.expression.{Term, Variable, IRI}
+import org.semanticweb.owlapi.model.OWLOntology
+import org.semanticweb.owlapi.model.{
+  OWLAxiom,
+  OWLClass,
+  OWLObjectPropertyExpression
+}
+
+import uk.ac.ox.cs.rsacomb.suffix.RSASuffix
+
+// Debug only
+import scala.collection.JavaConverters._
+
+object RSA {
+
+  val Prefixes: Prefixes = new Prefixes()
+  Prefixes.declarePrefix("rsa:", "http://www.cs.ox.ac.uk/isg/rsa/")
+
+  private def atom(name: IRI, vars: List[Term]) =
+    TupleTableAtom.create(TupleTableName.create(name.getIRI), vars: _*)
+
+  def PE(t1: Term, t2: Term) =
+    TupleTableAtom.rdf(t1, RSA("PE"), t2)
+
+  def U(t: Term) =
+    TupleTableAtom.rdf(t, IRI.RDF_TYPE, RSA("U"))
+
+  def In(t: Term)(implicit set: Term) =
+    TupleTableAtom.rdf(t, RSA("In"), set)
+
+  def notIn(t: Term)(implicit set: Term) = Negation.create(In(t)(set))
+
+  def congruent(t1: Term, t2: Term) =
+    TupleTableAtom.rdf(t1, RSA("congruent"), t2)
+
+  def QM(implicit variables: (List[Term], List[Term])) = {
+    val (answer, bounded) = variables
+    atom(RSA("QM"), answer ::: bounded)
+  }
+
+  def ID(t1: Term, t2: Term)(implicit variables: (List[Term], List[Term])) = {
+    val (answer, bounded) = variables
+    atom(RSA("ID"), (answer ::: bounded) :+ t1 :+ t2)
+  }
+
+  def Named(t: Term) =
+    TupleTableAtom.rdf(t, IRI.RDF_TYPE, RSA("Named"))
+
+  def Thing(t: Term) =
+    TupleTableAtom.rdf(t, IRI.RDF_TYPE, IRI.THING)
+
+  def NI(t: Term) =
+    TupleTableAtom.rdf(t, IRI.RDF_TYPE, RSA("NI"))
+
+  def TQ(t1: Term, t2: Term, sx: RSASuffix)(implicit
+      variables: (List[Term], List[Term])
+  ) = {
+    val (answer, bounded) = variables
+    atom(RSA("TQ" :: sx), (answer ::: bounded) :+ t1 :+ t2)
+  }
+
+  def AQ(t1: Term, t2: Term, sx: RSASuffix)(implicit
+      variables: (List[Term], List[Term])
+  ) = {
+    val (answer, bounded) = variables
+    atom(RSA("AQ" :: sx), (answer ::: bounded) :+ t1 :+ t2)
+  }
+
+  def FK(implicit variables: (List[Term], List[Term])) = {
+    val (answer, bounded) = variables
+    atom(RSA("FK"), answer ::: bounded)
+  }
+
+  def SP(implicit variables: (List[Term], List[Term])) = {
+    val (answer, bounded) = variables
+    atom(RSA("SP"), answer ::: bounded)
+  }
+
+  def Ans(implicit variables: (List[Term], List[Term])) = {
+    val (answer, _) = variables
+    atom(RSA("Ans"), answer)
+  }
+
+  def apply(name: Any): IRI =
+    IRI.create(
+      Prefixes.getPrefixIRIsByPrefixName.get("rsa:").getIRI + name.toString
+    )
+}