10 files changed, 598 insertions, 83 deletions

diff --git a/src/main/scala/rsacomb/FilteringProgram.scala b/src/main/scala/rsacomb/FilteringProgram.scala
new file mode 100644
index 0000000..91c98d8
--- /dev/null
+++ b/src/main/scala/rsacomb/FilteringProgram.scala
@@ -0,0 +1,295 @@
+package rsacomb
+
+import tech.oxfordsemantic.jrdfox.logic._
+import scala.collection.JavaConverters._
+
+class FilteringProgram(query: Query, constants: List[Term]) extends RDFTriple {
+
+  private val bounded: List[Term] = this.getBoundedVariables
+  private val answer: List[Term] = query.getAnswerVariables.asScala.toList
+
+  val facts: List[Atom] = constants.map(named)
+  val rules: List[Rule] = this.generateFilteringProgram()
+
+  private def named(t: Term): Atom =
+    Atom.rdf(t, IRI.RDF_TYPE, RSA.internal("NAMED"))
+
+  private def getBoundedVariables: List[Variable] = List()
+
+  private def generateFilteringProgram(): List[Rule] = {
+    // Query formula as a rule body
+    val body = queryToBody(query.getQueryFormula)
+    // Auxiliar predicates/helpers
+    def not(atom: Atom): BodyFormula = Negation.create(atom)
+    val predQM =
+      Atom.create(
+        TupleTableName.create(RSA.internal("QM").getIRI),
+        (answer ++ bounded): _*
+      )
+    def predID(t1: Term, t2: Term) =
+      Atom.create(
+        TupleTableName.create(RSA.internal("ID").getIRI),
+        (answer ++ bounded).appended(t1).appended(t2): _*
+      )
+    def predNI(t1: Term): Atom =
+      Atom.rdf(t1, IRI.RDF_TYPE, RSA.internal("NI"))
+    def predTQ(sx: String, t1: Term, t2: Term) =
+      Atom.create(
+        TupleTableName.create(RSA.internal(s"TQ_$sx").getIRI),
+        (answer ++ bounded).appended(t1).appended(t2): _*
+      )
+    def predAQ(sx: String, t1: Term, t2: Term) =
+      Atom.create(
+        TupleTableName.create(RSA.internal(s"AQ_$sx").getIRI),
+        (answer ++ bounded).appended(t1).appended(t2): _*
+      )
+    val predFK =
+      Atom.create(
+        TupleTableName.create(RSA.internal("FK").getIRI),
+        (answer ++ bounded): _*
+      )
+    val predSP =
+      Atom.create(
+        TupleTableName.create(RSA.internal("SP").getIRI),
+        (answer ++ bounded): _*
+      )
+    val predANS =
+      Atom.create(
+        TupleTableName.create(RSA.internal("ANS").getIRI),
+        answer: _*
+      )
+
+    /* Rule 1 */
+    val r1 = Rule.create(predQM, body: _*)
+
+    /* Rules 3x */
+    val r3a =
+      for ((v, i) <- bounded.zipWithIndex)
+        yield Rule.create(
+          predID(RSA.internal(i), RSA.internal(i)),
+          predQM,
+          not(predNI(v))
+        )
+    val r3b = Rule.create(
+      predID(Variable.create("V"), Variable.create("U")),
+      predID(Variable.create("U"), Variable.create("V"))
+    )
+    val r3c = Rule.create(
+      predID(Variable.create("U"), Variable.create("W")),
+      predID(Variable.create("U"), Variable.create("V")),
+      predID(Variable.create("V"), Variable.create("W"))
+    )
+
+    /* Rules 4x */
+    val r4a = for {
+      role1 <- body.filter(_.isRoleAssertion)
+      if bounded contains (role1 getArgument 2)
+      role2 <- body.filter(_.isRoleAssertion)
+      if bounded contains (role2 getArgument 2)
+    } yield Rule.create(
+      predFK,
+      role1 suffix "_f",
+      role2 suffix "_f",
+      predID(
+        RSA.internal(bounded.indexOf(role1 getArgument 2)),
+        RSA.internal(bounded.indexOf(role2 getArgument 2))
+      ),
+      not(Atom.rdf(role1 getArgument 0, IRI.SAME_AS, role2 getArgument 0))
+    )
+    val r4b = for {
+      role1 <- body.filter(_.isRoleAssertion)
+      if bounded contains (role1 getArgument 2)
+      role2 <- body.filter(_.isRoleAssertion)
+      if bounded contains (role2 getArgument 0)
+    } yield Rule.create(
+      predFK,
+      role1 suffix "_f",
+      role2 suffix "_b",
+      predID(
+        RSA.internal(bounded.indexOf(role1 getArgument 2)),
+        RSA.internal(bounded.indexOf(role2 getArgument 0))
+      ),
+      not(Atom.rdf(role1 getArgument 0, IRI.SAME_AS, role2 getArgument 2))
+    )
+    val r4c = for {
+      role1 <- body.filter(_.isRoleAssertion)
+      if bounded contains (role1 getArgument 0)
+      role2 <- body.filter(_.isRoleAssertion)
+      if bounded contains (role2 getArgument 0)
+    } yield Rule.create(
+      predFK,
+      role1 suffix "_b",
+      role2 suffix "_b",
+      predID(
+        RSA.internal(bounded.indexOf(role1 getArgument 0)),
+        RSA.internal(bounded.indexOf(role2 getArgument 0))
+      ),
+      not(Atom.rdf(role1 getArgument 2, IRI.SAME_AS, role2 getArgument 2))
+    )
+
+    /* Rules 5x */
+    val r5a = for {
+      role1 <- body.filter(_.isRoleAssertion)
+      role1arg0 = role1 getArgument 0
+      role1arg2 = role1 getArgument 2
+      if bounded contains role1arg0
+      if bounded contains role1arg2
+      role2 <- body.filter(_.isRoleAssertion)
+      role2arg0 = role2 getArgument 0
+      role2arg2 = role2 getArgument 2
+      if bounded contains role2arg0
+      if bounded contains role2arg2
+    } yield Rule.create(
+      predID(
+        RSA.internal(bounded indexOf role1arg0),
+        RSA.internal(bounded indexOf role2arg0)
+      ),
+      role1 suffix "_f",
+      role2 suffix "_f",
+      predID(
+        RSA.internal(bounded indexOf role1arg2),
+        RSA.internal(bounded indexOf role2arg2)
+      ),
+      Atom.rdf(role1arg0, IRI.SAME_AS, role2arg0),
+      not(predNI(role1arg0))
+    )
+    val r5b = for {
+      role1 <- body.filter(_.isRoleAssertion)
+      role1arg0 = role1 getArgument 0
+      role1arg2 = role1 getArgument 2
+      if bounded contains role1arg0
+      if bounded contains role1arg2
+      role2 <- body.filter(_.isRoleAssertion)
+      role2arg0 = role2 getArgument 0
+      role2arg2 = role2 getArgument 2
+      if bounded contains role2arg0
+      if bounded contains role2arg2
+    } yield Rule.create(
+      predID(
+        RSA.internal(bounded indexOf role1arg0),
+        RSA.internal(bounded indexOf role2arg2)
+      ),
+      role1 suffix "_f",
+      role2 suffix "_b",
+      predID(
+        RSA.internal(bounded indexOf role1arg2),
+        RSA.internal(bounded indexOf role2arg0)
+      ),
+      Atom.rdf(role1arg0, IRI.SAME_AS, role2arg2),
+      not(predNI(role1arg0))
+    )
+    val r5c = for {
+      role1 <- body.filter(_.isRoleAssertion)
+      role1arg0 = role1 getArgument 0
+      role1arg2 = role1 getArgument 2
+      if bounded contains role1arg0
+      if bounded contains role1arg2
+      role2 <- body.filter(_.isRoleAssertion)
+      role2arg0 = role2 getArgument 0
+      role2arg2 = role2 getArgument 2
+      if bounded contains role2arg0
+      if bounded contains role2arg2
+    } yield Rule.create(
+      predID(
+        RSA.internal(bounded indexOf role1arg2),
+        RSA.internal(bounded indexOf role2arg2)
+      ),
+      role1 suffix "_b",
+      role2 suffix "_b",
+      predID(
+        RSA.internal(bounded indexOf role1arg0),
+        RSA.internal(bounded indexOf role2arg0)
+      ),
+      Atom.rdf(role1arg2, IRI.SAME_AS, role2arg2),
+      not(predNI(role1arg2))
+    )
+
+    /* Rules 6 */
+    val r6 = for {
+      role <- body.filter(_.isRoleAssertion)
+      arg0 = role getArgument 0
+      arg2 = role getArgument 2
+      if bounded contains arg0
+      if bounded contains arg2
+      sx <- List("_f", "_b")
+    } yield Rule.create(
+      predAQ(sx, Variable.create("V"), Variable.create("W")),
+      role suffix sx,
+      predID(
+        RSA.internal(bounded indexOf arg0),
+        RSA.internal(Variable.create("V"))
+      ),
+      predID(
+        RSA.internal(bounded indexOf arg2),
+        RSA.internal(Variable.create("W"))
+      )
+    )
+
+    /* Rules 7x */
+    val r7a =
+      for (sx <- List("f", "b"))
+        yield Rule.create(
+          predTQ(sx, Variable.create("U"), Variable.create("V")),
+          predAQ(sx, Variable.create("U"), Variable.create("V"))
+        )
+    val r7b =
+      for (r <- List("f", "b"))
+        yield Rule.create(
+          predTQ(r, Variable.create("U"), Variable.create("W")),
+          predAQ(r, Variable.create("U"), Variable.create("V")),
+          predTQ(r, Variable.create("V"), Variable.create("W"))
+        )
+
+    /* Rules 8x */
+    val r8a =
+      for (v <- answer) yield Rule.create(predSP, predQM, not(named(v)))
+    val r8b =
+      Rule.create(predSP, predFK)
+    val r8c =
+      for (sx <- List("_f", "_b"))
+        yield Rule.create(
+          predSP,
+          predTQ(sx, Variable.create("V"), Variable.create("V"))
+        )
+
+    /* Rule 9 */
+    val r9 = Rule.create(predANS, predQM, not(predSP))
+
+    List.empty
+      .prepended(r9)
+      .prependedAll(r8c)
+      .prepended(r8b)
+      .prependedAll(r8a)
+      .prependedAll(r7b)
+      .prependedAll(r7a)
+      .prependedAll(r6)
+      .prependedAll(r5c)
+      .prependedAll(r5b)
+      .prependedAll(r5a)
+      .prependedAll(r4c)
+      .prependedAll(r4b)
+      .prependedAll(r4a)
+      .prepended(r3c)
+      .prepended(r3b)
+      .prependedAll(r3a)
+      .prepended(r1)
+  }
+
+  /* NOTE: we are restricting to queries that contain conjunctions of
+   * atoms for the time being. This might need to be reviewed in the
+   * future.
+   */
+  private def queryToBody(body: Formula): List[Atom] =
+    body match {
+      case a: Atom => List(a);
+      case a: Conjunction =>
+        a.getConjuncts.asScala.toList.flatMap(queryToBody);
+      case _ => List()
+    }
+
+} // class FilteringProgram
+
+object FilteringProgram {
+  def apply(query: Query, constants: List[Term]): FilteringProgram =
+    new FilteringProgram(query, constants)
+}
diff --git a/src/main/scala/rsacomb/Main.scala b/src/main/scala/rsacomb/Main.scala
index 9cd6680..d2bc2a8 100644
--- a/src/main/scala/rsacomb/Main.scala
+++ b/src/main/scala/rsacomb/Main.scala
@@ -48,18 +48,20 @@ object RSAComb {
      */
 
     val ontology = RSA.loadOntology(ontoPath)
-    ontology.isRSA
+    if (ontology.isRSA) {
 
-    /* Build canonical model */
-    //val tboxCanon = rsa.canonicalModel()
+      /* Build canonical model */
+      //val tboxCanon = rsa.canonicalModel()
 
-    /* Load query */
-    //val query = ...
+      /* Load query */
+      val query = RSA.test_query
 
-    /* Compute the filtering program from the given query */
-    //val tboxFilter = rsa.filteringProgram(query)
+      /* Compute the filtering program from the given query */
+      val filter = ontology.getFilteringProgram(query)
 
-    /* ... */
+      /* ... */
+
+    }
 
     /* DEBUG ONLY */
     println("Ok!")
diff --git a/src/main/scala/rsacomb/RDFTriple.scala b/src/main/scala/rsacomb/RDFTriple.scala
new file mode 100644
index 0000000..11ad6d4
--- /dev/null
+++ b/src/main/scala/rsacomb/RDFTriple.scala
@@ -0,0 +1,60 @@
+package rsacomb
+
+import tech.oxfordsemantic.jrdfox.logic.{Atom, IRI, TupleTableName}
+
+trait RDFTriple {
+
+  implicit class RDFTriple(atom: Atom) {
+
+    /* Is this the best way to determine if an atom is an RDF triple?
+     * Note that we can't use `getNumberOfArguments()` because is not
+     * "consistent":
+     * - for an atom created with `rdf(<term1>, <term2>, <term3>)`,
+     * `getNumberOfArguments` returns 3
+     * - for an atom created with `Atom.create(<tupletablename>, <term1>,
+     * <term2>, <term3>)`, `getNumberOfArguments()` returns 3
+     *
+     * This is probably because `Atom.rdf(...) is implemented as:
+     * ```scala
+     *  def rdf(term1: Term, term2: Term, term3: Term): Atom =
+     *    Atom.create(TupleTableName.create("internal:triple"), term1, term2, term3)
+     * ```
+     */
+    def isRdfTriple: Boolean =
+      atom.getTupleTableName.getIRI.equals("internal:triple")
+
+    def isClassAssertion: Boolean =
+      atom.isRdfTriple && atom.getArgument(1).equals(IRI.RDF_TYPE)
+
+    def isRoleAssertion: Boolean =
+      atom.isRdfTriple && !atom.getArgument(1).equals(IRI.RDF_TYPE)
+
+    def suffix(sx: String): Atom =
+      if (this.isClassAssertion) {
+        val newclass = atom.getArgument(2) match {
+          case iri: IRI => IRI.create(iri.getIRI.appendedAll(sx))
+          case other    => other
+        }
+        Atom.rdf(
+          atom getArgument 0,
+          atom getArgument 1,
+          newclass
+        )
+      } else if (this.isRoleAssertion) {
+        val newrole = atom.getArgument(1) match {
+          case iri: IRI => IRI.create(iri.getIRI.appendedAll(sx))
+          case other    => other
+        }
+        Atom.rdf(
+          atom getArgument 0,
+          newrole,
+          atom getArgument 2
+        )
+      } else {
+        val newname =
+          TupleTableName.create(atom.getTupleTableName.getIRI.appendedAll(sx))
+        Atom.create(newname, atom.getArguments())
+      }
+  }
+
+}
diff --git a/src/main/scala/rsacomb/RDFoxAxiomConverter.scala b/src/main/scala/rsacomb/RDFoxAxiomConverter.scala
index 0a79823..d90c966 100644
--- a/src/main/scala/rsacomb/RDFoxAxiomConverter.scala
+++ b/src/main/scala/rsacomb/RDFoxAxiomConverter.scala
@@ -1,6 +1,11 @@
 package rsacomb
 
-import org.semanticweb.owlapi.model.{OWLAxiom, OWLSubClassOfAxiom, OWLEquivalentClassesAxiom, OWLObjectPropertyExpression}
+import org.semanticweb.owlapi.model.{
+  OWLAxiom,
+  OWLSubClassOfAxiom,
+  OWLEquivalentClassesAxiom,
+  OWLObjectPropertyExpression
+}
 import org.semanticweb.owlapi.model.OWLAxiomVisitorEx
 
 import tech.oxfordsemantic.jrdfox.logic.{Rule, BodyFormula}
@@ -17,22 +22,24 @@ import org.semanticweb.owlapi.model.OWLObjectProperty
 object RDFoxAxiomConverter {
 
   def apply(
-    term : Term = Variable.create("x"),
-    skolem : SkolemStrategy = SkolemStrategy.None,
-    unsafe : List[OWLObjectPropertyExpression] = List()
-  ) : RDFoxAxiomConverter =
-          new RDFoxAxiomConverter(term, skolem, unsafe)
+      term: Term,
+      skolem: SkolemStrategy = SkolemStrategy.None,
+      unsafe: List[OWLObjectPropertyExpression] = List()
+  ): RDFoxAxiomConverter =
+    new RDFoxAxiomConverter(term, skolem, unsafe)
 
 } // object RDFoxAxiomConverter
 
