Include built-in rules in RSA check

4 files changed, 214 insertions, 112 deletions

diff --git a/src/main/scala/rsacomb/RDFox.scala b/src/main/scala/rsacomb/RDFox.scala
deleted file mode 100644
index a263091..0000000
--- a/src/main/scala/rsacomb/RDFox.scala
+++ /dev/null
@@ -1,24 +0,0 @@
-package rsacomb
-
-/* Java imports */
-import java.util.HashMap
-import tech.oxfordsemantic.jrdfox.client.{ConnectionFactory,ServerConnection,DataStoreConnection}
-
-object RDFox {
-
-    def openConnection(dataStore: String): (ServerConnection,DataStoreConnection) = {
-      val serverUrl = "rdfox:local"
-      val role = ""
-      val password = ""
-      val server = ConnectionFactory.newServerConnection(serverUrl, role, password)
-      server.createDataStore(dataStore,"seq",new HashMap())
-      val data = server.newDataStoreConnection(dataStore)
-      (server,data)
-    }
-
-    def closeConnection(server: ServerConnection, data: DataStoreConnection): Unit = {
-      server.close();
-      data.close();
-    }
-
-} // object RDFox
\ No newline at end of file
diff --git a/src/main/scala/rsacomb/RDFoxClassExprConverter.scala b/src/main/scala/rsacomb/RDFoxClassExprConverter.scala
index 227c25b..9116be0 100644
--- a/src/main/scala/rsacomb/RDFoxClassExprConverter.scala
+++ b/src/main/scala/rsacomb/RDFoxClassExprConverter.scala
@@ -1,12 +1,29 @@
 package rsacomb
 
 import scala.collection.JavaConverters._
-import java.util.stream.{Stream,Collectors}
+import java.util.stream.{Stream, Collectors}
 
-import org.semanticweb.owlapi.model.{OWLClassExpression, OWLClass, OWLObjectSomeValuesFrom, OWLObjectIntersectionOf, OWLObjectOneOf, OWLObjectMaxCardinality}
+import org.semanticweb.owlapi.model.{
+  OWLClassExpression,
+  OWLClass,
+  OWLObjectSomeValuesFrom,
+  OWLObjectIntersectionOf,
+  OWLObjectOneOf,
+  OWLObjectMaxCardinality
+}
 import org.semanticweb.owlapi.model.OWLClassExpressionVisitorEx
-import tech.oxfordsemantic.jrdfox.logic.{BindAtom, BuiltinFunctionCall, TupleTableName}
-import tech.oxfordsemantic.jrdfox.logic.{Atom, Term, Variable, Literal, Datatype}
+import tech.oxfordsemantic.jrdfox.logic.{
+  BindAtom,
+  BuiltinFunctionCall,
+  TupleTableName
+}
+import tech.oxfordsemantic.jrdfox.logic.{
+  Atom,
+  Term,
+  Variable,
+  Literal,
+  Datatype
+}
 
 import rsacomb.SkolemStrategy
 import rsacomb.RDFoxRuleShards
@@ -16,87 +33,100 @@ import org.semanticweb.owlapi.model.OWLObjectProperty
 object RDFoxClassExprConverter {
 
   def apply(
-    term : Term = Variable.create("x"),
-    skolem : SkolemStrategy = SkolemStrategy.None,
-    unsafe : List[OWLObjectPropertyExpression] = List()
-  ) : RDFoxClassExprConverter =
-          new RDFoxClassExprConverter(term, skolem, unsafe)
+      term: Term = Variable.create("x"),
+      skolem: SkolemStrategy = SkolemStrategy.None,
+      unsafe: List[OWLObjectPropertyExpression] = List()
+  ): RDFoxClassExprConverter =
+    new RDFoxClassExprConverter(term, skolem, unsafe)
 
