aboutsummaryrefslogtreecommitdiff
path: root/src/main/scala/rsacomb/SkolemStrategy.scala
diff options
context:
space:
mode:
authorFederico Igne <federico.igne@cs.ox.ac.uk>2020-11-10 17:16:02 +0000
committerFederico Igne <federico.igne@cs.ox.ac.uk>2020-11-10 17:16:02 +0000
commit43234b253a74e71977ce29d0c7e2947e64fc6966 (patch)
tree02902f1d8afcbd21c20062f31ad4d3e5f8fc5ce7 /src/main/scala/rsacomb/SkolemStrategy.scala
parent159605a3b8b55a8394600a9c73d0c8bccba0546f (diff)
downloadRSAComb-43234b253a74e71977ce29d0c7e2947e64fc6966.tar.gz
RSAComb-43234b253a74e71977ce29d0c7e2947e64fc6966.zip
Fix SKOLEM call creation during function skolemization
The first argument of a SKOLEM call needs to be a literal string. Note that this is not enforced in any way by RDFox, that will fail silently.
Diffstat (limited to 'src/main/scala/rsacomb/SkolemStrategy.scala')
-rw-r--r--src/main/scala/rsacomb/SkolemStrategy.scala20
1 files changed, 16 insertions, 4 deletions
diff --git a/src/main/scala/rsacomb/SkolemStrategy.scala b/src/main/scala/rsacomb/SkolemStrategy.scala
index b05cd17..a2ad0a1 100644
--- a/src/main/scala/rsacomb/SkolemStrategy.scala
+++ b/src/main/scala/rsacomb/SkolemStrategy.scala
@@ -1,6 +1,7 @@
1package rsacomb 1package rsacomb
2 2
3import tech.oxfordsemantic.jrdfox.logic.expression.IRI 3import tech.oxfordsemantic.jrdfox.logic.Datatype
4import tech.oxfordsemantic.jrdfox.logic.expression.{Literal, IRI}
4 5
5sealed trait SkolemStrategy 6sealed trait SkolemStrategy
6 7
@@ -22,13 +23,24 @@ object SkolemStrategy {
22 * From 23 * From
23 * A ⊑ ∃R.B 24 * A ⊑ ∃R.B
24 * to 25 * to
25 * A(y) -> R(x,f(x)), B(f(x)) 26 * A(x) -> R(x,f(x)), B(f(x))
26 * for f, fresh function associated with the input axiom 27 * for f, fresh function associated with the input axiom
28 *
29 * In RDFox this can represented combining the BIND operator with the
30 * SKOLEM operator as such:
31 * A(x), BIND(y, SKOLEM("f", x)) -> R(x,y), B(y)
32 * The first argument of a SKOLEM call is a literal string (ideally
33 * identifing the simulated function name).
34 *
35 * NOTE: this requirement for the SKOLEM operator is not enforced by
36 * RDFox, that will fail silently if omitted.
27 */ 37 */
28 case class Standard(func: IRI) extends SkolemStrategy 38 case class Standard(func: Literal) extends SkolemStrategy
29 object Standard { 39 object Standard {
30 def apply(axiom: String) = 40 def apply(axiom: String) =
31 new Standard(IRI.create(genFunctionString(axiom))) 41 new Standard(
42 Literal.create(genFunctionString(axiom), Datatype.XSD_STRING)
43 )
32 def genFunctionString(str: String) = "f_" ++ str.hashCode.toString 44 def genFunctionString(str: String) = "f_" ++ str.hashCode.toString
33 } 45 }
34 46