aboutsummaryrefslogtreecommitdiff
path: root/src/main/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
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')
-rw-r--r--src/main/scala/rsacomb/RDFoxClassExprConverter.scala8
-rw-r--r--src/main/scala/rsacomb/SkolemStrategy.scala20
2 files changed, 20 insertions, 8 deletions
diff --git a/src/main/scala/rsacomb/RDFoxClassExprConverter.scala b/src/main/scala/rsacomb/RDFoxClassExprConverter.scala
index de0f623..7f44ab1 100644
--- a/src/main/scala/rsacomb/RDFoxClassExprConverter.scala
+++ b/src/main/scala/rsacomb/RDFoxClassExprConverter.scala
@@ -20,6 +20,7 @@ import tech.oxfordsemantic.jrdfox.logic.datalog.{
20} 20}
21import tech.oxfordsemantic.jrdfox.logic.expression.{ 21import tech.oxfordsemantic.jrdfox.logic.expression.{
22 Term, 22 Term,
23 Literal,
23 Variable, 24 Variable,
24 FunctionCall, 25 FunctionCall,
25 IRI 26 IRI
@@ -118,14 +119,13 @@ class RDFoxClassExprConverter(
118 else 119 else
119 (List(), List(), c) 120 (List(), List(), c)
120 } 121 }
121 case SkolemStrategy.Standard(f) => 122 case SkolemStrategy.Standard(f) => {
122 // particular class for the "SKOLEM" operator and it is instead
123 // a simple builtin function with a "special" name.
124 ( 123 (
125 List(), 124 List(),
126 List(BindAtom.create(FunctionCall.create("SKOLEM", term), y)), 125 List(BindAtom.create(FunctionCall.create("SKOLEM", f, term), y)),
127 y 126 y
128 ) 127 )
128 }
129 } 129 }
130 val classVisitor = 130 val classVisitor =
131 new RDFoxClassExprConverter(term1, unsafe, skolem, suffix) 131 new RDFoxClassExprConverter(term1, unsafe, skolem, suffix)
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