Adapt LP conversion to RSA check

Part of the process involves the search of unsafe roles in the input
ontology. This is still to be implemented and for now the set of unsafe
roles for the testing example is hardcoded.

1 files changed, 17 insertions, 1 deletions

diff --git a/src/main/scala/rsacomb/SkolemStrategy.scala b/src/main/scala/rsacomb/SkolemStrategy.scala
index 9df167f..bcf6828 100644
--- a/src/main/scala/rsacomb/SkolemStrategy.scala
+++ b/src/main/scala/rsacomb/SkolemStrategy.scala
@@ -29,7 +29,7 @@ object SkolemStrategy {
     def genFunctionString(str : String) = "f_" ++ str.hashCode.toString
   }
 
-  /* Functional skolemization
+  /* Constant skolemization
    *
    * From 
    *    A ⊑ ∃R.B
@@ -42,5 +42,21 @@ object SkolemStrategy {
     def apply(axiom : String) = new Constant(genConstantString(axiom))
     def genConstantString(str : String) = "internal:c_" ++ str.hashCode.toString
   }
+
+  /* (RSA) Constant skolemization
+   * This is a special skolemization option to introduce additional atoms for RSA
+   * checking algorithm.
+   *
+   * From 
+   *    A ⊑ ∃R.B
+   * to
+   *    A(y) -> R(x,c), PE(x,c), B(c)
+   * for c, fresh constant associated with the input axiom and PE an internal predicate.
+   */
+  case class ConstantRSA(const : String) extends SkolemStrategy
+  object ConstantRSA {
+    def apply(axiom : String) = new ConstantRSA(genConstantString(axiom))
+    def genConstantString(str : String) = "internal:c_" ++ str.hashCode.toString
+  }
 }