10 files changed, 967 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..2f7896d
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+target/
diff --git a/build.sbt b/build.sbt
new file mode 100644
index 0000000..e3df19c
--- /dev/null
+++ b/build.sbt
@@ -0,0 +1,15 @@
+import Dependencies._
+
+ThisBuild / scalaVersion     := "2.13.1"
+ThisBuild / version          := "0.1.0"
+//ThisBuild / organization     := "com.example"
+//ThisBuild / organizationName := "example"
+
+lazy val root = (project in file("."))
+  .settings(
+    name := "RSAComb",
+    libraryDependencies ++= Seq(
+        scalaTest % Test,
+        "net.sourceforge.owlapi" % "owlapi-apibinding" % "5.1.13"
+    )
+  )
diff --git a/src/main/scala/example/RDFoxAxiomConverter.scala b/src/main/scala/example/RDFoxAxiomConverter.scala
new file mode 100644
index 0000000..0a6272f
--- /dev/null
+++ b/src/main/scala/example/RDFoxAxiomConverter.scala
@@ -0,0 +1,58 @@
+package rsacomb
+
+import org.semanticweb.owlapi.model.{OWLAxiom, OWLSubClassOfAxiom, OWLEquivalentClassesAxiom}
+import org.semanticweb.owlapi.model.OWLAxiomVisitorEx
+
+import tech.oxfordsemantic.jrdfox.logic.Rule
+import tech.oxfordsemantic.jrdfox.logic.{Atom, Term, Literal, Individual}
+
+import scala.collection.JavaConverters._
+
+import rsacomb.SkolemStrategy
+import rsacomb.RDFoxRuleShards
+
+object RDFoxAxiomConverter {
+
+  def apply(term : Term, skolem : SkolemStrategy) : RDFoxAxiomConverter =
+        new RDFoxAxiomConverter(term, skolem)
+
+  def apply(term : Term) : RDFoxAxiomConverter =
+        new RDFoxAxiomConverter(term, SkolemStrategy.None)
+
+} // object RDFoxAxiomConverter
+
+class RDFoxAxiomConverter(term : Term, skolem : SkolemStrategy)
+  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,SkolemStrategy.None)
+    val superVisitor = new RDFoxClassExprConverter(term, skolem)
+    // 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
+  }
+
+  def doDefault(axiom : OWLAxiom) : List[Rule] = List()
+
+} // class RDFoxAxiomConverter
diff --git a/src/main/scala/example/RDFoxClassExprConverter.scala b/src/main/scala/example/RDFoxClassExprConverter.scala
new file mode 100644
index 0000000..3e60461
--- /dev/null
+++ b/src/main/scala/example/RDFoxClassExprConverter.scala
@@ -0,0 +1,119 @@
+package rsacomb
+
+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.{AtomicFormula, Bind,BuiltinFunctionCall}
+import tech.oxfordsemantic.jrdfox.logic.{Atom, Predicate, Term, Variable, Literal, Individual}
+
+import rsacomb.SkolemStrategy
+import rsacomb.RDFoxRuleShards
+
+object RDFoxClassExprConverter {
+
+  def apply(term : Term, skolem : SkolemStrategy) : RDFoxClassExprConverter =
+        new RDFoxClassExprConverter(term, skolem)
+
+  def apply(term : Term) : RDFoxClassExprConverter =
+        new RDFoxClassExprConverter(term, SkolemStrategy.None)
+
+  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, skolem : SkolemStrategy)
+  extends OWLClassExpressionVisitorEx[RDFoxRuleShards]
+{
+
+  // OWLClass
+  override
+  def visit(expr : OWLClass) : RDFoxRuleShards = {
+    val name = expr.getIRI.getIRIString
+    val atom = List(Atom.create(Predicate.create(name), term))
+    RDFoxRuleShards(atom,List())
+  }
+
+  // OWLObjectIntersectionOf
+  override
+  def visit(expr : OWLObjectIntersectionOf) : RDFoxRuleShards = {
+    val visitor = new RDFoxClassExprConverter(term,skolem)
+    // 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,skolem)
+    // 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.getIRIString
+    val atom = List(Atom.create(
+      Predicate.create("owl:sameAs"), term, Individual.create(ind)
+    ))
+    RDFoxRuleShards(atom,List())
+  }
+
+  // OWLObjectSomeValuesFrom
+  override
+  def visit(expr : OWLObjectSomeValuesFrom) : RDFoxRuleShards = {
+    // TODO: variables needs to be handled at visitor level. Hardcoding
+    // the name of the varibles might lead to errors for complex cases.
+    val y = Variable.create("y")
+        val (fun,term1) = skolem match {
+      case SkolemStrategy.None => (List(),y)
+      case SkolemStrategy.Constant(c) => (List(), Individual.create(c))
+      case SkolemStrategy.Standard(f) => 
+        // At the time of writing the RDFox library does not have a
+        // particular class for the "SKOLEM" operator and it is instead
+        // a simple builtin function with a special name.
+        (List(Bind.create(BuiltinFunctionCall.create("SKOLEM",term),y)),y)
+        }
+    val classVisitor = new RDFoxClassExprConverter(term1,skolem)
+    val classResult = expr.getFiller.accept(classVisitor)
+    val propertyVisitor = new RDFoxPropertyExprConverter(term, term1, skolem)
+    val propertyResult = expr.getProperty.accept(propertyVisitor)
+    RDFoxRuleShards(
+      classResult.res ++ propertyResult,
+      fun ++ classResult.ext
+    )
+  }
+
+  // OWLObjectMaxCardinality
+  override
+  def visit(expr : OWLObjectMaxCardinality) : RDFoxRuleShards = {
+    // TODO: again, no hardcoded variables
+    val vars = List(Variable.create("y"),Variable.create("z"))
+    val classResult = RDFoxClassExprConverter.merge(
+      vars.map(new RDFoxClassExprConverter(_,skolem))
+          .map(expr.getFiller.accept(_))
+    )
+    val propertyResult = 
+      vars.map(new RDFoxPropertyExprConverter(term,_,skolem))
+          .map(expr.getProperty.accept(_))
+          .flatten
+    RDFoxRuleShards(
+      List(Atom.create(Predicate.create("owl:sameAs"),vars(0),vars(1))),
+      classResult.res ++ propertyResult
+    )
+  }
+        
+  def doDefault(expr : OWLClassExpression) : RDFoxRuleShards =
+    RDFoxRuleShards(List(),List())
+
+} // class RDFoxClassExprConverter
diff --git a/src/main/scala/example/RDFoxPropertyExprConverter.scala b/src/main/scala/example/RDFoxPropertyExprConverter.scala
new file mode 100644
index 0000000..2885ed9
--- /dev/null
+++ b/src/main/scala/example/RDFoxPropertyExprConverter.scala
@@ -0,0 +1,23 @@
+package rsacomb
+
+import org.semanticweb.owlapi.model.{OWLPropertyExpression, OWLObjectProperty}
+import org.semanticweb.owlapi.model.OWLPropertyExpressionVisitorEx
+
+import tech.oxfordsemantic.jrdfox.logic.{Atom, Predicate, Term, Variable, Literal}
+
+import rsacomb.SkolemStrategy
+
+class RDFoxPropertyExprConverter(term1 : Term, term2 : Term, skolem : SkolemStrategy)
+  extends OWLPropertyExpressionVisitorEx[List[Atom]]
+{
+
+  override
+  def visit(expr : OWLObjectProperty) : List[Atom] = {
+    val name = expr.getIRI.getIRIString
+    List(Atom.create(Predicate.create(name), term1, term2))
+  }
+
+  def doDefault(expr : OWLPropertyExpression) : List[Atom] = List()
+
+} // class RDFoxPropertyExprConverter
+
diff --git a/src/main/scala/example/RDFoxRuleShards.scala b/src/main/scala/example/RDFoxRuleShards.scala
new file mode 100644
index 0000000..bce31d2
--- /dev/null
+++ b/src/main/scala/example/RDFoxRuleShards.scala
@@ -0,0 +1,6 @@
+package rsacomb
+
+import tech.oxfordsemantic.jrdfox.logic.{Rule, Atom, Literal}
+
+case class RDFoxRuleShards(res : List[Atom], ext : List[Literal])
+
diff --git a/src/main/scala/example/RSAComb.scala b/src/main/scala/example/RSAComb.scala
new file mode 100644
index 0000000..bc94a8d
--- /dev/null
+++ b/src/main/scala/example/RSAComb.scala
@@ -0,0 +1,138 @@
+package rsacomb
+
+import java.io.File
+import java.util.HashMap
+import java.util.stream.{Stream,Collectors}
+
+import org.semanticweb.owlapi.apibinding.OWLManager
+import org.semanticweb.owlapi.model.{AxiomType, ClassExpressionType, OWLObjectSomeValuesFrom}
+import org.semanticweb.owlapi.model.{OWLAxiom, OWLSubClassOfAxiom, OWLEquivalentClassesAxiom}
+import org.semanticweb.owlapi.model.OWLClassExpression
+import org.semanticweb.owlapi.model.OWLOntology
+import org.semanticweb.owlapi.model.OWLOntologyManager
+import org.semanticweb.owlapi.model.parameters.Imports
+
+import tech.oxfordsemantic.jrdfox.Prefixes
+import tech.oxfordsemantic.jrdfox.client.{ConnectionFactory, ServerConnection, DataStoreConnection}
+import tech.oxfordsemantic.jrdfox.client.UpdateType
+import tech.oxfordsemantic.jrdfox.logic.{Rule, Atom, Literal, Predicate, Term, Variable}
+import tech.oxfordsemantic.jrdfox.logic.{Bind, BuiltinFunctionCall}
+
+import scala.collection.JavaConverters._
+
+import rsacomb.SkolemStrategy
+
+class RSA(ontology : OWLOntology) {
+
+  /* Alternative constructor(s) */
+  def this(file : File) = this(RSA.loadOntology(file))
+
+  def getOntology : OWLOntology = ontology
+
+} // class RSA
+
+object RSA {
+
+  def loadOntology( onto : File ) : OWLOntology = {
+    /* Retrieve ontology manager */
+    val manager : OWLOntologyManager = OWLManager.createOWLOntologyManager()
+    /* Retrieve ontology */
+    manager.loadOntologyFromOntologyDocument(onto)
+  }
+
+  def isRSA( onto : OWLOntology ) : Boolean = {
+    /* TODO: 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
+     */
+
+    /* Ontology axiom convertion into LP rules */
+        for {
+      axiom <- onto.tboxAxioms(Imports.EXCLUDED).collect(Collectors.toList()).asScala
+      visitor = new RDFoxAxiomConverter(Variable.create("x"), SkolemStrategy.Constant(axiom.toString))
+      rule  <- axiom.accept(visitor)
+        } yield println(rule)
+
+    /* Return true for now... */
+    true
+  }
+
+} // object RSA
+
+object RSAComb {
+
+  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.
+  """
+
+  def main( args : Array[String] ) : Unit = {
+
+    /* Simple arguments handling
+     *
+     * TODO: use something better later on
+     */
+
+    if (args.length < 2) {
+      println(help)
+      return ()
+    }
+
+    val ontologyPath = new File(args(0))
+    val queryPath = new File(args(1))
+
+    if (!ontologyPath.isFile || !queryPath.isFile) {
+      println("The provided arguments are not regular files.\n\n")
+      println(help)
+      return ()
+    }
+
+    /* 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 rsa = new RSA(ontologyPath)
+    RSA.isRSA(rsa.getOntology)
+
+    /* Build canonical model */
+    //val tboxCanon = rsa.canonicalModel()
+
+    /* Load query */
+    //val query = ...
+
+    /* Compute the filtering program from the given query */
+    //val tboxFilter = rsa.filteringProgram(query)
+
+    /* ... */
+
+    /* DEBUG ONLY */
+    println("Ok!")
+  }
+}
+
+/* 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/example/SkolemStrategy.scala b/src/main/scala/example/SkolemStrategy.scala
new file mode 100644
index 0000000..9df167f
--- /dev/null
+++ b/src/main/scala/example/SkolemStrategy.scala
@@ -0,0 +1,46 @@
+package rsacomb
+
+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(y) -> R(x,f(x)), B(f(x))
+   * for f, fresh function associated with the input axiom
+   */
+  case class Standard(func : String) extends SkolemStrategy
+  object Standard {
+    def apply(axiom : String) = new Standard(genFunctionString(axiom))
+    def genFunctionString(str : String) = "f_" ++ str.hashCode.toString
+  }
+
+  /* Functional 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 : String) extends SkolemStrategy
+  object Constant {
+    def apply(axiom : String) = new Constant(genConstantString(axiom))
+    def genConstantString(str : String) = "internal:c_" ++ str.hashCode.toString
+  }
+}
+
diff --git a/src/test/scala/buzz/OWLAxiomSpec.scala b/src/test/scala/buzz/OWLAxiomSpec.scala
new file mode 100644
index 0000000..b6a44f4
--- /dev/null
+++ b/src/test/scala/buzz/OWLAxiomSpec.scala
@@ -0,0 +1,302 @@
+package rsacomb
+
+import java.util.ArrayList
+import org.scalatest.{FlatSpec, Matchers, LoneElement}
+
+import uk.ac.manchester.cs.owl.owlapi.{OWLSubClassOfAxiomImpl}
+import uk.ac.manchester.cs.owl.owlapi.{OWLClassImpl, OWLObjectSomeValuesFromImpl, OWLObjectIntersectionOfImpl, OWLObjectOneOfImpl, OWLObjectAllValuesFromImpl, OWLObjectMaxCardinalityImpl, OWLNamedIndividualImpl}
+import uk.ac.manchester.cs.owl.owlapi.{OWLObjectPropertyImpl}
+import org.semanticweb.owlapi.model.{OWLAxiom,IRI}
+
+import tech.oxfordsemantic.jrdfox.logic.{Rule,Bind,BuiltinFunctionCall}
+import tech.oxfordsemantic.jrdfox.logic.{Atom, Predicate, Term, Variable, Individual}
+
+object OWLAxiomSpec {
+
+  // IRI
+  val iri_Professor = IRI.create("univ:Professor")
+  val iri_Female    = IRI.create("std:Female")
+  val iri_Student   = IRI.create("univ:Student")
+  val iri_PartTimeStudent = IRI.create("univ:PartTimeStudent")
+  val iri_Worker    = IRI.create("univ:Worker")
+  val iri_alice     = IRI.create("univ:alice")
+  val iri_supervises    = IRI.create("univ:supervises")
+  val iri_hasSupervisor = IRI.create("univ:hasSupervisor")
+  val iri_sameAs = IRI.create("owl:sameAs")
+
+  // RDFox Terms
+  val term_x = Variable.create("x")
+  val term_y = Variable.create("y")
+  val term_z = Variable.create("z")
+  val term_c1 = Individual.create("internal:c_1")
+  val term_c2 = Individual.create("internal:c_2")
+  val term_alice = Individual.create("univ:alice")
+
+  // RDFox Predicates
+  val pred_sameAs = Predicate.create("owl:sameAs")
+  val pred_Professor = Predicate.create(iri_Professor.getIRIString)
+  val pred_hasSupervisor = Predicate.create(iri_hasSupervisor.getIRIString)
+
+  // OWL Classes
+  // Name Class corresponding to
+  //
+  //    Professor
+  //
+  val class_Professor = new OWLClassImpl(iri_Professor)
+  val class_Female    = new OWLClassImpl(iri_Female)
+  val class_Student   = new OWLClassImpl(iri_Student)
+  val class_PartTimeStudent   = new OWLClassImpl(iri_PartTimeStudent)
+  val class_Worker    = new OWLClassImpl(iri_Worker)
+  val class_OWLClass = class_Professor
+  // Class Conjunction corresponding to
+  //
+  //    Student ∧ Worker
+  //
+  val class_OWLObjectIntersectionOf = 
+    new OWLObjectIntersectionOfImpl(
+      class_Student, class_Worker
+    )
+  // Singleton Class corresponding to
+  //
+  //    { alice }
+  //
+  val class_OWLObjectOneOf =
+    new OWLObjectOneOfImpl(
+      new OWLNamedIndividualImpl(iri_alice)
+    )
+  // Object Existential Restiction corresponding to
+  //
+  //    ∃ hasSupervisor.Professor
+  //
+  val class_OWLObjectSomeValuesFrom =
+    new OWLObjectSomeValuesFromImpl(
+      new OWLObjectPropertyImpl(iri_hasSupervisor),
+      class_Professor
+    )
+  // Object Max Cardinality Restriction corresponding to
+  //
+  //    ≤ 1 hasSupervisor . Professor
+  val class_OWLObjectMaxCardinality =
+    new OWLObjectMaxCardinalityImpl(
+      new OWLObjectPropertyImpl(iri_hasSupervisor),
+      1,
+      class_Professor
+    )
+
+  // OWL Axioms
+  // Axiom SubClassOf corresponding to
+  //
+  //    Student ∧ Worker -> PartTimeStudent
+  //
+  val axiom_OWLSubClassOf1 = 
+    new OWLSubClassOfAxiomImpl(
+      class_OWLObjectIntersectionOf,
+      class_PartTimeStudent,
+      new ArrayList()
+    )
+
+  // Axiom SubClassOf corresponding to
+  //
+  //    Student -> ∃ hasSupervisor.Professor
+  //
+  val axiom_OWLSubClassOf2 =
+    new OWLSubClassOfAxiomImpl(
+      class_Student,
+      class_OWLObjectSomeValuesFrom,
+      new ArrayList()
+    )
+
+  // Axiom SubClassOf corresponding to
+  //
+  //    ∃ hasSupervisor.Professor -> Student
+  //
+  val axiom_OWLSubClassOf3 =
+    new OWLSubClassOfAxiomImpl(
+      class_OWLObjectSomeValuesFrom,
+      class_Student,
+      new ArrayList()
+    )
+
+  // Axiom SubClassOf corresponding to
+  //
+  //    Student -> { alice }
+  //
+  val axiom_OWLSubClassOf4 =
+    new OWLSubClassOfAxiomImpl(
+      class_Student,
+      class_OWLObjectOneOf,
+      new ArrayList()
+    )
+
+  // Axiom SubClassOf corresponding to
+  //
+  //    Student -> ≤1 hasSupervisor.Professor
+  //
+  val axiom_OWLSubClassOf5 =
+    new OWLSubClassOfAxiomImpl(
+      class_Student,
+      class_OWLObjectMaxCardinality,
+      new ArrayList()
+    )
+
+  def convertAxiom(
+    axiom: OWLAxiom,
+    term: Term,
+    skolem: SkolemStrategy = SkolemStrategy.None
+  ) : List[Rule] = {
+    axiom.accept(RDFoxAxiomConverter(term,skolem))
+  }
+
+} // object OWLAxiomSpec
+
+class OWLAxiomSpec
+  extends FlatSpec with Matchers with LoneElement
+{
+  // Import required data
+  import OWLAxiomSpec._
+
+  // OWLSubClassOfAxiom #1
+  axiom_OWLSubClassOf1.toString should "be converted into a singleton List[Rule]" in {
+    val result = convertAxiom(axiom_OWLSubClassOf1,term_x)
+    result.loneElement shouldBe a [Rule]
+  }
+
+  it should "contain a conjuction of atoms (Student[?x],Worker[?x]) in the body of the rule" in {
+    val result = convertAxiom(axiom_OWLSubClassOf1,term_x)
+    val body = List(
+      Atom.create(Predicate.create(iri_Student.getIRIString),term_x),
+      Atom.create(Predicate.create(iri_Worker.getIRIString),term_x)
+    )
+    result.loneElement.getBody should contain theSameElementsAs body
+  }
+
+  it should "contain a single atom (PartTimeStudent[?x]) in the head of the rule" in {
+    val result = convertAxiom(axiom_OWLSubClassOf1,term_x)
+    val head = Atom.create(Predicate.create(iri_PartTimeStudent.getIRIString),term_x)
+    result.loneElement.getHead.loneElement should be (head)
+  }
+
+  // OWLSubClassOfAxiom #2 (w/ constant skolemization)
+  (axiom_OWLSubClassOf2.toString + "\n(w/ constant skolemization)") should
+    "be converted into a singleton List[Rule]" in
+  {
+    val skolem = SkolemStrategy.Constant(axiom_OWLSubClassOf2.toString)
+    val result = convertAxiom(axiom_OWLSubClassOf2,term_x,skolem)
+    result.loneElement shouldBe a [Rule]
+  }
+
+  it should "contain a single atom (Student[?x]) in the body of the rule" in {
+    val skolem = SkolemStrategy.Constant(axiom_OWLSubClassOf2.toString)
+    val result = convertAxiom(axiom_OWLSubClassOf2,term_x,skolem)
+    val body = Atom.create(Predicate.create(iri_Student.getIRIString),term_x)
+    result.loneElement.getBody.loneElement should equal (body)
+  }
+
+  it should "contain a conjuction of atoms (hasSupervisor[?x,?c],Professor[?c]) in the head of the rule" in {
+    val skolem = SkolemStrategy.Constant(axiom_OWLSubClassOf2.toString)
+    val result = convertAxiom(axiom_OWLSubClassOf2,term_x,skolem)
+    val term_c = Individual.create(skolem.const)
+    val head = List(
+      Atom.create(Predicate.create(iri_hasSupervisor.getIRIString),term_x,term_c),
+      Atom.create(Predicate.create(iri_Professor.getIRIString),term_c)
+    )
+    result.loneElement.getHead should contain theSameElementsAs (head)
+  }
+
+  // OWLSubClassOfAxiom #2 (w/ skolemization)
+  (axiom_OWLSubClassOf2.toString + "\n(w/ skolemization)") should
+    "be converted into a singleton List[Rule]" in
+  {
+    val skolem = SkolemStrategy.Standard(axiom_OWLSubClassOf2.toString)
+    val result = convertAxiom(axiom_OWLSubClassOf2, term_x, skolem)
+    result.loneElement shouldBe a [Rule]
+  }
+
+  it should "contain an atom (Student[?x]) in the body of the rule" in {
+    val skolem = SkolemStrategy.Standard(axiom_OWLSubClassOf2.toString)
+    val result = convertAxiom(axiom_OWLSubClassOf2, term_x, skolem)
+    val body = Atom.create(Predicate.create(iri_Student.getIRIString),term_x)
+    result.loneElement.getBody should contain (body)
+  }
+
+  it should "contain a built-in function call (BIND(?y,SKOLEM(?f,?x))) in the body of the rule" in {
+    val skolem = SkolemStrategy.Standard(axiom_OWLSubClassOf2.toString)
+    val result = convertAxiom(axiom_OWLSubClassOf2, term_x, skolem)
+    val call = Bind.create(BuiltinFunctionCall.create("SKOLEM",term_x),term_y)
+    result.loneElement.getBody should contain (call)
+  }
+
+  it should "contain a conjuction of atom (hasSupervisor[?x,?y],Professor[?y]) in the head of the rule" in {
+    val skolem = SkolemStrategy.Standard(axiom_OWLSubClassOf2.toString)
+    val result = convertAxiom(axiom_OWLSubClassOf2, term_x, skolem)
+    val head = List(
+      Atom.create(Predicate.create(iri_hasSupervisor.getIRIString),term_x,term_y),
+      Atom.create(Predicate.create(iri_Professor.getIRIString),term_y)
+    )
+    result.loneElement.getHead should contain theSameElementsAs head
+  }
+
+  // OWLSubClassOfAxiom #3
+  axiom_OWLSubClassOf3.toString should "be converted into a singleton List[Rule]" in {
+    val result = convertAxiom(axiom_OWLSubClassOf3,term_x)
+    result.loneElement shouldBe a [Rule]
+  }
+
+  it should "contain a conjunction of atoms (hasSupervisor[?x,?y],Professor[?y]) in the body of the rule" in {
+    val result = convertAxiom(axiom_OWLSubClassOf3,term_x)
+    val body = List(
+      Atom.create(Predicate.create(iri_hasSupervisor.getIRIString),term_x,term_y),
+      Atom.create(Predicate.create(iri_Professor.getIRIString),term_y)
+    )
+    result.loneElement.getBody should contain theSameElementsAs body
+  }
+
+  it should "contain a single atom (Student[?x]) in the head of the rule" in {
+    val result = convertAxiom(axiom_OWLSubClassOf3, term_x)
+    val head = Atom.create(Predicate.create(iri_Student.getIRIString),term_x)
+    result.loneElement.getHead.loneElement should be (head)
+  }
+
+  // OWLSubClassOfAxiom #4
+  axiom_OWLSubClassOf4.toString should "be converted into a singleton List[Rule]" in {
+    val result = convertAxiom(axiom_OWLSubClassOf4,term_x)
+    result.loneElement shouldBe a [Rule]
+  }
+
+  it should "contain a single atoms (Student[?x]) in the body of the rule" in {
+    val result = convertAxiom(axiom_OWLSubClassOf4,term_x)
+    val body = Atom.create(Predicate.create(iri_Student.getIRIString),term_x)
+    result.loneElement.getBody.loneElement should be (body)
+  }
+
+  it should "contain a single atom (sameAs[?x,alice])) in the head of the rule" in {
+    val result = convertAxiom(axiom_OWLSubClassOf4, term_x)
+    val head = Atom.create(Predicate.create(iri_sameAs.getIRIString),term_x,term_alice)
+    result.loneElement.getHead.loneElement should be (head)
+  }
+
+  // OWLSubClassOfAxiom #5
+  axiom_OWLSubClassOf5.toString should "be converted into a singleton List[Rule]" in {
+    val result = convertAxiom(axiom_OWLSubClassOf5,term_x)
+    result.loneElement shouldBe a [Rule]
+  }
+
+  it should "contain a conjunction of atoms (...) in the body of the rule" in {
+    val result = convertAxiom(axiom_OWLSubClassOf5,term_x)
+    val body = List(
+      Atom.create(Predicate.create(iri_Student.getIRIString),term_x),
+      Atom.create(Predicate.create(iri_hasSupervisor.getIRIString),term_x,term_y),
+      Atom.create(Predicate.create(iri_Professor.getIRIString),term_y),
+      Atom.create(Predicate.create(iri_hasSupervisor.getIRIString),term_x,term_z),
+      Atom.create(Predicate.create(iri_Professor.getIRIString),term_z)
+    )
+    result.loneElement.getBody should contain theSameElementsAs body
+  }
+
+  it should "contain a single atom (sameAs[?x,?z])) in the head of the rule" in {
+    val result = convertAxiom(axiom_OWLSubClassOf5, term_x)
+    val head = Atom.create(Predicate.create(iri_sameAs.getIRIString),term_y,term_z)
+    result.loneElement.getHead.loneElement should be (head)
+  }
+
+} // class OWLAxiomSpec
diff --git a/src/test/scala/buzz/OWLClassSpec.scala b/src/test/scala/buzz/OWLClassSpec.scala
new file mode 100644
index 0000000..df10e19
--- /dev/null
+++ b/src/test/scala/buzz/OWLClassSpec.scala
@@ -0,0 +1,259 @@
+package rsacomb
+
+import org.scalatest.{FlatSpec, Matchers, LoneElement}
+
+import uk.ac.manchester.cs.owl.owlapi.{OWLClassImpl, OWLObjectSomeValuesFromImpl, OWLObjectIntersectionOfImpl, OWLObjectOneOfImpl, OWLObjectAllValuesFromImpl, OWLObjectMaxCardinalityImpl, OWLNamedIndividualImpl}
+import uk.ac.manchester.cs.owl.owlapi.{OWLObjectPropertyImpl}
+import org.semanticweb.owlapi.model.IRI
+
+import tech.oxfordsemantic.jrdfox.logic.{Bind,BuiltinFunctionCall}
+import tech.oxfordsemantic.jrdfox.logic.{Atom, Predicate, Term, Variable, Individual}
+
+import rsacomb.RDFoxRuleShards
+
+object OWLClassSpec {
+
+  // IRI
+  val iri_Professor = IRI.create("univ:Professor")
+  val iri_Female    = IRI.create("std:Female")
+  val iri_Student   = IRI.create("univ:Student")
+  val iri_Worker    = IRI.create("univ:Worker")
+  val iri_alice     = IRI.create("univ:alice")
+  val iri_supervises    = IRI.create("univ:supervises")
+  val iri_hasSupervisor = IRI.create("univ:hasSupervisor")
+
+  // RDFox Terms
+  val term_x = Variable.create("x")
+  val term_y = Variable.create("y")
+  val term_c1 = Individual.create("internal:c_1")
+  val term_c2 = Individual.create("internal:c_2")
+  val term_alice = Individual.create("univ:alice")
+
+  // RDFox Predicates
+  val pred_sameAs = Predicate.create("owl:sameAs")
+  val pred_Professor = Predicate.create(iri_Professor.getIRIString)
+  val pred_hasSupervisor = Predicate.create(iri_hasSupervisor.getIRIString)
+
+  // OWL Classes
+  // Name Class corresponding to
+  //
+  //    Professor
+  //
+  val class_Professor = new OWLClassImpl(iri_Professor)
+  val class_Female    = new OWLClassImpl(iri_Female)
+  val class_Student   = new OWLClassImpl(iri_Student)
+  val class_Worker    = new OWLClassImpl(iri_Worker)
+  val class_OWLClass = class_Professor
+
+  // Class Conjunction corresponding to
+  //
+  //    Female ∧ Student ∧ Worker
+  //
+  val class_OWLObjectIntersectionOf = 
+    new OWLObjectIntersectionOfImpl(
+      class_Female, class_Student, class_Worker
+    )
+  // Singleton Class corresponding to
+  //
+  //    { alice }
+  //
+  val class_OWLObjectOneOf =
+    new OWLObjectOneOfImpl(
+      new OWLNamedIndividualImpl(iri_alice)
+    )
+  // Object Existential Restiction corresponding to
+  //
+  //   ∃ hasSupervisor.Professor
+  //
+  val class_OWLObjectSomeValuesFrom =
+    new OWLObjectSomeValuesFromImpl(
+      new OWLObjectPropertyImpl(iri_hasSupervisor),
+      class_Professor
+    )
+  // Object Max Cardinality Restriction corresponding to
+  //
+  //    ≤1 hasSupervisor.Professor
+  val class_OWLObjectMaxCardinality =
+    new OWLObjectMaxCardinalityImpl(
+      new OWLObjectPropertyImpl(iri_hasSupervisor),
+      1,
+      class_Professor
+    )
+} // object OWLClassSpec
+
+class OWLClassSpec
+  extends FlatSpec with Matchers with LoneElement
+{
+  // Import required data
+  import OWLClassSpec._
+
+  // OWLClass
+  class_OWLClass.toString should "be converted into a RDFoxRuleShards" in {
+    val visitor = RDFoxClassExprConverter(term_x)
+    val result = class_OWLClass.accept(visitor)
+    result shouldBe a [RDFoxRuleShards]
+  }
+
+  it should "have a single Atom in its result list" in {
+    val visitor = RDFoxClassExprConverter(term_x)
+    val result = class_OWLClass.accept(visitor)
+    result.res.loneElement shouldBe an [Atom]
+  }
+
+  it should "have an empty extension list" in {
+    val visitor = RDFoxClassExprConverter(term_x)
+    val result = class_OWLClass.accept(visitor)
+    result.ext shouldBe empty
+  }
+
+  // OWLObjectIntersectionOf
+  class_OWLObjectIntersectionOf.toString should "be converted into a RDFoxRuleShards" in {
+    val visitor = RDFoxClassExprConverter(term_x)
+    val result = class_OWLObjectIntersectionOf.accept(visitor)
+    result shouldBe a [RDFoxRuleShards]
+  }
+
+  it should "be converted in the union of its converted conjuncts" in {
+    val visitor = RDFoxClassExprConverter(term_x)
+    val result1= class_OWLObjectIntersectionOf.accept(visitor)
+    val result2 = RDFoxClassExprConverter.merge(List(
+      class_Female.accept(visitor),
+      class_Student.accept(visitor),
+      class_Worker.accept(visitor)
+    ))
+    result1.res should contain theSameElementsAs result2.res
+    result1.ext should contain theSameElementsAs result2.ext
+  }
+
+  // OWLObjectOneOf
+  class_OWLObjectOneOf.toString should "be converted into a RDFoxRuleShards" in {
+    val visitor = RDFoxClassExprConverter(term_x)
+    val result = class_OWLObjectOneOf.accept(visitor)
+    result shouldBe a [RDFoxRuleShards]
+  }
+
+  it should "be converted into a single <owl:sameAs> Atom" in {
+    val visitor = RDFoxClassExprConverter(term_x)
+    val result = class_OWLObjectOneOf.accept(visitor)
+    result.res.loneElement should (be (a [Atom]) and have ('predicate (pred_sameAs)))
+  }
+
+  it should "have an empty extension list" in {
+    val visitor = RDFoxClassExprConverter(term_x)
+    val result = class_OWLObjectOneOf.accept(visitor)
+    result.ext shouldBe empty
+  }
+
+  // OWLObjectSomeValuesFrom
+  (class_OWLObjectSomeValuesFrom.toString ++ " w/o skolemization") should
+    "be converted into a RDFoxRuleShards" in {
+      val visitor = RDFoxClassExprConverter(term_x,SkolemStrategy.None)
+      val result = class_OWLObjectSomeValuesFrom.accept(visitor)
+      result shouldBe a [RDFoxRuleShards]
+  }
+
+  it should "have exactly one unary Atom in its result list" in {
+    val visitor = RDFoxClassExprConverter(term_x,SkolemStrategy.None)
+    val result = class_OWLObjectSomeValuesFrom.accept(visitor)
+    exactly (1, result.res) should (be (an [Atom]) and have ('numberOfArguments (1)))
+  }
+
+  it should "have exactly one binary Atom in its result list" in {
+    val visitor = RDFoxClassExprConverter(term_x,SkolemStrategy.None)
+    val result = class_OWLObjectSomeValuesFrom.accept(visitor)
+    exactly (1, result.res) should (be (an [Atom]) and have ('numberOfArguments (2)))
+  }
+
+  it should "have an empty extension list" in {
+    val visitor = RDFoxClassExprConverter(term_x,SkolemStrategy.None)
+    val result = class_OWLObjectSomeValuesFrom.accept(visitor)
+    result.ext shouldBe empty
+  }
+
+  (class_OWLObjectSomeValuesFrom.toString ++ " w/ skolemization") should
+    "be converted into a RDFoxRuleShards" in {
+      val skolem = SkolemStrategy.Standard(class_OWLObjectSomeValuesFrom.toString)
+      val visitor = RDFoxClassExprConverter(term_x,skolem)
+      val result = class_OWLObjectSomeValuesFrom.accept(visitor)
+      result shouldBe a [RDFoxRuleShards]
+  }
+
+  it should "have exactly one unary Atom in its result list" in {
+    val skolem = SkolemStrategy.Standard(class_OWLObjectSomeValuesFrom.toString)
+    val visitor = RDFoxClassExprConverter(term_x,skolem)
+    val result = class_OWLObjectSomeValuesFrom.accept(visitor)
+    exactly (1, result.res) should (be (an [Atom]) and have ('numberOfArguments (1)))
+  }
+
+  it should "have exactly one binary Atom in its result list" in {
+    val skolem = SkolemStrategy.Standard(class_OWLObjectSomeValuesFrom.toString)
+    val visitor = RDFoxClassExprConverter(term_x,skolem)
+    val result = class_OWLObjectSomeValuesFrom.accept(visitor)
+    exactly (1, result.res) should (be (an [Atom]) and have ('numberOfArguments (2)))
+  }
+
+  it should "should have a single SKOLEM call in the extension list" in {
+    val skolem = SkolemStrategy.Standard(class_OWLObjectSomeValuesFrom.toString)
+    val visitor = RDFoxClassExprConverter(term_x,skolem)
+    val result = class_OWLObjectSomeValuesFrom.accept(visitor)
+    result.ext.loneElement shouldBe a [Bind]
+    val builtin = result.ext.head.asInstanceOf[Bind].getBuiltinExpression
+    builtin should (be (a [BuiltinFunctionCall]) and have ('functionName ("SKOLEM")))
+  }
+
+  (class_OWLObjectSomeValuesFrom.toString ++ " w/ constant skolemization") should
+    "be converted into a RDFoxRuleShards" in {
+      val skolem = SkolemStrategy.Constant(class_OWLObjectSomeValuesFrom.toString)
+      val visitor = RDFoxClassExprConverter(term_x,skolem)
+      val result = class_OWLObjectSomeValuesFrom.accept(visitor)
+      result shouldBe a [RDFoxRuleShards]
+  }
+
+  it should "have exactly one unary Atom in its result list" in {
+    val skolem = SkolemStrategy.Constant(class_OWLObjectSomeValuesFrom.toString)
+    val visitor = RDFoxClassExprConverter(term_x,skolem)
+    val result = class_OWLObjectSomeValuesFrom.accept(visitor)
+    exactly (1, result.res) should (be (an [Atom]) and have ('numberOfArguments (1)))
+  }
+
+  it should "have exactly one binary Atom in its result list" in {
+    val skolem = SkolemStrategy.Constant(class_OWLObjectSomeValuesFrom.toString)
+    val visitor = RDFoxClassExprConverter(term_x,skolem)
+    val result = class_OWLObjectSomeValuesFrom.accept(visitor)
+    exactly (1, result.res) should (be (an [Atom]) and have ('numberOfArguments (2)))
+  }
+
+  it should "have an empty extension list" in {
+    val skolem = SkolemStrategy.Constant(class_OWLObjectSomeValuesFrom.toString)
+    val visitor = RDFoxClassExprConverter(term_x,skolem)
+    val result = class_OWLObjectSomeValuesFrom.accept(visitor)
+    result.ext shouldBe empty
+  }
+
+  // OWLObjectMaxCardinalityImpl
+  class_OWLObjectMaxCardinality.toString should
+    "be converted into a RDFoxRuleShards" in {
+      val visitor = RDFoxClassExprConverter(term_x)
+      val result = class_OWLObjectMaxCardinality.accept(visitor)
+      result shouldBe a [RDFoxRuleShards]
+  }
+
+  it should "have a single <owl:sameAs> Atom in the result list" in {
+    val visitor = RDFoxClassExprConverter(term_x)
+    val result = class_OWLObjectMaxCardinality.accept(visitor)
+    result.res.loneElement should (be (an [Atom]) and have ('predicate (pred_sameAs)))
+  }
+
+  it should "have two unary Atoms in its extension list" in {
+    val visitor = RDFoxClassExprConverter(term_x)
+    val result = class_OWLObjectMaxCardinality.accept(visitor)
+    exactly (2, result.ext) should (be (an [Atom]) and have ('numberOfArguments (1)))
+  }
+
+  it should "have two binary Atoms in its extension list" in {
+    val visitor = RDFoxClassExprConverter(term_x)
+    val result = class_OWLObjectMaxCardinality.accept(visitor)
+    exactly (2, result.ext) should (be (an [Atom]) and have ('numberOfArguments (2)))
+  }
+
+} // class OWLClassSpec