9 files changed, 101 insertions, 419 deletions

diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/Main.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/Main.scala
index eaacedc..f54884f 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/Main.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/Main.scala
@@ -64,23 +64,35 @@ object RSAComb extends App {
       case Some(query) => {
         val answers = ontology ask query
         Logger.print(s"$answers", Logger.QUIET)
-        Logger print s"Number of answer: ${answers.length}"
+        Logger print s"Number of answer: ${answers.length} (${answers.lengthWithMultiplicity})"
 
         val unfiltered = ontology askUnfiltered query
-        val percentage = unfiltered match {
-          case Some(u) => {
+        unfiltered map { u =>
+          Logger.print(
+            s"Number of unfiltered answers: ${u.length} (${u.map(_._1).sum}).",
+            Logger.DEBUG
+          )
+          //u foreach println
+          val spurious = {
+            val sp =
+              RDFoxUtil.buildDescriptionQuery("SP", query.variables.length)
+            ontology.queryDataStore(query, sp, RSA.Prefixes)
+          }
+          spurious map { s =>
             Logger.print(
-              s"Number of spurious answers: ${u.length}.",
+              s"Number of spurious answers: ${s.length} (${s.map(_._1).sum})",
+              Logger.DEBUG
+            )
+            //s foreach println
+            val perc =
+              if (u.length > 0) (s.length / u.length.toFloat) * 100 else 0
+            Logger.print(
+              s"Percentage of spurious answers: $perc%",
               Logger.DEBUG
             )
-            if (u.length > 0) (1 - answers.length / u.length) * 100 else 0
           }
-          case None => 0
+
         }
-        Logger.print(
-          s"Percentage of spurious answers: $percentage%",
-          Logger.DEBUG
-        )
       }
       case None =>
         throw new RuntimeException("Submitted query is not conjunctive")
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
index 0f1cd5e..4ac5a77 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
@@ -24,7 +24,11 @@ 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.client.{
+  DataStoreConnection,
+  TransactionType,
+  UpdateType
+}
 import tech.oxfordsemantic.jrdfox.Prefixes
 import tech.oxfordsemantic.jrdfox.logic.datalog.{
   Rule,
@@ -352,22 +356,31 @@ class RSAOntology(val ontology: OWLOntology) {
       val canon = this.canonicalModel
       val filter = this.filteringProgram(query)
 
+      //data.beginTransaction(TransactionType.READ_WRITE)
+
       Logger print s"Canonical model: ${canon.rules.length} rules"
       RDFoxUtil.addRules(data, this.canonicalModel.rules)
 
       Logger print s"Canonical model: ${canon.facts.length} facts"
       RDFoxUtil.addFacts(data, this.canonicalModel.facts)
 
-      RDFoxUtil printStatisticsFor data
+      Logger print s"Filtering program: ${filter.facts.length} facts"
+      RDFoxUtil.addFacts(data, filter.facts)
 
       Logger print s"Filtering program: ${filter.rules.length} rules"
       RDFoxUtil.addRules(data, filter.rules)
 
-      Logger print s"Filtering program: ${filter.facts.length} facts"
-      RDFoxUtil.addFacts(data, filter.facts)
+      //data.commitTransaction()
 
       RDFoxUtil printStatisticsFor data
 
+      //{
+      //  import java.io.{FileOutputStream, File}
+      //  val rules = new FileOutputStream(new File("rules2.dlog"))
+      //  val facts = new FileOutputStream(new File("facts2.ttl"))
+      //  RDFoxUtil.export(data, rules, facts)
+      //}
+
       val answers = {
         val ans = RDFoxUtil.buildDescriptionQuery("Ans", query.answer.size)
         RDFoxUtil
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
deleted file mode 100644
index 1fbf28a..0000000
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxAxiomConverter.scala
+++ /dev/null
@@ -1,134 +0,0 @@
-package uk.ac.ox.cs.rsacomb.converter
-
-import org.semanticweb.owlapi.model.{
-  OWLAxiom,
-  OWLSubClassOfAxiom,
-  OWLEquivalentClassesAxiom,
-  OWLObjectPropertyExpression,
-  OWLObjectPropertyDomainAxiom,
-  OWLObjectPropertyRangeAxiom,
-  OWLDataPropertyDomainAxiom,
-  OWLDataPropertyRangeAxiom,
-  OWLInverseObjectPropertiesAxiom
-}
-import org.semanticweb.owlapi.model.OWLAxiomVisitorEx
-
-import tech.oxfordsemantic.jrdfox.logic.datalog.{
-  Rule,
-  BodyFormula,
-  TupleTableAtom,
-  TupleTableName
-}
-import tech.oxfordsemantic.jrdfox.logic.expression.{
-  Term,
-  IRI => RDFoxIRI,
-  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}
-import uk.ac.manchester.cs.owl.owlapi.OWLSubClassOfAxiomImpl
-import uk.ac.manchester.cs.owl.owlapi.OWLObjectSomeValuesFromImpl
-import uk.ac.manchester.cs.owl.owlapi.OWLClassImpl
-import org.semanticweb.owlapi.model.IRI
-
-object RDFoxAxiomConverter {
-
-  def apply(
-      term: Term,
-      unsafe: List[OWLObjectPropertyExpression],
-      skolem: SkolemStrategy = NoSkolem,
-      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]] {
-
-  import uk.ac.ox.cs.rsacomb.implicits.JavaCollections._
-
-  override def visit(axiom: OWLSubClassOfAxiom): List[Rule] = {
-    // Skolemization is needed only for the head of an axiom
-    val subVisitor =
-      new RDFoxClassExprConverter(term, unsafe, NoSkolem, 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: OWLObjectPropertyDomainAxiom): List[Rule] =
-    axiom.asOWLSubClassOfAxiom.accept(this)
-
-  override def visit(axiom: OWLObjectPropertyRangeAxiom): List[Rule] = {
-    val term1 = RSAOntology.genFreshVariable()
-    val rangeVisitor = new RDFoxClassExprConverter(term, unsafe, skolem, suffix)
-    val range = axiom.getRange.accept(rangeVisitor)
-    val propertyVisitor = new RDFoxPropertyExprConverter(term1, term, suffix)
-    val prop = axiom.getProperty.accept(propertyVisitor)
-    List(Rule.create(range.res, range.ext ::: prop))
-  }
-
-  override def visit(axiom: OWLDataPropertyDomainAxiom): List[Rule] =
-    axiom.asOWLSubClassOfAxiom.accept(this)
-
-  override def visit(axiom: OWLInverseObjectPropertiesAxiom): List[Rule] =
-    axiom.asSubObjectPropertyOfAxioms.asScala.toList.flatMap(_.accept(this))
-
-  override def visit(axiom: OWLClassAssertionAxiom): List[Rule] = {
-    val ind = axiom.getIndividual
-    if (ind.isNamed) {
-      val term = RDFoxIRI.create(ind.asOWLNamedIndividual().getIRI.getIRIString)
-      val cls = axiom.getClassExpression
-      val visitor =
-        new RDFoxClassExprConverter(term, unsafe, NoSkolem, 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
deleted file mode 100644
index 9551c61..0000000
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxClassExprConverter.scala
+++ /dev/null
@@ -1,191 +0,0 @@
-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,
-  OWLDataSomeValuesFrom,
-  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 = NoSkolem,
-      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 = NoSkolem,
-    suffix: RSASuffix = Empty
-) 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 = {
-    // 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 NoSkolem    => (List(), List(), y)
-      case c: Constant => (List(), List(), c.iri)
-      case s: Standard => {
-        (
-          List(),
-          List(
-            BindAtom.create(FunctionCall.create("SKOLEM", s.literal, 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
-    )
-  }
-
-  /** Converts a [[org.semanticweb.owlapi.model.OWLDataSomeValuesFrom OWLDataSomeValuesFrom]]
-    *
-    * @note we assume the expression is "simple", meaning that the
-    * property involved is a role name or the inverse of a role name.
-    * This assumption will be lifted when we will deal with the
-    * normalization of the input ontology.
-    *
-    * @todo the "filler" of this OWL expression is currently ignored. We
-    * need to find a way (if any) to handle
-    * [[org.semanticweb.owlapi.model.OWLDataRange OWLDataRange]]
-    * in RDFox.
-    */
-  override def visit(expr: OWLDataSomeValuesFrom): RDFoxRuleShards = {
-    val y = RSAOntology.genFreshVariable()
-    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 NoSkolem    => (List(), List(), y)
-      case c: Constant => (List(), List(), c.iri)
-      case s: Standard => {
-        (
-          List(),
-          List(
-            BindAtom.create(FunctionCall.create("SKOLEM", s.literal, term), y)
-          ),
-          y
-        )
-      }
-    }
-    val propertyVisitor = new RDFoxPropertyExprConverter(term, term1, suffix)
-    val propertyResult = expr.getProperty.accept(propertyVisitor)
-    RDFoxRuleShards(head ::: propertyResult, body)
-  }
-
-  // OWLObjectMaxCardinality
-  override def visit(expr: OWLObjectMaxCardinality): RDFoxRuleShards = {
-    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/RDFoxConverter.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxConverter.scala
index b4f5adb..845ec1f 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxConverter.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxConverter.scala
@@ -40,7 +40,7 @@ import tech.oxfordsemantic.jrdfox.logic.datalog.{
 import tech.oxfordsemantic.jrdfox.logic.expression.{Term, IRI, FunctionCall}
 import uk.ac.ox.cs.rsacomb.RSAOntology
 import uk.ac.ox.cs.rsacomb.suffix.{Empty, Inverse, RSASuffix}
-import uk.ac.ox.cs.rsacomb.util.RSA
+import uk.ac.ox.cs.rsacomb.util.{RSA, RDFoxUtil}
 
 /** Horn-ALCHOIQ to RDFox axiom converter.
   *
@@ -328,10 +328,7 @@ trait RDFoxConverter {
         val (bind, term1) = skolem match {
           case NoSkolem    => (None, varX)
           case c: Constant => (None, c.iri)
-          case s: Standard => {
-            val func = FunctionCall.create("SKOLEM", s.literal, term)
-            (Some(BindAtom.create(func, varX)), varX)
-          }
+          case s: Standard => (Some(RDFoxUtil.skolem(s.name, term, varX)), varX)
         }
         val (res, ext) = convert(cls, term1, unsafe, skolem, suffix)
         val prop = convert(role, term, term1, suffix)
@@ -359,10 +356,7 @@ trait RDFoxConverter {
         val (bind, term1) = skolem match {
           case NoSkolem    => (None, varX)
           case c: Constant => (None, c.iri)
-          case s: Standard => {
-            val func = FunctionCall.create("SKOLEM", s.literal, term)
-            (Some(BindAtom.create(func, varX)), varX)
-          }
+          case s: Standard => (Some(RDFoxUtil.skolem(s.name, term, varX)), varX)
         }
         val prop = convert(role, term, term1, suffix)
         (List(prop), bind.toList)
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
deleted file mode 100644
index 46a70fa..0000000
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxPropertyExprConverter.scala
+++ /dev/null
@@ -1,45 +0,0 @@
-package uk.ac.ox.cs.rsacomb.converter
-
-import org.semanticweb.owlapi.model.{
-  OWLAnnotationProperty,
-  OWLDataProperty,
-  OWLObjectInverseOf,
-  OWLObjectProperty,
-  OWLPropertyExpression
-}
-import org.semanticweb.owlapi.model.OWLPropertyExpressionVisitorEx
-
-import tech.oxfordsemantic.jrdfox.logic.datalog.TupleTableAtom
-import tech.oxfordsemantic.jrdfox.logic.expression.{Term, IRI, Literal}
-
-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: OWLDataProperty): 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/SkolemStrategy.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/SkolemStrategy.scala
index 2142ff3..426a327 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/SkolemStrategy.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/SkolemStrategy.scala
@@ -53,8 +53,7 @@ case object NoSkolem extends SkolemStrategy {
 case class Standard(axiom: OWLAxiom)(implicit toString: (OWLAxiom) => String)
     extends SkolemStrategy {
   def dup(_axiom: OWLAxiom): Standard = copy(axiom = _axiom)(toString)
-  lazy val literal =
-    Literal.create(s"f_${toString(axiom)}", Datatype.XSD_STRING)
+  lazy val name = s"f_${toString(axiom)}"
 }
 
 /** Constant skolemization
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/implicits/RSAAtom.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/implicits/RSAAtom.scala
index 615722b..9b04f0e 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/implicits/RSAAtom.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/implicits/RSAAtom.scala
@@ -1,17 +1,17 @@
 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.expression.{Literal, FunctionCall, Term}
 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
+import uk.ac.ox.cs.rsacomb.suffix.{RSASuffix, Nth}
+import uk.ac.ox.cs.rsacomb.util.RDFoxUtil
 
 /* Is this the best way to determine if an atom is an RDF triple?
  * Note that we can't use `getNumberOfArguments()` because is not
@@ -24,7 +24,7 @@ import uk.ac.ox.cs.rsacomb.RSAOntology
  * 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)
+ *    Atom.create(TupleTableName.create("rdfox:DefaultTriples"), term1, term2, term3)
  * ```
  */
 
@@ -33,10 +33,14 @@ object RSAAtom {
   implicit class RSAAtom(val atom: TupleTableAtom) {
 
     import RDFox._
+    import JavaCollections._
 
     val name: String = atom.getTupleTableName.getName
 
-    val isRDF: Boolean = name == "internal:triple"
+    val args: List[Term] = atom.getArguments
+
+    val isRDF: Boolean =
+      name == "http://oxfordsemantic.tech/RDFox#DefaultTriples"
 
     val isClassAssertion: Boolean = {
       isRDF && {
@@ -70,19 +74,16 @@ object RSAAtom {
         TupleTableAtom.create(ttname, atom.getArguments())
       }
 
-    lazy val reified: (Option[BindAtom], List[TupleTableAtom]) =
+    lazy val reified: (Option[TupleTableAtom], 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 varS = RSAOntology.genFreshVariable()
+        val skolem = RDFoxUtil.skolem(name, (args :+ varS): _*)
+        val atom = TupleTableAtom.rdf(varS, IRI.RDF_TYPE, name)
         val atoms = args.zipWithIndex
-          .map { case (t, i) => TupleTableAtom.rdf(bvar, name :: Nth(i), t) }
-        (Some(bind), atoms)
+          .map { case (a, i) => TupleTableAtom.rdf(varS, name :: Nth(i), a) }
+        (Some(skolem), atom :: atoms)
       }
   }
-
 }
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 76f720c..d072e48 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
@@ -1,7 +1,6 @@
 package uk.ac.ox.cs.rsacomb.util
 
-import java.io.File
-import java.io.StringReader
+import java.io.{OutputStream, File, StringReader}
 import tech.oxfordsemantic.jrdfox.Prefixes
 import tech.oxfordsemantic.jrdfox.client.{
   ComponentInfo,
@@ -11,6 +10,7 @@ import tech.oxfordsemantic.jrdfox.client.{
   UpdateType
 }
 import tech.oxfordsemantic.jrdfox.formats.SPARQLParser
+import tech.oxfordsemantic.jrdfox.logic.Datatype
 import tech.oxfordsemantic.jrdfox.logic.datalog.{
   Rule,
   BodyFormula,
@@ -18,7 +18,12 @@ import tech.oxfordsemantic.jrdfox.logic.datalog.{
   TupleTableAtom,
   TupleTableName
 }
-import tech.oxfordsemantic.jrdfox.logic.expression.{Resource}
+import tech.oxfordsemantic.jrdfox.logic.expression.{
+  Literal,
+  Resource,
+  Variable,
+  Term
+}
 import tech.oxfordsemantic.jrdfox.logic.sparql.statement.SelectQuery
 import uk.ac.ox.cs.rsacomb.suffix.Nth
 import uk.ac.ox.cs.rsacomb.util.Logger
@@ -69,6 +74,13 @@ object RDFoxUtil {
     (server, data)
   }
 
+  /** Create a built-in `rdfox:SKOLEM` TupleTableAtom. */
+  def skolem(name: String, terms: Term*): TupleTableAtom =
+    TupleTableAtom.create(
+      TupleTableName.SKOLEM,
+      (Literal.create(name, Datatype.XSD_STRING) +: terms): _*
+    )
+
   /** Prints statistics from RDFox datastore.
     *
     * Prints something only when Logger level is set to DEBUG or more.
@@ -127,6 +139,26 @@ object RDFoxUtil {
     query
   }
 
+  /** Export data in `text/turtle`.
+    *
+    * @param data datastore connection from which to export data.
+    * @param rules output stream for rules
+    * @param facts output stream for facts
+    */
+  def export(
+      data: DataStoreConnection,
+      rules: OutputStream,
+      facts: OutputStream
+  ): Unit = {
+    data.exportData(Prefixes.s_emptyPrefixes, facts, "text/turtle", RDFoxOpts())
+    data.exportData(
+      Prefixes.s_emptyPrefixes,
+      rules,
+      "application/x.datalog",
+      RDFoxOpts()
+    )
+  }
+
   /** Parse a SELECT query from a string in SPARQL format.
     *
     * @param query the string containing the SPARQL query
@@ -218,7 +250,7 @@ object RDFoxUtil {
           .map(i => s"?S rsa:${pred :: Nth(i)} ?X$i .")
           .mkString("WHERE {\n", "\n", "\n}")
     } else {
-      s"ASK { ?X a rsa:${pred :: Nth(0)} }"
+      s"ASK { ?X a rsa:$pred }"
     }
   }
 
@@ -231,11 +263,11 @@ object RDFoxUtil {
     * built-in `SKOLEM` funtion of RDFox.
     */
   def reify(rule: Rule): Rule = {
-    val (bs, as) = rule.getHead.map(_.reified).unzip
+    val (sk, as) = rule.getHead.map(_.reified).unzip
     val head: List[TupleTableAtom] = as.flatten
-    val bind: List[BodyFormula] = bs.flatten
+    val skolem: List[BodyFormula] = sk.flatten
     val body: List[BodyFormula] = rule.getBody.map(reify).flatten
-    Rule.create(head, bind ::: body)
+    Rule.create(head, skolem ::: body)
   }
 
   /** Reify a [[tech.oxfordsemantic.jrdfox.logic.datalog.BodyFormula BodyFormula]].
@@ -250,15 +282,16 @@ object RDFoxUtil {
     formula match {
       case atom: TupleTableAtom => atom.reified._2
       case neg: Negation => {
-        val (bs, as) = neg.getNegatedAtoms
+        val (sk, as) = neg.getNegatedAtoms
           .map({
             case a: TupleTableAtom => a.reified
             case a                 => (None, List(a))
           })
           .unzip
-        val bind = bs.flatten.map(_.getBoundVariable)
+        val skolem =
+          sk.flatten.map(_.getArguments.last).collect { case v: Variable => v }
         val atoms = as.flatten
-        List(Negation.create(bind, atoms))
+        List(Negation.create(skolem, atoms))
       }
       case other => List(other)
     }