-class RDFoxAxiomConverter(term : Term, skolem : SkolemStrategy, unsafe : List[OWLObjectPropertyExpression])
-  extends OWLAxiomVisitorEx[List[Rule]]
-{
+class RDFoxAxiomConverter(
+    term: Term,
+    skolem: SkolemStrategy,
+    unsafe: List[OWLObjectPropertyExpression]
+) extends OWLAxiomVisitorEx[List[Rule]] {
 
-  override
-  def visit(axiom : OWLSubClassOfAxiom) : 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, unsafe)
+    val subVisitor =
+      new RDFoxClassExprConverter(term, SkolemStrategy.None, unsafe)
     val superVisitor = new RDFoxClassExprConverter(term, skolem, unsafe)
     // Each visitor returns a `RDFoxRuleShards`, a tuple (res,ext):
     // - the `res` List is a list of atoms resulting from the conversion
@@ -45,30 +52,27 @@ class RDFoxAxiomConverter(term : Term, skolem : SkolemStrategy, unsafe : List[OW
     val sup = axiom.getSuperClass.accept(superVisitor)
     val head = sup.res.asJava
     val body = (sub.res ++ sup.ext).asJava
-    List(Rule.create(head,body))
+    List(Rule.create(head, body))
   }
 
-  override
-  def visit(axiom : OWLEquivalentClassesAxiom) : List[Rule] = {
+  override def visit(axiom: OWLEquivalentClassesAxiom): List[Rule] = {
     for {
       axiom1 <- axiom.asPairwiseAxioms.asScala.toList
       axiom2 <- axiom1.asOWLSubClassOfAxioms.asScala.toList
-      rule   <- axiom2.accept(this)
+      rule <- axiom2.accept(this)
     } yield rule
   }
 
-  override
-  def visit(axiom : OWLSubObjectPropertyOfAxiom) : List[Rule] = {
-    // TODO: variables needs to be handled at visitor level. Hardcoding
-    // the name of the varibles might lead to errors for complex cases.
-    val term1 = Variable.create("y")
-    val subVisitor = new RDFoxPropertyExprConverter(term,term1,SkolemStrategy.None)
-    val superVisitor = new RDFoxPropertyExprConverter(term,term1,skolem)
+  override def visit(axiom: OWLSubObjectPropertyOfAxiom): List[Rule] = {
+    val term1 = RSA.getFreshVariable()
+    val subVisitor =
+      new RDFoxPropertyExprConverter(term, term1, SkolemStrategy.None)
+    val superVisitor = new RDFoxPropertyExprConverter(term, term1, skolem)
     val body: List[BodyFormula] = axiom.getSubProperty.accept(subVisitor)
     val head: List[Atom] = axiom.getSuperProperty.accept(superVisitor)
-    List(Rule.create(head.asJava,body.asJava))
+    List(Rule.create(head.asJava, body.asJava))
   }
 
-  def doDefault(axiom : OWLAxiom) : List[Rule] = List()
+  def doDefault(axiom: OWLAxiom): List[Rule] = List()
 
 } // class RDFoxAxiomConverter
diff --git a/src/main/scala/rsacomb/RDFoxClassExprConverter.scala b/src/main/scala/rsacomb/RDFoxClassExprConverter.scala
index b9d3ea2..a319d86 100644
--- a/src/main/scala/rsacomb/RDFoxClassExprConverter.scala
+++ b/src/main/scala/rsacomb/RDFoxClassExprConverter.scala
@@ -34,7 +34,7 @@ import org.semanticweb.owlapi.model.OWLObjectProperty
 object RDFoxClassExprConverter {
 
   def apply(
-      term: Term = Variable.create("x"),
+      term: Term,
       skolem: SkolemStrategy = SkolemStrategy.None,
       unsafe: List[OWLObjectPropertyExpression] = List()
   ): RDFoxClassExprConverter =
@@ -61,7 +61,8 @@ class RDFoxClassExprConverter(
 
   // OWLClass
   override def visit(expr: OWLClass): RDFoxRuleShards = {
-    val atom = List(Atom.rdf(term, IRI.RDF_TYPE, expr.getIRI()))
+    val iri: IRI = if (expr.isTopEntity()) IRI.THING else expr.getIRI()
+    val atom = List(Atom.rdf(term, IRI.RDF_TYPE, iri))
     RDFoxRuleShards(atom, List())
   }
 
@@ -94,9 +95,8 @@ class RDFoxClassExprConverter(
 
   // 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 y = RSA.getFreshVariable()
+    // 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,
@@ -139,7 +139,7 @@ class RDFoxClassExprConverter(
   // OWLObjectMaxCardinality
   override def visit(expr: OWLObjectMaxCardinality): RDFoxRuleShards = {
     // TODO: again, no hardcoded variables
-    val vars = List(Variable.create("y"), Variable.create("z"))
+    val vars = List(RSA.getFreshVariable(), RSA.getFreshVariable())
     val classResult = RDFoxClassExprConverter.merge(
       vars
         .map(new RDFoxClassExprConverter(_, skolem, unsafe))
diff --git a/src/main/scala/rsacomb/RDFoxPropertyExprConverter.scala b/src/main/scala/rsacomb/RDFoxPropertyExprConverter.scala
index 340fa90..6eecdbf 100644
--- a/src/main/scala/rsacomb/RDFoxPropertyExprConverter.scala
+++ b/src/main/scala/rsacomb/RDFoxPropertyExprConverter.scala
@@ -3,7 +3,7 @@ package rsacomb
 import org.semanticweb.owlapi.model.{OWLPropertyExpression, OWLObjectProperty}
 import org.semanticweb.owlapi.model.OWLPropertyExpressionVisitorEx
 
-import tech.oxfordsemantic.jrdfox.logic.{Atom, Term, IRI, Variable, Literal}
+import tech.oxfordsemantic.jrdfox.logic.{Atom, Term, IRI, Literal}
 
 import rsacomb.SkolemStrategy
 import org.semanticweb.owlapi.model.OWLObjectInverseOf
diff --git a/src/main/scala/rsacomb/RDFoxUtil.scala b/src/main/scala/rsacomb/RDFoxUtil.scala
index 4cefd83..9699fb4 100644
--- a/src/main/scala/rsacomb/RDFoxUtil.scala
+++ b/src/main/scala/rsacomb/RDFoxUtil.scala
@@ -15,6 +15,10 @@ object RDFoxUtil {
     IRI.create(iri.getIRIString())
   }
 
+  implicit def owlapi2rdfox(iri: String): IRI = {
+    IRI.create(iri)
+  }
+
   def openConnection(
       dataStore: String
   ): (ServerConnection, DataStoreConnection) = {
@@ -37,7 +41,7 @@ object RDFoxUtil {
     (server, data)
   }
 
-  def query(
+  def submitQuery(
       data: DataStoreConnection,
       prefixes: Prefixes,
       query: String
diff --git a/src/main/scala/rsacomb/RSA.scala b/src/main/scala/rsacomb/RSA.scala
index 79617c7..9125f9f 100644
--- a/src/main/scala/rsacomb/RSA.scala
+++ b/src/main/scala/rsacomb/RSA.scala
@@ -8,6 +8,18 @@ import tech.oxfordsemantic.jrdfox.Prefixes
 import tech.oxfordsemantic.jrdfox.logic.IRI
 import org.semanticweb.owlapi.apibinding.OWLManager
 import org.semanticweb.owlapi.model.OWLOntology
+import rsacomb.RSAOntology
+
+// Debug only
+import tech.oxfordsemantic.jrdfox.logic.{
+  Formula,
+  Atom,
+  Variable,
+  Query,
+  QueryType,
+  Conjunction
+}
+import scala.collection.JavaConverters._
 
 object RSA extends RSAOntology {
 
@@ -18,9 +30,30 @@ object RSA extends RSAOntology {
   Prefixes.declarePrefix("rdfs:", "http://www.w3.org/2000/01/rdf-schema#")
   Prefixes.declarePrefix("owl:", "http://www.w3.org/2002/07/owl#")
 
-  def internal(name: String): IRI =
+  // Counter used to implement a simple fresh variable generator
+  private var counter = -1;
+
+  def getFreshVariable(): Variable = {
+    counter += 1
+    Variable.create(f"I$counter%03d")
+  }
+
+  val varX = Variable.create("X")
+  val varY = Variable.create("Y")
+  val varZ = Variable.create("Z")
+  val testAnswerVars = List[Variable](varX, varY, varZ).asJava;
+  val testFormula: Formula =
+    Conjunction.create(
+      Atom.rdf(varX, IRI.TOP_OBJECT_PROPERTY, varY),
+      Atom.rdf(varY, IRI.TOP_OBJECT_PROPERTY, varZ)
+    )
+  val test_query =
+    Query.create(QueryType.SELECT, false, testAnswerVars, testFormula)
+
+  def internal(name: Any): IRI =
     IRI.create(
-      Prefixes.getPrefixIRIsByPrefixName.get("internal:").getIRI + name
+      Prefixes.getPrefixIRIsByPrefixName.get("internal:").getIRI
+        + name.toString
     )
 
   // TODO: move this somewhere else... maybe an OntoUtils class or something.
diff --git a/src/main/scala/rsacomb/RSAAxiom.scala b/src/main/scala/rsacomb/RSAAxiom.scala
index 9e9a016..50dc37e 100644
--- a/src/main/scala/rsacomb/RSAAxiom.scala
+++ b/src/main/scala/rsacomb/RSAAxiom.scala
@@ -1,10 +1,23 @@
 package rsacomb
 
 /* Java imports */
-import org.semanticweb.owlapi.model.{OWLAxiom,OWLSubClassOfAxiom, OWLEquivalentClassesAxiom}
-import org.semanticweb.owlapi.model.{OWLObjectPropertyExpression,OWLClass,OWLClassExpression,OWLObjectSomeValuesFrom,OWLObjectMaxCardinality}
+import org.semanticweb.owlapi.model.{
+  OWLAxiom,
+  OWLSubClassOfAxiom,
+  OWLEquivalentClassesAxiom
+}
+import org.semanticweb.owlapi.model.{
+  OWLObjectPropertyExpression,
+  OWLClass,
+  OWLClassExpression,
+  OWLObjectSomeValuesFrom,
+  OWLObjectMaxCardinality
+}
 import org.semanticweb.owlapi.model.ClassExpressionType
-import org.semanticweb.owlapi.model.{OWLAxiomVisitorEx,OWLClassExpressionVisitorEx}
+import org.semanticweb.owlapi.model.{
+  OWLAxiomVisitorEx,
+  OWLClassExpressionVisitorEx
+}
 
 /* Wrapper trait for the implicit class `RSAAxiom`.
  */
@@ -16,10 +29,10 @@ trait RSAAxiom {
    */
   private sealed trait RSAAxiomType
   private object RSAAxiomType {
-    case object T3    extends RSAAxiomType // ∃R.A ⊑ B
+    case object T3 extends RSAAxiomType // ∃R.A ⊑ B
     case object T3top extends RSAAxiomType // ∃R.⊤ ⊑ B
-    case object T4    extends RSAAxiomType // A ⊑ ≤1R.B
-    case object T5    extends RSAAxiomType // A ⊑ ∃R.B
+    case object T4 extends RSAAxiomType // A ⊑ ≤1R.B
+    case object T5 extends RSAAxiomType // A ⊑ ∃R.B
   }
 
   /* Implements additional features on top of `OWLAxiom` from
@@ -32,20 +45,22 @@ trait RSAAxiom {
      * In order to reason about role unsafety in Horn-ALCHOIQ
      * ontologies we need to detect and filter axioms by their
      * "type".
-     * 
+     *
      * This is a simple implementation following the Visitor
      * pattern imposed by the OWLAPI.
      */
     private class RSAAxiomTypeDetector(t: RSAAxiomType)
-      extends OWLAxiomVisitorEx[Boolean]
-    {
-      override
-      def visit(axiom: OWLSubClassOfAxiom): Boolean = {
+        extends OWLAxiomVisitorEx[Boolean] {
+      override def visit(axiom: OWLSubClassOfAxiom): Boolean = {
         val sub = axiom.getSubClass().getClassExpressionType()
         val sup = axiom.getSuperClass().getClassExpressionType()
         t match {
           case RSAAxiomType.T3top => // ∃R.⊤ ⊑ B
-            axiom.isT5 && axiom.getSubClass().asInstanceOf[OWLObjectSomeValuesFrom].getFiller.isOWLThing
+            axiom.isT3 && axiom
+              .getSubClass()
+              .asInstanceOf[OWLObjectSomeValuesFrom]
+              .getFiller
+              .isOWLThing
           case RSAAxiomType.T3 => // ∃R.A ⊑ B
             sub == ClassExpressionType.OBJECT_SOME_VALUES_FROM && sup == ClassExpressionType.OWL_CLASS
           case RSAAxiomType.T4 => // A ⊑ ≤1R.B
@@ -55,13 +70,12 @@ trait RSAAxiom {
         }
       }
 
-      override
-      def visit(axiom: OWLEquivalentClassesAxiom): Boolean = {
+      override def visit(axiom: OWLEquivalentClassesAxiom): Boolean = {
         // TODO
         false
       }
 
-      def doDefault(axiom : OWLAxiom): Boolean = false
+      def doDefault(axiom: OWLAxiom): Boolean = false
     }
 
     private def isOfType(t: RSAAxiomType): Boolean = {
@@ -74,13 +88,13 @@ trait RSAAxiom {
     def isT3: Boolean = isOfType(RSAAxiomType.T3)
     def isT4: Boolean = isOfType(RSAAxiomType.T4)
     def isT5: Boolean = isOfType(RSAAxiomType.T5)
-    
+
     /* Extracting ObjectPropertyExpressions from axioms
      *
      * This extracts all ObjectPropertyExpressions from a given
      * axiom. While the implementation is generic we use it on axioms
      * of specific types (see above).
-     * 
+     *
      * NOTE: it is not possible to use the `objectPropertyInSignature`
      * method of `OWLAxiom` because it returns all "role names" involved
      * in the signature of an axiom. In particular we won't get the inverse
@@ -88,55 +102,61 @@ trait RSAAxiom {
      * itself instead).
      */
     private class RSAAxiomRoleExtractor()
-      extends OWLAxiomVisitorEx[List[OWLObjectPropertyExpression]]
-    {
+        extends OWLAxiomVisitorEx[List[OWLObjectPropertyExpression]] {
 
       private class RSAExprRoleExtractor()
-        extends OWLClassExpressionVisitorEx[List[OWLObjectPropertyExpression]]
-      {
-        override
-        def visit(expr: OWLObjectSomeValuesFrom): List[OWLObjectPropertyExpression] =
+          extends OWLClassExpressionVisitorEx[
+            List[OWLObjectPropertyExpression]
+          ] {
+        override def visit(
+            expr: OWLObjectSomeValuesFrom
+        ): List[OWLObjectPropertyExpression] =
           List(expr.getProperty)
 
-        override
-        def visit(expr: OWLObjectMaxCardinality): List[OWLObjectPropertyExpression] =
+        override def visit(
+            expr: OWLObjectMaxCardinality
+        ): List[OWLObjectPropertyExpression] =
           List(expr.getProperty)
 
         /* NOTE: this instance of `visit` for `OWLClass` shouldn't be necessary. However
          * if missing, the code throws a `NullPointerException`. It seems like, for some
-         * reason, `OWLClass` is not really a subinterface of `OWLClassExpression`, as 
+         * reason, `OWLClass` is not really a subinterface of `OWLClassExpression`, as
          * stated in the JavaDocs.
          */
-        override
-        def visit(expr: OWLClass): List[OWLObjectPropertyExpression] =
+        override def visit(expr: OWLClass): List[OWLObjectPropertyExpression] =
           List()
 
-        def doDefault(expr: OWLClassExpression): List[OWLObjectPropertyExpression] =
+        def doDefault(
+            expr: OWLClassExpression
+        ): List[OWLObjectPropertyExpression] =
           List()
       }
 
-      override
-      def visit(axiom: OWLSubClassOfAxiom): List[OWLObjectPropertyExpression] = {
+      override def visit(
+          axiom: OWLSubClassOfAxiom
+      ): List[OWLObjectPropertyExpression] = {
         val visitor = new RSAExprRoleExtractor()
         val sub = axiom.getSubClass.accept(visitor)
         val sup = axiom.getSuperClass.accept(visitor)
         sub ++ sup
       }
 
-      override
-      def visit(axiom: OWLEquivalentClassesAxiom): List[OWLObjectPropertyExpression] = {
+      override def visit(
+          axiom: OWLEquivalentClassesAxiom
+      ): List[OWLObjectPropertyExpression] = {
         // TODO
         List()
       }
 
-      def doDefault(axiom : OWLAxiom): List[OWLObjectPropertyExpression] = List()
+      def doDefault(axiom: OWLAxiom): List[OWLObjectPropertyExpression] = List()
     }
 
     /* Exposed methods */
-    def objectPropertyExpressionsInSignature: List[OWLObjectPropertyExpression] = {
+    def objectPropertyExpressionsInSignature
+        : List[OWLObjectPropertyExpression] = {
       val visitor = new RSAAxiomRoleExtractor()
       axiom.accept(visitor)
     }
   }
 
-} // trait RSAAxiom
\ No newline at end of file
+} // trait RSAAxiom
diff --git a/src/main/scala/rsacomb/RSAOntology.scala b/src/main/scala/rsacomb/RSAOntology.scala
index 3d9210e..efd6e7f 100644
--- a/src/main/scala/rsacomb/RSAOntology.scala
+++ b/src/main/scala/rsacomb/RSAOntology.scala
@@ -19,6 +19,7 @@ import scalax.collection.GraphEdge.UnDiEdge
 
 /* Debug only */
 import org.semanticweb.owlapi.dlsyntax.renderer.DLSyntaxObjectRenderer
+import tech.oxfordsemantic.jrdfox.logic._
 
 /* Wrapper trait for the implicit class `RSAOntology`.
  */
@@ -27,7 +28,9 @@ trait RSAOntology {
   /* Implements additional features to reason about RSA ontologies
    * on top of `OWLOntology` from the OWLAPI.
    */
-  implicit class RSAOntology(ontology: OWLOntology) extends RSAAxiom {
+  implicit class RSAOntology(ontology: OWLOntology)
+      extends RSAAxiom
+      with RDFTriple {
 
     /* Steps for RSA check
      * 1) convert ontology axioms into LP rules
@@ -60,7 +63,7 @@ trait RSAOntology {
       val datalog = for {
         axiom <- axioms
         visitor = new RDFoxAxiomConverter(
-          Variable.create("x"),
+          RSA.getFreshVariable(),
           SkolemStrategy.ConstantRSA(axiom.toString),
           unsafe
         )
@@ -163,8 +166,9 @@ trait RSAOntology {
       } yield role1
 
       /* TODO: We should be able to avoid this last conversion to List.
-       * Maybe we should just move everything to Sets instead of Lists, since
-       * they have a more straightforward conversion from Java collections.
+       * Maybe we should just move everything to Sets instead of Lists,
+       * since they have a more straightforward conversion from Java
+       * collections.
        */
       (unsafe1 ++ unsafe2).toList
     }
@@ -184,6 +188,99 @@ trait RSAOntology {
       Graph(edges: _*)
     }
 
+    def getFilteringProgram(query: Query): List[Rule] = {
+
+      // Import implicit conversion to RDFox IRI
+      import RDFoxUtil._
+
+      sealed trait Reified;
+      case class ReifiedHead(bind: BindAtom, atoms: List[Atom]) extends Reified
+      case class ReifiedBody(atoms: List[Atom]) extends Reified
+      case class Unaltered(formula: BodyFormula) extends Reified
+
+      def getBindAtom(atom: Atom): BindAtom = {
+        // TODO: We need to implement another way to introduce fresh
+        // variables.
+        val newvar = RSA.getFreshVariable()
+        val name =
+          Literal.create(atom.getTupleTableName.getIRI, Datatype.XSD_STRING)
+        val args = atom
+          .getArguments()
+          .asScala
+          .toSeq
+          .prepended(name)
+        BindAtom.create(
+          BuiltinFunctionCall
+            .create("SKOLEM", args: _*),
+          newvar
+        )
+      }
+
+      def reifyAtom(atom: Atom, variable: Variable): List[Atom] = {
+        def iri(i: Int) = atom.getTupleTableName().getIRI() ++ s"_$i"
+        atom
+          .getArguments()
+          .asScala
+          .zipWithIndex
+          .map { case (t, i) => Atom.rdf(variable, iri(i), t) }
+          .toList
+      }
+
+      def reify(
+          formula: BodyFormula,
+          head: Boolean
+      ): Reified = {
+        def default[A <: BodyFormula](x: A) = Unaltered(x)
+        formula match {
+          case a: Atom => {
+            if (!a.isRdfTriple) {
+              if (head) {
+                val b = getBindAtom(a)
+                ReifiedHead(b, reifyAtom(a, b.getBoundVariable))
+              } else {
+                val varA = RSA.getFreshVariable()
+                ReifiedBody(reifyAtom(a, varA))
+              }
+            } else {
+              default(a)
+            }
+          }
+          case a => default(a)
+        }
+      }
+
+      def skolemizeRule(rule: Rule): Rule = {
+        // Rule body
+        val body =
+          rule.getBody.asScala.map(reify(_, false)).flatMap {
+            case ReifiedHead(_, _) => List(); /* handle impossible case */
+            case ReifiedBody(x)    => x;
+            case Unaltered(x)      => List(x)
+          }
+        // Rule head
+        val reified = rule.getHead.asScala.map(reify(_, true))
+        val skols = reified.flatMap {
+          case ReifiedHead(x, _) => Some(x);
+          case ReifiedBody(_)    => None; /* handle impossible case */
+          case Unaltered(_)      => None
+        }
+        val head = reified.flatMap {
+          case ReifiedHead(_, x) => x;
+          case ReifiedBody(_)    => List(); /* handle impossible case */
+          case Unaltered(x) =>
+            List(x.asInstanceOf[Atom]) /* Can we do better that a cast? */
+        }
+        Rule.create(head.asJava, (skols ++ body).asJava)
+      }
+
+      // DEBUG
+      val rules = FilteringProgram(query, List()).rules
+      println("FILTERING PROGRAM:")
+      rules.map(skolemizeRule(_)).foreach(println(_))
+
+      List()
+    }
+
   } // implicit class RSAOntology
 
 } // trait RSAOntology