diff options
Diffstat (limited to 'src/main/scala/rsacomb/SkolemStrategy.scala')
| -rw-r--r-- | src/main/scala/rsacomb/SkolemStrategy.scala | 32 |
1 files changed, 18 insertions, 14 deletions
diff --git a/src/main/scala/rsacomb/SkolemStrategy.scala b/src/main/scala/rsacomb/SkolemStrategy.scala index bcf6828..9d45b4c 100644 --- a/src/main/scala/rsacomb/SkolemStrategy.scala +++ b/src/main/scala/rsacomb/SkolemStrategy.scala | |||
| @@ -1,5 +1,7 @@ | |||
| 1 | package rsacomb | 1 | package rsacomb |
| 2 | 2 | ||
| 3 | import tech.oxfordsemantic.jrdfox.logic.IRI | ||
| 4 | |||
| 3 | sealed trait SkolemStrategy | 5 | sealed trait SkolemStrategy |
| 4 | 6 | ||
| 5 | object SkolemStrategy { | 7 | object SkolemStrategy { |
| @@ -8,7 +10,7 @@ object SkolemStrategy { | |||
| 8 | 10 | ||
| 9 | /* No skolemization at all. | 11 | /* No skolemization at all. |
| 10 | * | 12 | * |
| 11 | * From | 13 | * From |
| 12 | * ∃R.A ⊑ B | 14 | * ∃R.A ⊑ B |
| 13 | * to | 15 | * to |
| 14 | * R(x,y), B(y) -> B(x) | 16 | * R(x,y), B(y) -> B(x) |
| @@ -17,46 +19,48 @@ object SkolemStrategy { | |||
| 17 | 19 | ||
| 18 | /* Functional skolemization | 20 | /* Functional skolemization |
| 19 | * | 21 | * |
| 20 | * From | 22 | * From |
| 21 | * A ⊑ ∃R.B | 23 | * A ⊑ ∃R.B |
| 22 | * to | 24 | * to |
| 23 | * A(y) -> R(x,f(x)), B(f(x)) | 25 | * A(y) -> R(x,f(x)), B(f(x)) |
| 24 | * for f, fresh function associated with the input axiom | 26 | * for f, fresh function associated with the input axiom |
| 25 | */ | 27 | */ |
| 26 | case class Standard(func : String) extends SkolemStrategy | 28 | case class Standard(func: IRI) extends SkolemStrategy |
| 27 | object Standard { | 29 | object Standard { |
| 28 | def apply(axiom : String) = new Standard(genFunctionString(axiom)) | 30 | def apply(axiom: String) = |
| 29 | def genFunctionString(str : String) = "f_" ++ str.hashCode.toString | 31 | new Standard(IRI.create(genFunctionString(axiom))) |
| 32 | def genFunctionString(str: String) = "f_" ++ str.hashCode.toString | ||
| 30 | } | 33 | } |
| 31 | 34 | ||
| 32 | /* Constant skolemization | 35 | /* Constant skolemization |
| 33 | * | 36 | * |
| 34 | * From | 37 | * From |
| 35 | * A ⊑ ∃R.B | 38 | * A ⊑ ∃R.B |
| 36 | * to | 39 | * to |
| 37 | * A(y) -> R(x,c), B(c) | 40 | * A(y) -> R(x,c), B(c) |
| 38 | * for c, fresh constant associated with the input axiom | 41 | * for c, fresh constant associated with the input axiom |
| 39 | */ | 42 | */ |
| 40 | case class Constant(const : String) extends SkolemStrategy | 43 | case class Constant(const: IRI) extends SkolemStrategy |
| 41 | object Constant { | 44 | object Constant { |
| 42 | def apply(axiom : String) = new Constant(genConstantString(axiom)) | 45 | def apply(axiom: String) = |
| 43 | def genConstantString(str : String) = "internal:c_" ++ str.hashCode.toString | 46 | new Constant(IRI.create(genConstantString(axiom))) |
| 47 | def genConstantString(str: String) = "c_" ++ str.hashCode.toString | ||
| 44 | } | 48 | } |
| 45 | 49 | ||
| 46 | /* (RSA) Constant skolemization | 50 | /* (RSA) Constant skolemization |
| 47 | * This is a special skolemization option to introduce additional atoms for RSA | 51 | * This is a special skolemization option to introduce additional atoms for RSA |
| 48 | * checking algorithm. | 52 | * checking algorithm. |
| 49 | * | 53 | * |
| 50 | * From | 54 | * From |
| 51 | * A ⊑ ∃R.B | 55 | * A ⊑ ∃R.B |
| 52 | * to | 56 | * to |
| 53 | * A(y) -> R(x,c), PE(x,c), B(c) | 57 | * A(y) -> R(x,c), PE(x,c), B(c) |
| 54 | * for c, fresh constant associated with the input axiom and PE an internal predicate. | 58 | * for c, fresh constant associated with the input axiom and PE an internal predicate. |
| 55 | */ | 59 | */ |
| 56 | case class ConstantRSA(const : String) extends SkolemStrategy | 60 | case class ConstantRSA(const: IRI) extends SkolemStrategy |
| 57 | object ConstantRSA { | 61 | object ConstantRSA { |
| 58 | def apply(axiom : String) = new ConstantRSA(genConstantString(axiom)) | 62 | def apply(axiom: String) = |
| 59 | def genConstantString(str : String) = "internal:c_" ++ str.hashCode.toString | 63 | new ConstantRSA(IRI.create(genConstantString(axiom))) |
| 64 | def genConstantString(str: String) = "c_" ++ str.hashCode.toString | ||
| 60 | } | 65 | } |
| 61 | } | 66 | } |
| 62 | |||
