aboutsummaryrefslogtreecommitdiff
path: root/src/main/scala/rsacomb/SkolemStrategy.scala
diff options
context:
space:
mode:
authorFederico Igne <federico.igne@cs.ox.ac.uk>2020-11-18 19:13:25 +0000
committerFederico Igne <federico.igne@cs.ox.ac.uk>2020-11-18 19:13:25 +0000
commit1efc189e90240c162b54cbc50362b46786643dad (patch)
tree9beabe0a2af7ba1674aea0060787782aa72e8a83 /src/main/scala/rsacomb/SkolemStrategy.scala
parenta45aeff72b82bbc9a52f10929bf15b414c868525 (diff)
downloadRSAComb-1efc189e90240c162b54cbc50362b46786643dad.tar.gz
RSAComb-1efc189e90240c162b54cbc50362b46786643dad.zip
Reorganize project with Java-like folder structure
Diffstat (limited to 'src/main/scala/rsacomb/SkolemStrategy.scala')
-rw-r--r--src/main/scala/rsacomb/SkolemStrategy.scala78
1 files changed, 0 insertions, 78 deletions
diff --git a/src/main/scala/rsacomb/SkolemStrategy.scala b/src/main/scala/rsacomb/SkolemStrategy.scala
deleted file mode 100644
index a2ad0a1..0000000
--- a/src/main/scala/rsacomb/SkolemStrategy.scala
+++ /dev/null
@@ -1,78 +0,0 @@
1package rsacomb
2
3import tech.oxfordsemantic.jrdfox.logic.Datatype
4import tech.oxfordsemantic.jrdfox.logic.expression.{Literal, IRI}
5
6sealed trait SkolemStrategy
7
8object SkolemStrategy {
9 // TODO: might want to use something else other than `hashCode` as a
10 // function to generate a fresh function/constant
11
12 /* No skolemization at all.
13 *
14 * From
15 * ∃R.A ⊑ B
16 * to
17 * R(x,y), B(y) -> B(x)
18 */
19 case object None extends SkolemStrategy
20
21 /* Functional skolemization
22 *
23 * From
24 * A ⊑ ∃R.B
25 * to
26 * A(x) -> R(x,f(x)), B(f(x))
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.
37 */
38 case class Standard(func: Literal) extends SkolemStrategy
39 object Standard {
40 def apply(axiom: String) =
41 new Standard(
42 Literal.create(genFunctionString(axiom), Datatype.XSD_STRING)
43 )
44 def genFunctionString(str: String) = "f_" ++ str.hashCode.toString
45 }
46
47 /* Constant skolemization
48 *
49 * From
50 * A ⊑ ∃R.B
51 * to
52 * A(y) -> R(x,c), B(c)
53 * for c, fresh constant associated with the input axiom
54 */
55 case class Constant(const: IRI) extends SkolemStrategy
56 object Constant {
57 def apply(axiom: String) =
58 new Constant(IRI.create(genConstantString(axiom)))
59 def genConstantString(str: String) = "c_" ++ str.hashCode.toString
60 }
61
62 /* (RSA) Constant skolemization
63 * This is a special skolemization option to introduce additional atoms for RSA
64 * checking algorithm.
65 *
66 * From
67 * A ⊑ ∃R.B
68 * to
69 * A(y) -> R(x,c), PE(x,c), B(c)
70 * for c, fresh constant associated with the input axiom and PE an internal predicate.
71 */
72 case class ConstantRSA(const: IRI) extends SkolemStrategy
73 object ConstantRSA {
74 def apply(axiom: String) =
75 new ConstantRSA(IRI.create(genConstantString(axiom)))
76 def genConstantString(str: String) = "c_" ++ str.hashCode.toString
77 }
78}