6 files changed, 641 insertions, 129 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 0f3b16a..bcc336a 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala
@@ -3,9 +3,10 @@ package uk.ac.ox.cs.rsacomb
 import org.semanticweb.owlapi.model.{OWLObjectInverseOf, OWLObjectProperty}
 import org.semanticweb.owlapi.model.{
   OWLClass,
+  OWLLogicalAxiom,
   // OWLObjectProperty,
   OWLSubObjectPropertyOfAxiom,
-  // OWLObjectPropertyExpression,
+  OWLObjectPropertyExpression,
   OWLObjectSomeValuesFrom,
   OWLSubClassOfAxiom
 }
@@ -25,10 +26,11 @@ import tech.oxfordsemantic.jrdfox.logic.expression.{
 
 import uk.ac.ox.cs.rsacomb.converter.{
   SkolemStrategy,
-  RDFoxAxiomConverter,
-  RDFoxPropertyExprConverter
+  RDFoxConverter
+  // RDFoxAxiomConverter,
+  // RDFoxPropertyExprConverter
 }
-import uk.ac.ox.cs.rsacomb.suffix.{Empty, Forward, Backward, Inverse}
+import uk.ac.ox.cs.rsacomb.suffix._
 import uk.ac.ox.cs.rsacomb.util.RSA
 
 class CanonicalModel(val ontology: RSAOntology) {
@@ -107,22 +109,28 @@ class CanonicalModel(val ontology: RSAOntology) {
     )
   }
 
-  val rules: List[Rule] = {
+  val (facts, rules): (List[TupleTableAtom], List[Rule]) = {
     // Compute rules from ontology axioms
-    val rules = ontology.axioms.flatMap(_.accept(RuleGenerator))
-    // Return full set of rules
-    rules ::: rolesAdditionalRules ::: topAxioms ::: equalityAxioms
+    val (facts, rules) = {
+      val term = RSAOntology.genFreshVariable()
+      val unsafe = ontology.unsafeRoles
+      val skolem = SkolemStrategy.None
+      val suffix = Empty
+      ontology.axioms
+        .map(CanonicalModelConverter.convert(_, term, unsafe, skolem, suffix))
+        .unzip
+    }
+    (
+      facts.flatten,
+      rolesAdditionalRules ::: topAxioms ::: equalityAxioms ::: rules.flatten
+    )
   }
 
-  object RuleGenerator
-      extends RDFoxAxiomConverter(
-        Variable.create("X"),
-        ontology.unsafeRoles,
-        SkolemStrategy.None,
-        Empty
-      ) {
+  object CanonicalModelConverter extends RDFoxConverter {
 
-    private def rules1(axiom: OWLSubClassOfAxiom): List[Rule] = {
+    private def rules1(
+        axiom: OWLSubClassOfAxiom
+    ): Result = {
       val unfold = ontology.unfold(axiom).toList
       // Fresh Variables
       val v0 = RSA("v0_" ++ axiom.hashed)
@@ -134,13 +142,9 @@ class CanonicalModel(val ontology: RSAOntology) {
         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 prop =
+          axiom.getSuperClass.asInstanceOf[OWLObjectSomeValuesFrom].getProperty
+        super.convert(prop, varX, v0, Forward)
       }
       val atomB: TupleTableAtom = {
         val cls = axiom.getSuperClass
@@ -154,12 +158,12 @@ class CanonicalModel(val ontology: RSAOntology) {
       // 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 facts = unfold map RSA.In
       val rules = List(
         Rule.create(roleRf, atomA, RSA.NotIn(varX)),
         Rule.create(atomB, atomA, RSA.NotIn(varX))
       )
-      facts ++ rules
+      (facts, rules)
     }
 
     private def rules2(axiom: OWLSubClassOfAxiom): List[Rule] = {
@@ -177,11 +181,8 @@ class CanonicalModel(val ontology: RSAOntology) {
           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 roleRf(t1: Term, t2: Term): TupleTableAtom =
+          super.convert(roleR, t1, t2, Forward)
         def atomB(t: Term): TupleTableAtom = {
           val cls = axiom.getSuperClass
             .asInstanceOf[OWLObjectSomeValuesFrom]
@@ -215,11 +216,8 @@ class CanonicalModel(val ontology: RSAOntology) {
         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
-      }
+      def roleRf(t: Term): TupleTableAtom =
+        super.convert(roleR, t, v1, Forward)
       val atomB: TupleTableAtom = {
         val cls = axiom.getSuperClass
           .asInstanceOf[OWLObjectSomeValuesFrom]
@@ -236,46 +234,37 @@ class CanonicalModel(val ontology: RSAOntology) {
       }
     }
 
-    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)
+    override def convert(
+        axiom: OWLLogicalAxiom,
+        term: Term,
+        unsafe: List[OWLObjectPropertyExpression],
+        skolem: SkolemStrategy,
+        suffix: RSASuffix
+    ): Result =
+      axiom match {
+
+        case a: OWLSubClassOfAxiom if a.isT5 => {
+          val role = axiom.objectPropertyExpressionsInSignature(0)
+          if (unsafe contains role) {
+            val skolem = SkolemStrategy.Standard(a.toString)
+            super.convert(a, term, unsafe, skolem, Forward)
+          } else {
+            val (f1, r1) = rules1(a)
+            (f1, r1 ::: rules2(a) ::: rules3(a))
+          }
         }
-      } 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)
-    }
+        case a: OWLSubObjectPropertyOfAxiom => {
+          val (factsF, rulesF) =
+            super.convert(a, term, unsafe, SkolemStrategy.None, Forward)
+          val (factsB, rulesB) =
+            super.convert(a, term, unsafe, SkolemStrategy.None, Backward)
+          (factsF ::: factsB, rulesF ::: rulesB)
+        }
 
+        case a => super.convert(a, term, unsafe, skolem, suffix)
+
+      }
   }
 
 }
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/FilteringProgram.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/FilteringProgram.scala
index 52be937..4e533c6 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/FilteringProgram.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/FilteringProgram.scala
@@ -76,6 +76,15 @@ class FilteringProgram(query: ConjunctiveQuery, constants: List[Term]) {
   val nis: Rule =
     Rule.create(RSA.NI(varX), RSA.Congruent(varX, varY), RSA.Named(varY))
 
+  /** Initializes instances of `rsa:Named`.
+    *
+    * They represent the set of constants appearing in the original
+    * ontology.
+    *
+    * @note corresponds to rules 2 in Table 3.
+    */
+  val facts = constants map RSA.Named
+
   /** Collection of filtering program rules. */
   val rules: List[Rule] =
     nis :: {
@@ -89,15 +98,6 @@ class FilteringProgram(query: ConjunctiveQuery, constants: List[Term]) {
         */
       val r1 = Rule.create(RSA.QM, query.atoms: _*)
 
-      /** Initializes instances of `rsa:Named`.
-        *
-        * They represent the set of constants appearing in the original
-        * ontology.
-        *
-        * @note corresponds to rules 2 in Table 3.
-        */
-      val r2 = constants.map(c => Rule.create(RSA.Named(c)))
-
       /** Initializes instances of `rsa:ID`.
         *
         * They are initialized as a minimal congruence relation over the
@@ -307,7 +307,7 @@ class FilteringProgram(query: ConjunctiveQuery, constants: List[Term]) {
         */
       val r9 = Rule.create(RSA.Ans, RSA.QM, not(RSA.SP))
 
-      (r1 :: r2 :::
+      (r1 ::
         r3a ::: r3b :: r3c ::
         r4a ::: r4b ::: r4c :::
         r5a ::: r5b ::: r5c :::
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 4dd554a..a965ef9 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
@@ -7,13 +7,15 @@ import java.util.stream.{Collectors, Stream}
 import java.io.File
 import org.semanticweb.owlapi.apibinding.OWLManager
 import org.semanticweb.owlapi.util.OWLOntologyMerger
-import org.semanticweb.owlapi.model.{OWLOntology, OWLAxiom}
+import org.semanticweb.owlapi.model.{OWLOntology, OWLAxiom, OWLLogicalAxiom}
 import org.semanticweb.owlapi.model.{
   OWLClass,
+  OWLClassExpression,
   OWLObjectProperty,
   OWLSubObjectPropertyOfAxiom,
   OWLObjectPropertyExpression,
   OWLObjectSomeValuesFrom,
+  OWLDataSomeValuesFrom,
   OWLSubClassOfAxiom
 }
 import org.semanticweb.owlapi.model.parameters.Imports
@@ -48,7 +50,7 @@ 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.converter.{RDFoxConverter, SkolemStrategy}
 import uk.ac.ox.cs.rsacomb.suffix._
 import uk.ac.ox.cs.rsacomb.sparql._
 import uk.ac.ox.cs.rsacomb.util.{RDFoxUtil, RSA}
@@ -82,30 +84,28 @@ object RSAOntology {
 class RSAOntology(val ontology: OWLOntology) {
 
   import uk.ac.ox.cs.rsacomb.implicits.RSAAxiom._
+  import uk.ac.ox.cs.rsacomb.implicits.JavaCollections._
 
   // Gather TBox/RBox/ABox from original ontology
-  val tbox: List[OWLAxiom] =
+  val tbox: List[OWLLogicalAxiom] =
     ontology
       .tboxAxioms(Imports.INCLUDED)
       .collect(Collectors.toList())
-      .asScala
-      .toList
+      .collect { case a: OWLLogicalAxiom => a }
 
-  val rbox: List[OWLAxiom] =
+  val rbox: List[OWLLogicalAxiom] =
     ontology
       .rboxAxioms(Imports.INCLUDED)
       .collect(Collectors.toList())
-      .asScala
-      .toList
+      .collect { case a: OWLLogicalAxiom => a }
 
-  val abox: List[OWLAxiom] =
+  val abox: List[OWLLogicalAxiom] =
     ontology
       .aboxAxioms(Imports.INCLUDED)
       .collect(Collectors.toList())
-      .asScala
-      .toList
+      .collect { case a: OWLLogicalAxiom => a }
 
-  val axioms: List[OWLAxiom] = abox ::: tbox ::: rbox
+  val axioms: List[OWLLogicalAxiom] = abox ::: tbox ::: rbox
 
   /* Retrieve individuals in the original ontology
    */
@@ -152,28 +152,54 @@ class RSAOntology(val ontology: OWLOntology) {
     //println("\nUnsafe roles:")
     //println(unsafe)
 
+    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, SkolemStrategy.Constant(c))
+              if unsafe contains e.getProperty => {
+            val (res, ext) = super.convert(e, term, unsafe, skolem, suffix)
+            (RSA.PE(term, c) :: RSA.U(c) :: res, ext)
+          }
+
+          case (e: OWLDataSomeValuesFrom, SkolemStrategy.Constant(c))
+              if unsafe contains e.getProperty => {
+            val (res, ext) = super.convert(e, term, unsafe, skolem, suffix)
+            (RSA.PE(term, c) :: RSA.U(c) :: res, ext)
+          }
+
+          case _ => super.convert(expr, term, unsafe, skolem, suffix)
+        }
+
+    }
+
     /* 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
+    val term = RSAOntology.genFreshVariable()
+    val datalog = axioms
+      .map(a => {
+        val skolem = SkolemStrategy.Constant(a.toString)
+        RSAConverter.convert(a, term, unsafe, skolem, Empty)
+      })
+      .unzip
+    val facts = datalog._1.flatten
+    val rules = datalog._2.flatten
 
     /* DEBUG: print datalog rules */
-    println("\nDatalog roles:")
-    datalog.foreach(println)
+    //println("\nDatalog rules:")
+    //rules.foreach(println)
 
     // Open connection with RDFox
     val (server, data) = RDFoxUtil.openConnection("RSACheck")
-    // Add Data (hardcoded for now)
-    //data.importData(UpdateType.ADDITION, RSA.Prefixes, ":a a :A .")
 
     /* Add built-in rules
+     * TODO: substitute with RDFoxUtil.addRules
      */
     data.importData(
       UpdateType.ADDITION,
@@ -181,20 +207,11 @@ class RSAOntology(val ontology: OWLOntology) {
       "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)
+    /* Add ontology facts and rules */
+    RDFoxUtil.addFacts(data, facts)
+    RDFoxUtil.addRules(data, rules)
 
-    /* Build graph
-     */
+    /* Build graph */
     val graph = this.rsaGraph(data);
     //println(graph)
 
@@ -267,8 +284,8 @@ class RSAOntology(val ontology: OWLOntology) {
   ): Graph[Resource, UnDiEdge] = {
     val query = "SELECT ?X ?Y WHERE { ?X rsa:E ?Y }"
     val answers = RDFoxUtil.submitQuery(data, query, RSA.Prefixes).get
-    var edges: Seq[UnDiEdge[Resource]] = answers.map {
-      case Seq(n1, n2) => UnDiEdge(n1, n2)
+    var edges: Seq[UnDiEdge[Resource]] = answers.map { case Seq(n1, n2) =>
+      UnDiEdge(n1, n2)
     }
     Graph(edges: _*)
   }
@@ -310,8 +327,11 @@ class RSAOntology(val ontology: OWLOntology) {
   def ask(query: ConjunctiveQuery): ConjunctiveQueryAnswers = {
     import implicits.JavaCollections._
     val (server, data) = RDFoxUtil.openConnection(RSAOntology.DataStore)
-    data.addRules(this.canonicalModel.rules)
-    data.addRules(this.filteringProgram(query).rules)
+    val filter = this.filteringProgram(query)
+    RDFoxUtil.addRules(data, this.canonicalModel.rules)
+    RDFoxUtil.addFacts(data, this.canonicalModel.facts)
+    RDFoxUtil.addRules(data, filter.rules)
+    RDFoxUtil.addFacts(data, filter.facts)
     val answers = RDFoxUtil
       .submitQuery(
         data,
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
new file mode 100644
index 0000000..7fd4dbe
--- /dev/null
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxConverter.scala
@@ -0,0 +1,479 @@
+package uk.ac.ox.cs.rsacomb.converter
+
+import java.util.stream.Collectors
+import org.semanticweb.owlapi.model.{
+  OWLAnnotationProperty,
+  OWLLogicalAxiom,
+  OWLClass,
+  OWLClassAssertionAxiom,
+  OWLClassExpression,
+  OWLDataProperty,
+  OWLDataPropertyDomainAxiom,
+  OWLDataPropertyExpression,
+  OWLDataSomeValuesFrom,
+  OWLEquivalentClassesAxiom,
+  OWLEquivalentObjectPropertiesAxiom,
+  OWLInverseObjectPropertiesAxiom,
+  OWLNamedIndividual,
+  OWLObjectIntersectionOf,
+  OWLObjectInverseOf,
+  OWLObjectMaxCardinality,
+  OWLObjectOneOf,
+  OWLObjectProperty,
+  OWLObjectPropertyAssertionAxiom,
+  OWLObjectPropertyDomainAxiom,
+  OWLObjectPropertyExpression,
+  OWLObjectPropertyRangeAxiom,
+  OWLObjectSomeValuesFrom,
+  OWLPropertyExpression,
+  OWLSubClassOfAxiom,
+  OWLSubObjectPropertyOfAxiom
+}
+import scala.collection.JavaConverters._
+import tech.oxfordsemantic.jrdfox.logic.datalog.{
+  BindAtom,
+  BodyFormula,
+  Rule,
+  TupleTableAtom
+}
+import tech.oxfordsemantic.jrdfox.logic.expression.{Term, IRI, FunctionCall}
+import uk.ac.ox.cs.rsacomb.RSAOntology
+import uk.ac.ox.cs.rsacomb.suffix.{RSASuffix, Inverse}
+import uk.ac.ox.cs.rsacomb.util.RSA
+
+/** Horn-ALCHOIQ to RDFox axiom converter.
+  *
+  * Provides the tools to translate Horn-ALCHOIQ axioms into logic rules
+  * using RDFox syntax.
+  *
+  * @note the input axioms are assumed to be normalized. Trying to
+  * convert non normalized axioms might result in undefined behavious.
+  * We use the normalization defined in the main paper.
+  *
+  * @see [[https://github.com/KRR-Oxford/RSA-combined-approach GitHub repository]]
+  * for more information on the theoretical aspects of the system.
+  *
+  * @todo this is not ideal and it would be more sensible to prepend a
+  * normalization procedure that will prevent errors or unexpected
+  * results.
+  */
+trait RDFoxConverter {
+
+  /** Simplify conversion between Java and Scala collections */
+  import uk.ac.ox.cs.rsacomb.implicits.JavaCollections._
+
+  /** Simplify conversion between similar concepts in OWLAPI and RDFox
+    * abstract syntax.
+    */
+  import uk.ac.ox.cs.rsacomb.implicits.RDFox._
+
+  /** Represents the result of the conversion of a
+    * [[org.semanticweb.owlapi.model.OWLClassExpression OWLClassExpression]].
+    *
+    * In general a class expression is translated into a list of
+    * [[tech.oxfordsemantic.jrdfox.logic.datalog.TupleTableAtom TupleTableAtoms]].
+    * In some cases a class appearing on the right of a GCI might
+    * generate additional atoms that will appear in the body of the
+    * resulting formula.
+    *
+    * @example
+    * In `A ⊑ ≤1R.B`, translated as
+    * ```
+    *   y = z <- A(x), R(x,y), B(y), R(x,z), B(z)
+    * ```
+    * the atom `≤1R.B` produces `y = z` to appear as head of the rule,
+    * along with a set of atoms for the body of the rule (namely
+    * `R(x,y), B(y), R(x,z), B(z)`).
+    */
+  protected type Shards = (List[TupleTableAtom], List[BodyFormula])
+
+  /** Represent the result of the conversion of
+    * [[org.semanticweb.owlapi.model.OWLLogicalAxiom OWLLogicalAxiom]].
+    *
+    * In general we have assertion returning (a collection of) atoms,
+    * while other axioms that generate rules.
+    */
+  protected type Result = (List[TupleTableAtom], List[Rule])
+  protected def Result(): Result = (List(), List())
+  protected def ResultF(atoms: List[TupleTableAtom]): Result = (atoms, List())
+  protected def ResultR(rules: List[Rule]): Result = (List(), rules)
+
+  /** Converts a
+    * [[org.semanticweb.owlapi.model.OWLLogicalAxiom OWLLogicalAxiom]]
+    * into a collection of
+    * [[tech.oxfordsemantic.jrdfox.logic.datalog.TupleTableAtom TupleTableAtoms]]
+    * and
+    * [[tech.oxfordsemantic.jrdfox.logic.datalog.Rule Rules]].
+    *
+    * @note not all possible axioms are handled correctly, and in
+    * general they are assumed to be normalised. Following is a list of
+    * all unhandled class expressions:
+    * - [[org.semanticweb.owlapi.model.OWLAsymmetricObjectPropertyAxiom OWLAsymmetricObjectPropertyAxiom]]
+    * - [[org.semanticweb.owlapi.model.OWLDataPropertyAssertionAxiom OWLDataPropertyAssertionAxiom]]
+    * - [[org.semanticweb.owlapi.model.OWLDataPropertyRangeAxiom OWLDataPropertyRangeAxiom]]
+    * - [[org.semanticweb.owlapi.model.OWLDatatypeDefinitionAxiom OWLDatatypeDefinitionAxiom]]
+    * - [[org.semanticweb.owlapi.model.OWLDifferentIndividualsAxiom OWLDifferentIndividualsAxiom]]
+    * - [[org.semanticweb.owlapi.model.OWLDisjointClassesAxiom OWLDisjointClassesAxiom]]
+    * - [[org.semanticweb.owlapi.model.OWLDisjointDataPropertiesAxiom OWLDisjointDataPropertiesAxiom]]
+    * - [[org.semanticweb.owlapi.model.OWLDisjointObjectPropertiesAxiom OWLDisjointObjectPropertiesAxiom]]
+    * - [[org.semanticweb.owlapi.model.OWLDisjointUnionAxiom OWLDisjointUnionAxiom]]
+    * - [[org.semanticweb.owlapi.model.OWLEquivalentDataPropertiesAxiom OWLEquivalentDataPropertiesAxiom]]
+    * - [[org.semanticweb.owlapi.model.OWLFunctionalDataPropertyAxiom OWLFunctionalDataPropertyAxiom]]
+    * - [[org.semanticweb.owlapi.model.OWLFunctionalObjectPropertyAxiom OWLFunctionalObjectPropertyAxiom]]
+    * - [[org.semanticweb.owlapi.model.OWLHasKeyAxiom OWLHasKeyAxiom]]
+    * - [[org.semanticweb.owlapi.model.OWLInverseFunctionalObjectPropertyAxiom OWLInverseFunctionalObjectPropertyAxiom]]
+    * - [[org.semanticweb.owlapi.model.OWLIrreflexiveObjectPropertyAxiom OWLIrreflexiveObjectPropertyAxiom]]
+    * - [[org.semanticweb.owlapi.model.OWLNegativeDataPropertyAssertionAxiom OWLNegativeDataPropertyAssertionAxiom]]
+    * - [[org.semanticweb.owlapi.model.OWLNegativeObjectPropertyAssertionAxiom OWLNegativeObjectPropertyAssertionAxiom]]
+    * - [[org.semanticweb.owlapi.model.OWLReflexiveObjectPropertyAxiom OWLReflexiveObjectPropertyAxiom]]
+    * - [[org.semanticweb.owlapi.model.OWLSameIndividualAxiom OWLSameIndividualAxiom]]
+    * - [[org.semanticweb.owlapi.model.OWLSubDataPropertyOfAxiom OWLSubDataPropertyOfAxiom]]
+    * - [[org.semanticweb.owlapi.model.OWLSubPropertyChainOfAxiom OWLSubPropertyChainOfAxiom]]
+    * - [[org.semanticweb.owlapi.model.OWLSymmetricObjectPropertyAxiom OWLSymmetricObjectPropertyAxiom]]
+    * - [[org.semanticweb.owlapi.model.OWLTransitiveObjectPropertyAxiom OWLTransitiveObjectPropertyAxiom]]
+    * - [[org.semanticweb.owlapi.model.SWRLRule SWRLRule]]
+    */
+  def convert(
+      axiom: OWLLogicalAxiom,
+      term: Term,
+      unsafe: List[OWLObjectPropertyExpression],
+      skolem: SkolemStrategy,
+      suffix: RSASuffix
+  ): Result =
+    axiom match {
+
+      case a: OWLSubClassOfAxiom => {
+        val (sub, _) =
+          convert(a.getSubClass, term, unsafe, SkolemStrategy.None, suffix)
+        val (sup, ext) =
+          convert(a.getSuperClass, term, unsafe, skolem, suffix)
+        val rule = Rule.create(sup, ext ::: sub)
+        ResultR(List(rule))
+      }
+
+      // cannot be left
+      // http://www.w3.org/TR/owl2-syntax/#Equivalent_Classes
+      case a: OWLEquivalentClassesAxiom => {
+        val (atoms, rules) = a.asPairwiseAxioms
+          .flatMap(_.asOWLSubClassOfAxioms)
+          .map(convert(_, term, unsafe, skolem, suffix))
+          .unzip
+        (atoms.flatten, rules.flatten)
+      }
+
+      case a: OWLEquivalentObjectPropertiesAxiom => {
+        val (atoms, rules) = a.asPairwiseAxioms
+          .flatMap(_.asSubObjectPropertyOfAxioms)
+          .map(convert(_, term, unsafe, skolem, suffix))
+          .unzip
+        (atoms.flatten, rules.flatten)
+      }
+
+      case a: OWLSubObjectPropertyOfAxiom => {
+        val term1 = RSAOntology.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: OWLObjectPropertyDomainAxiom =>
+        convert(a.asOWLSubClassOfAxiom, term, unsafe, skolem, suffix)
+
+      case a: OWLObjectPropertyRangeAxiom => {
+        val term1 = RSAOntology.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)))
+      }
+
+      case a: OWLDataPropertyDomainAxiom =>
+        convert(a.asOWLSubClassOfAxiom, term, unsafe, skolem, suffix)
+
+      case a: OWLInverseObjectPropertiesAxiom => {
+        val (atoms, rules) = a.asSubObjectPropertyOfAxioms
+          .map(convert(_, term, unsafe, skolem, suffix))
+          .unzip
+        (atoms.flatten, rules.flatten)
+      }
+
+      case a: OWLClassAssertionAxiom => {
+        val ind = a.getIndividual
+        ind match {
+          case i: OWLNamedIndividual => {
+            val cls = a.getClassExpression
+            val (res, _) =
+              convert(cls, i.getIRI, unsafe, SkolemStrategy.None, suffix)
+            ResultF(res)
+          }
+          case _ => Result()
+        }
+      }
+
+      case a: OWLObjectPropertyAssertionAxiom =>
+        if (!a.getSubject.isNamed || !a.getObject.isNamed)
+          Result()
+        else {
+          val subj = a.getSubject.asOWLNamedIndividual.getIRI
+          val obj = a.getObject.asOWLNamedIndividual.getIRI
+          val prop = convert(a.getProperty, subj, obj, suffix)
+          ResultF(List(prop))
+        }
+
+      /** Catch-all case for all unhandled axiom types. */
+      case a =>
+        throw new RuntimeException(
+          s"Axiom '$a' is not supported (yet?)"
+        )
+
+    }
+
+  /** Converts a class expression into a collection of atoms.
+    *
+    * @note not all possible class expressions are handled correctly.
+    * Following is a list of all unhandled class expressions:
+    * - [[org.semanticweb.owlapi.model.OWLDataAllValuesFrom OWLDataAllValuesFrom]]
+    * - [[org.semanticweb.owlapi.model.OWLDataExactCardinality OWLDataExactCardinality]]
+    * - [[org.semanticweb.owlapi.model.OWLDataMaxCardinality OWLDataMaxCardinality]]
+    * - [[org.semanticweb.owlapi.model.OWLDataMinCardinality OWLDataMinCardinality]]
+    * - [[org.semanticweb.owlapi.model.OWLDataHasValue OWLDataHasValue]]
+    * - [[org.semanticweb.owlapi.model.OWLObjectAllValuesFrom OWLObjectAllValuesFrom]]
+    * - [[org.semanticweb.owlapi.model.OWLObjectComplementOf OWLObjectComplementOf]]
+    * - [[org.semanticweb.owlapi.model.OWLObjectExactCardinality OWLObjectExactCardinality]]
+    * - [[org.semanticweb.owlapi.model.OWLObjectHasSelf OWLObjectHasSelf]]
+    * - [[org.semanticweb.owlapi.model.OWLObjectHasValue OWLObjectHasValue]]
+    * - [[org.semanticweb.owlapi.model.OWLObjectMinCardinality OWLObjectMinCardinality]]
+    * - [[org.semanticweb.owlapi.model.OWLObjectUnionOf OWLObjectUnionOf]]
+    *
+    * Moreover:
+    * - [[org.semanticweb.owlapi.model.OWLObjectMaxCardinality OWLObjectMaxCardinality]]
+    *   is accepted only when cardinality is set to 1;
+    * - [[org.semanticweb.owlapi.model.OWLObjectOneOf OWLObjectOneOf]]
+    *   is accepted only when its arity is 1.
+    */
+  def convert(
+      expr: OWLClassExpression,
+      term: Term,
+      unsafe: List[OWLObjectPropertyExpression],
+      skolem: SkolemStrategy,
+      suffix: RSASuffix
+  ): Shards =
+    expr match {
+
+      /** Simple class name.
+        *
+        * @see [[http://www.w3.org/TR/owl2-syntax/#Classes]]
+        */
+      case e: OWLClass => {
+        val iri: IRI = if (e.isTopEntity()) IRI.THING else e.getIRI
+        val atom = TupleTableAtom.rdf(term, IRI.RDF_TYPE, iri)
+        (List(atom), List())
+      }
+
+      /** Conjunction of class expressions.
+        *
+        * @see [[http://www.w3.org/TR/owl2-syntax/#Intersection_of_Class_Expressions]]
+        */
+      case e: OWLObjectIntersectionOf => {
+        val (res, ext) = e.asConjunctSet
+          .map(convert(_, term, unsafe, skolem, suffix))
+          .unzip
+        (res.flatten, ext.flatten)
+      }
+
+      /** Enumeration of individuals.
+        *
+        * @note we only admit enumerations of arity 1.
+        *
+        * @throws `RuntimeException` when dealing with an enumeration
+        * with arity != 1.
+        *
+        * @see [[http://www.w3.org/TR/owl2-syntax/#Enumeration_of_Individuals]]
+        */
+      case e: OWLObjectOneOf => {
+        val named = e.individuals
+          .collect(Collectors.toList())
+          .collect { case x: OWLNamedIndividual => x }
+        if (named.length != 1)
+          throw new RuntimeException(s"Class expression '$e' has arity != 1.")
+        val atom = TupleTableAtom.rdf(term, IRI.SAME_AS, named.head.getIRI)
+        (List(atom), List())
+      }
+
+      /** Existential class expression (for data properties).
+        *
+        * Parameter `skolem` is used to determine the skolemization
+        * technique (if any) to use for the translation.
+        *
+        * @see [[http://www.w3.org/TR/owl2-syntax/#Existential_Quantification]]
+        */
+      case e: OWLObjectSomeValuesFrom => {
+        val cls = e.getFiller()
+        val role = e.getProperty()
+        // TODO: simplify this:
+        // 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(), RSAOntology.genFreshVariable)
+          case SkolemStrategy.Constant(c) => (List(), List(), c)
+          case SkolemStrategy.ConstantRSA(c) => {
+            if (unsafe.contains(role))
+              (List(RSA.PE(term, c), RSA.U(c)), List(), c)
+            else
+              (List(), List(), c)
+          }
+          case SkolemStrategy.Standard(f) => {
+            val x = RSAOntology.genFreshVariable
+            (
+              List(),
+              List(BindAtom.create(FunctionCall.create("SKOLEM", f, term), x)),
+              x
+            )
+          }
+        }
+        val (res, ext) = convert(cls, term1, unsafe, skolem, suffix)
+        val prop = convert(role, term, term1, suffix)
+        (prop :: head ::: res, body ::: ext)
+      }
+
+      /** Existential class expression (for data properties).
+        *
+        * Parameter `skolem` is used to determine the skolemization
+        * technique (if any) to use for the translation.
+        *
+        * @todo the "filler" of this OWL expression is currently ignored.
+        * This, in general might not be how we want to handle
+        * [[org.semanticweb.owlapi.model.OWLDataRange OWLDataRanges]].
+        *
+        * @see [[http://www.w3.org/TR/owl2-syntax/#Existential_Quantification_2]]
+        */
+      case e: OWLDataSomeValuesFrom => {
+        val role = e.getProperty()
+        // TODO: simplify this:
+        // 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(), RSAOntology.genFreshVariable)
+          case SkolemStrategy.Constant(c) => (List(), List(), c)
+          case SkolemStrategy.ConstantRSA(c) => {
+            if (unsafe.contains(role))
+              (List(RSA.PE(term, c), RSA.U(c)), List(), c)
+            else
+              (List(), List(), c)
+          }
+          case SkolemStrategy.Standard(f) => {
+            val y = RSAOntology.genFreshVariable()
+            (
+              List(),
+              List(BindAtom.create(FunctionCall.create("SKOLEM", f, term), y)),
+              y
+            )
+          }
+        }
+        val prop = convert(role, term, term1, suffix)
+        (prop :: head, body)
+      }
+
+      /** Maximum cardinality restriction class
+        *
+        * @note we only admit classes with cardinality set to 1.
+        *
+        * @throws `RuntimeException` when dealing with a restriction
+        * with cardinality != 1.
+        *
+        * @see [[http://www.w3.org/TR/owl2-syntax/#Maximum_Cardinality_2]]
+        */
+      case e: OWLObjectMaxCardinality => {
+        if (e.getCardinality != 1)
+          throw new RuntimeException(
+            s"Class expression '$e' has cardinality restriction != 1."
+          )
+        val vars @ (y :: z :: _) =
+          Seq(RSAOntology.genFreshVariable(), RSAOntology.genFreshVariable())
+        val cls = e.getFiller
+        val role = e.getProperty
+        val (res, ext) = vars.map(convert(cls, _, unsafe, skolem, suffix)).unzip
+        val props = vars.map(convert(role, term, _, suffix))
+        val eq = TupleTableAtom.rdf(y, IRI.SAME_AS, z)
+        (List(eq), res.flatten ++ props)
+      }
+
+      /** Catch-all case for all unhandled class expressions. */
+      case e =>
+        throw new RuntimeException(
+          s"Class expression '$e' is not supported (yet?)"
+        )
+    }
+
+  /** Converts an object property expression into an atom. */
+  def convert(
+      expr: OWLObjectPropertyExpression,
+      term1: Term,
+      term2: Term,
+      suffix: RSASuffix
+  ): TupleTableAtom =
+    expr match {
+
+      /** Simple named role/object property.
+        *
+        * @see [[http://www.w3.org/TR/owl2-syntax/#Object_Properties Object Properties]]
+        */
+      case e: OWLObjectProperty => {
+        val role = IRI.create(e.getIRI.getIRIString :: suffix)
+        TupleTableAtom.rdf(term1, role, term2)
+      }
+
+      /** Inverse of a named role/property
+        *
+        * OWLAPI does not admit nesting of negation, and double
+        * negations are always simplified.
+        *
+        * @see [[https://www.w3.org/TR/owl2-syntax/#Inverse_Object_Properties Inverse Object Properties]]
+        */
+      case e: OWLObjectInverseOf =>
+        convert(e.getInverse, term1, term2, suffix + Inverse)
+
+      /** The infamous impossible case.
+        *
+        * @note all relevant cases are taken care of, and this branch
+        * throws a runtime exception to notify of the problem.
+        */
+      case e =>
+        throw new RuntimeException(
+          s"Unable to convert '$e' into a logic expression. This should be happening (TM)."
+        )
+    }
+
+  /** Converts a data property expression into an atom. */
+  def convert(
+      expr: OWLDataPropertyExpression,
+      term1: Term,
+      term2: Term,
+      suffix: RSASuffix
+  ): TupleTableAtom =
+    expr match {
+
+      /** Simple named role/data property
+        *
+        * @see [[https://www.w3.org/TR/owl2-syntax/#Datatypes Data Properties]]
+        */
+      case e: OWLDataProperty => {
+        val role = IRI.create(e.getIRI.getIRIString :: suffix)
+        TupleTableAtom.rdf(term1, role, term2)
+      }
+
+      /** The infamous impossible case.
+        *
+        * @note all relevant cases are taken care of, and this branch
+        * throws a runtime exception to notify of the problem.
+        */
+      case e =>
+        throw new RuntimeException(
+          s"Unable to convert '$e' into a logic expression. This should be happening (TM)."
+        )
+    }
+
+}
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
index 4565017..8c513fd 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/implicits/JavaCollections.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/implicits/JavaCollections.scala
@@ -17,4 +17,8 @@ object JavaCollections {
       set: java.util.Collection[A]
   ): List[A] =
     set.asScala.toList
+
+  implicit def scalaSeqTojavaCollection[A](
+      seq: Seq[A]
+  ): java.util.Collection[A] = seq.asJavaCollection
 }
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/util/RDFoxUtil.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/util/RDFoxUtil.scala
index f7abde3..193119f 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/util/RDFoxUtil.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/util/RDFoxUtil.scala
@@ -5,7 +5,8 @@ import tech.oxfordsemantic.jrdfox.Prefixes
 import tech.oxfordsemantic.jrdfox.client.{
   ConnectionFactory,
   ServerConnection,
-  DataStoreConnection
+  DataStoreConnection,
+  UpdateType
 }
 import tech.oxfordsemantic.jrdfox.formats.SPARQLParser
 import tech.oxfordsemantic.jrdfox.logic.datalog.{
@@ -47,9 +48,8 @@ object RDFoxUtil {
     * @return a tuple with the newly opened server and data store
     * connections.
     *
-    * @see [[uk.ac.ox.cs.rsacomb.util.RDFoxUtil.closeConnection
-    * RDFoxUtil.closeConnection]] for
-    * details on how to close an open connection.
+    * @see [[uk.ac.ox.cs.rsacomb.util.RDFoxUtil.closeConnection RDFoxUtil.closeConnection]]
+    * for details on how to close an open connection.
     */
   def openConnection(
       datastore: String,
@@ -66,6 +66,26 @@ object RDFoxUtil {
     (server, data)
   }
 
+  /** Adds a collection of rules to a data store.
+    *
+    * @param data datastore connection
+    * @param rules collection of rules to be added to the data store
+    */
+  def addRules(data: DataStoreConnection, rules: Seq[Rule]): Unit =
+    data addRules rules
+
+  /** Adds a collection of facts to a data store.
+    *
+    * @param data datastore connection
+    * @param facts collection of facts to be added to the data store
+    */
+  def addFacts(data: DataStoreConnection, facts: Seq[TupleTableAtom]): Unit =
+    data.importData(
+      UpdateType.ADDITION,
+      RSA.Prefixes,
+      facts.map(_.toString(Prefixes.s_emptyPrefixes)).mkString("", ".\n", ".")
+    )
+
   /** Parse a SELECT query from a string in SPARQL format.
     *
     * @param query the string containing the SPARQL query