From e8518528a77edf6a28449a57bd96048a6232a5db Mon Sep 17 00:00:00 2001 From: Federico Igne Date: Tue, 4 Aug 2020 11:11:57 +0100 Subject: 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. --- src/main/scala/rsacomb/SkolemStrategy.scala | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) (limited to 'src/main/scala/rsacomb/SkolemStrategy.scala') 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 + } } -- cgit v1.2.3