diff options
author | Federico Igne <federico.igne@cs.ox.ac.uk> | 2020-11-18 19:13:25 +0000 |
---|---|---|
committer | Federico Igne <federico.igne@cs.ox.ac.uk> | 2020-11-18 19:13:25 +0000 |
commit | 1efc189e90240c162b54cbc50362b46786643dad (patch) | |
tree | 9beabe0a2af7ba1674aea0060787782aa72e8a83 /src/main/scala/rsacomb/SkolemStrategy.scala | |
parent | a45aeff72b82bbc9a52f10929bf15b414c868525 (diff) | |
download | RSAComb-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.scala | 78 |
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 @@ | |||
1 | package rsacomb | ||
2 | |||
3 | import tech.oxfordsemantic.jrdfox.logic.Datatype | ||
4 | import tech.oxfordsemantic.jrdfox.logic.expression.{Literal, IRI} | ||
5 | |||
6 | sealed trait SkolemStrategy | ||
7 | |||
8 | object 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 | } | ||