-  def merge(rules : List[RDFoxRuleShards]) : RDFoxRuleShards = {
-    rules.foldLeft(RDFoxRuleShards(List(),List())) {
-      (r1,r2) =>
-        RDFoxRuleShards(
-          r1.res ++ r2.res,
-          r1.ext ++ r2.ext
-        )
+  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, unsafe : List[OWLObjectPropertyExpression])
-  extends OWLClassExpressionVisitorEx[RDFoxRuleShards]
-{
+class RDFoxClassExprConverter(
+    term: Term,
+    skolem: SkolemStrategy,
+    unsafe: List[OWLObjectPropertyExpression]
+) extends OWLClassExpressionVisitorEx[RDFoxRuleShards] {
 
   // OWLClass
-  override
-  def visit(expr : OWLClass) : RDFoxRuleShards = {
+  override def visit(expr: OWLClass): RDFoxRuleShards = {
     val name = expr.getIRI.getIRIString
     val atom = List(Atom.create(TupleTableName.create(name), term))
-    RDFoxRuleShards(atom,List())
+    RDFoxRuleShards(atom, List())
   }
 
   // OWLObjectIntersectionOf
-  override
-  def visit(expr : OWLObjectIntersectionOf) : RDFoxRuleShards = {
+  override def visit(expr: OWLObjectIntersectionOf): RDFoxRuleShards = {
     val visitor = new RDFoxClassExprConverter(term, skolem, unsafe)
     // TODO: maybe using `flatMap` instead of `merge` + `map` works as well
-        RDFoxClassExprConverter.merge (
+    RDFoxClassExprConverter.merge(
       expr.asConjunctSet.asScala.toList
-          .map((e : OWLClassExpression) => e.accept(visitor))
+        .map((e: OWLClassExpression) => e.accept(visitor))
     )
   }
 
   // OWLObjectOneOf
-  override
-  def visit(expr : OWLObjectOneOf) : RDFoxRuleShards = {
-    val visitor = RDFoxClassExprConverter(term,skolem)
+  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(
-      TupleTableName.create("owl:sameAs"), term, Literal.create(ind, Datatype.IRI_REFERENCE)
-    ))
-    RDFoxRuleShards(atom,List())
+    val ind = expr.individuals
+      .collect(Collectors.toList())
+      .asScala
+      .filter(_.isOWLNamedIndividual)
+      .head // restricts to proper "nominals"
+      .asOWLNamedIndividual
+      .getIRI
+      .getIRIString
+    val atom = List(
+      Atom.sameAs(term, Literal.create(ind, Datatype.IRI_REFERENCE))
+    )
+    RDFoxRuleShards(atom, List())
   }
 
   // OWLObjectSomeValuesFrom
-  override
-  def visit(expr : OWLObjectSomeValuesFrom) : RDFoxRuleShards = {
+  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 prop = expr.getProperty()
-    // Computes the result of rule skolemization. Depending on the used 
+    // Computes the result of rule skolemization. Depending on the used
     // technique it might involve the introduction of additional atoms,
     // and/or fresh constants and variables.
     val (head, body, term1) = skolem match {
-        case SkolemStrategy.None => (List(), List(), y)
-        case SkolemStrategy.Constant(c) => (List(), List(), Literal.create(c, Datatype.IRI_REFERENCE))
-        case SkolemStrategy.ConstantRSA(c) => {
-          val lit = Literal.create(c, Datatype.IRI_REFERENCE)
-          if (unsafe.contains(prop))
-            (List(Atom.create(TupleTableName.create("internal:PE"),term,lit), Atom.create(TupleTableName.create("internal:U"),lit)), List(), lit)
-          else 
-            (List(), List(), lit)
-        }
-        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(),List(BindAtom.create(BuiltinFunctionCall.create("SKOLEM",term),y)),y)
+      case SkolemStrategy.None => (List(), List(), y)
+      case SkolemStrategy.Constant(c) =>
+        (List(), List(), Literal.create(c, Datatype.IRI_REFERENCE))
+      case SkolemStrategy.ConstantRSA(c) => {
+        val lit = Literal.create(c, Datatype.IRI_REFERENCE)
+        if (unsafe.contains(prop))
+          (
+            List(
+              Atom.create(TupleTableName.create("internal:PE"), term, lit),
+              Atom.create(TupleTableName.create("internal:U"), lit)
+            ),
+            List(),
+            lit
+          )
+        else
+          (List(), List(), lit)
+      }
+      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(),
+          List(BindAtom.create(BuiltinFunctionCall.create("SKOLEM", term), y)),
+          y
+        )
     }
     val classVisitor = new RDFoxClassExprConverter(term1, skolem, unsafe)
     val classResult = expr.getFiller.accept(classVisitor)
@@ -109,25 +139,26 @@ class RDFoxClassExprConverter(term : Term, skolem : SkolemStrategy, unsafe : Lis
   }
 
   // OWLObjectMaxCardinality
-  override
-  def visit(expr : OWLObjectMaxCardinality) : RDFoxRuleShards = {
+  override def visit(expr: OWLObjectMaxCardinality): RDFoxRuleShards = {
     // TODO: again, no hardcoded variables
-    val vars = List(Variable.create("y"),Variable.create("z"))
+    val vars = List(Variable.create("y"), Variable.create("z"))
     val classResult = RDFoxClassExprConverter.merge(
-      vars.map(new RDFoxClassExprConverter(_,skolem, unsafe))
-          .map(expr.getFiller.accept(_))
+      vars
+        .map(new RDFoxClassExprConverter(_, skolem, unsafe))
+        .map(expr.getFiller.accept(_))
     )
-    val propertyResult = 
-      vars.map(new RDFoxPropertyExprConverter(term,_,skolem))
-          .map(expr.getProperty.accept(_))
-          .flatten
+    val propertyResult =
+      vars
+        .map(new RDFoxPropertyExprConverter(term, _, skolem))
+        .map(expr.getProperty.accept(_))
+        .flatten
     RDFoxRuleShards(
-      List(Atom.create(TupleTableName.create("owl:sameAs"),vars(0),vars(1))),
+      List(Atom.create(TupleTableName.create("owl:sameAs"), vars(0), vars(1))),
       classResult.res ++ propertyResult
     )
   }
-        
-  def doDefault(expr : OWLClassExpression) : RDFoxRuleShards =
-    RDFoxRuleShards(List(),List())
+
+  def doDefault(expr: OWLClassExpression): RDFoxRuleShards =
+    RDFoxRuleShards(List(), List())
 
 } // class RDFoxClassExprConverter
diff --git a/src/main/scala/rsacomb/RDFoxUtil.scala b/src/main/scala/rsacomb/RDFoxUtil.scala
new file mode 100644
index 0000000..96710c4
--- /dev/null
+++ b/src/main/scala/rsacomb/RDFoxUtil.scala
@@ -0,0 +1,42 @@
+package rsacomb
+
+/* Java imports */
+import java.util.HashMap
+import tech.oxfordsemantic.jrdfox.client.{
+  ConnectionFactory,
+  ServerConnection,
+  DataStoreConnection
+}
+
+object RDFoxUtil {
+
+  def openConnection(
+      dataStore: String
+  ): (ServerConnection, DataStoreConnection) = {
+    /* Create local server connection
+     */
+    val serverUrl = "rdfox:local"
+    val role = ""
+    val password = ""
+    val server =
+      ConnectionFactory.newServerConnection(serverUrl, role, password)
+
+    /* Create datastore connection
+     */
+    val parameters = new HashMap[String, String]()
+    //parameters.put("equality", "noUNA")
+    server.createDataStore(dataStore, "seq", parameters)
+    val data = server.newDataStoreConnection(dataStore)
+
+    (server, data)
+  }
+
+  def closeConnection(
+      server: ServerConnection,
+      data: DataStoreConnection
+  ): Unit = {
+    server.close();
+    data.close();
+  }
+
+} // object RDFox
diff --git a/src/main/scala/rsacomb/RSAOntology.scala b/src/main/scala/rsacomb/RSAOntology.scala
index 3b08e61..06752ef 100644
--- a/src/main/scala/rsacomb/RSAOntology.scala
+++ b/src/main/scala/rsacomb/RSAOntology.scala
@@ -2,7 +2,7 @@ package rsacomb
 
 /* Java imports */
 import java.util.HashMap
-import java.util.stream.{Collectors,Stream}
+import java.util.stream.{Collectors, Stream}
 
 import org.semanticweb.owlapi.model.OWLOntology
 import org.semanticweb.owlapi.model.OWLObjectPropertyExpression
@@ -13,7 +13,6 @@ import tech.oxfordsemantic.jrdfox.Prefixes
 import tech.oxfordsemantic.jrdfox.logic.Variable
 import tech.oxfordsemantic.jrdfox.client.UpdateType
 
-
 /* Scala imports */
 import scala.collection.JavaConverters._
 
@@ -42,9 +41,14 @@ trait RSAOntology {
        *    step of approximation of an Horn-ALCHOIQ to RSA
        */
 
-      val tbox = 
-        Stream.concat(ontology.tboxAxioms(Imports.INCLUDED), ontology.rboxAxioms(Imports.INCLUDED))
-              .collect(Collectors.toList()).asScala
+      val tbox =
+        Stream
+          .concat(
+            ontology.tboxAxioms(Imports.INCLUDED),
+            ontology.rboxAxioms(Imports.INCLUDED)
+          )
+          .collect(Collectors.toList())
+          .asScala
       val unsafe = ontology.getUnsafeRoles
 
       /* DEBUG: print rules in DL syntax */
@@ -55,18 +59,29 @@ trait RSAOntology {
       /* Ontology convertion into LP rules */
       val datalog = for {
         axiom <- tbox
-        visitor = new RDFoxAxiomConverter(Variable.create("x"), SkolemStrategy.ConstantRSA(axiom.toString), unsafe)
-        rule  <- axiom.accept(visitor)
+        visitor = new RDFoxAxiomConverter(
+          Variable.create("x"),
+          SkolemStrategy.ConstantRSA(axiom.toString),
+          unsafe
+        )
+        rule <- axiom.accept(visitor)
       } yield rule
 
       val prefixes = new Prefixes()
       prefixes.declarePrefix(":", "http://example.com/rsa_example.owl#")
+      prefixes.declarePrefix(
+        "rdf:",
+        "http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+      )
+      prefixes.declarePrefix("rdfs:", "http://www.w3.org/2000/01/rdf-schema#")
+      prefixes.declarePrefix("owl:", "http://www.w3.org/2002/07/owl#")
 
       // Open connection with RDFox
-      val (server,data) = RDFox.openConnection("RSACheck")
+      val (server, data) = RDFoxUtil.openConnection("RSACheck")
       // Add Data (hardcoded for now)
-      data.importData(UpdateType.ADDITION, prefixes,":a a :A .")
-      /* Add Datalog rules
+      data.importData(UpdateType.ADDITION, prefixes, ":a a :A .")
+
+      /* Add rules
        *
        * NOTE:
        * - using the `addRules(...)` method in `DataStoreConnection` is not working as expected, complaining
@@ -76,18 +91,45 @@ trait RSAOntology {
        *   for predicate arguments (e.g., `<predicate>(?X,?Y)`) while the specification for the proprietary RDFox
        *   syntax uses squared brackets (e.g., `<preditate>[?X,?Y]`).
        */
+
+      /* Add built-in rules
+       */
+      data.importData(
+        UpdateType.ADDITION,
+        prefixes,
+        "<internal:E>[?X,?Y] :- <internal:PE>[?X,?Y], <internal:U>[?X], <internal:U>[?Y] ."
+      )
+
+      /* Add ontology rules
+       */
       data.importData(
         UpdateType.ADDITION,
         prefixes,
-        datalog.foldLeft("")((str,rule) => str ++ "\n" ++ rule.toString().replace("(", "[").replace(")","]"))
+        datalog.foldLeft("")((str, rule) =>
+          str ++ "\n" ++ rule.toString().replace("(", "[").replace(")", "]")
+        )
       )
 
       // Retrieve all instances of PE
       println("\nQuery results:")
-      data.evaluateQuery(prefixes,"SELECT ?X ?Y WHERE { ?X <internal:PE> ?Y }", new HashMap[String,String](), System.out, "text/csv");
+      data.evaluateQuery(
+        prefixes,
+        "SELECT ?X ?Y WHERE { ?X <internal:PE> ?Y }",
+        new HashMap[String, String](),
+        System.out,
+        "text/csv"
+      );
+
+      data.evaluateQuery(
+        prefixes,
+        "SELECT ?X ?Y WHERE { ?X <internal:E> ?Y }",
+        new HashMap[String, String](),
+        System.out,
+        "text/csv"
+      );
 
       // Close connection to RDFox
-      RDFox.closeConnection(server,data)
+      RDFoxUtil.closeConnection(server, data)
 
       /* DEBUG */
       true
@@ -98,13 +140,16 @@ trait RSAOntology {
       val factory = new StructuralReasonerFactory()
       val reasoner = factory.createReasoner(ontology)
 
-      val tbox = ontology.tboxAxioms(Imports.INCLUDED).collect(Collectors.toSet()).asScala
+      val tbox = ontology
+        .tboxAxioms(Imports.INCLUDED)
+        .collect(Collectors.toSet())
+        .asScala
 
       /* DEBUG: print rules in DL syntax */
       //val renderer = new DLSyntaxObjectRenderer()
 
       /* Checking for (1) unsafety condition:
-       * 
+       *
        *    For all roles r1 appearing in an axiom of type T5, r1 is unsafe
        *    if there exists a role r2 (different from top) appearing in an axiom
        *    of type T3 and r1 is a subproperty of the inverse of r2.
@@ -113,11 +158,15 @@ trait RSAOntology {
         axiom <- tbox
         if axiom.isT5
         role1 <- axiom.objectPropertyExpressionsInSignature
-        roleSuper = role1 +: reasoner.superObjectProperties(role1).collect(Collectors.toList()).asScala
+        roleSuper =
+          role1 +: reasoner
+            .superObjectProperties(role1)
+            .collect(Collectors.toList())
+            .asScala
         roleSuperInv = roleSuper.map(_.getInverseProperty)
         axiom <- tbox
         if axiom.isT3 && !axiom.isT3top
-        role2 <- axiom.objectPropertyExpressionsInSignature 
+        role2 <- axiom.objectPropertyExpressionsInSignature
         if roleSuperInv.contains(role2)
       } yield role1
 
@@ -126,17 +175,21 @@ trait RSAOntology {
        *    For all roles p1 appearing in an axiom of type T5, p1 is unsafe if
        *    there exists a role p2 appearing in an axiom of type T4 and p1 is a
        *    subproperty of either p2 or the inverse of p2.
-       * 
+       *
        */
       val unsafe2 = for {
         axiom <- tbox
         if axiom.isT5
         role1 <- axiom.objectPropertyExpressionsInSignature
-        roleSuper = role1 +: reasoner.superObjectProperties(role1).collect(Collectors.toList()).asScala
+        roleSuper =
+          role1 +: reasoner
+            .superObjectProperties(role1)
+            .collect(Collectors.toList())
+            .asScala
         roleSuperInv = roleSuper.map(_.getInverseProperty)
         axiom <- tbox
         if axiom.isT4
-        role2 <- axiom.objectPropertyExpressionsInSignature 
+        role2 <- axiom.objectPropertyExpressionsInSignature
         if roleSuper.contains(role2) || roleSuperInv.contains(role2)
       } yield role1
 
@@ -149,4 +202,4 @@ trait RSAOntology {
 
   } // implicit class RSAOntology
 
-} // trait RSAOntology
\ No newline at end of file
+} // trait RSAOntology