diff options
author | Federico Igne <federico.igne@cs.ox.ac.uk> | 2020-08-04 11:11:57 +0100 |
---|---|---|
committer | Federico Igne <federico.igne@cs.ox.ac.uk> | 2020-08-04 11:11:57 +0100 |
commit | e8518528a77edf6a28449a57bd96048a6232a5db (patch) | |
tree | 1dca0e5f8cb1b465e85096f4e5699dd75e77b0f0 /src/main/scala | |
parent | 88597503975804e3cb83d116f3cc9a3f12c57461 (diff) | |
download | RSAComb-e8518528a77edf6a28449a57bd96048a6232a5db.tar.gz RSAComb-e8518528a77edf6a28449a57bd96048a6232a5db.zip |
Adapt LP conversion to RSA check
Part of the process involves the search of unsafe roles in the input
ontology. This is still to be implemented and for now the set of unsafe
roles for the testing example is hardcoded.
Diffstat (limited to 'src/main/scala')
-rw-r--r-- | src/main/scala/rsacomb/RDFoxAxiomConverter.scala | 21 | ||||
-rw-r--r-- | src/main/scala/rsacomb/RDFoxClassExprConverter.scala | 46 | ||||
-rw-r--r-- | src/main/scala/rsacomb/RSAComb.scala | 11 | ||||
-rw-r--r-- | src/main/scala/rsacomb/SkolemStrategy.scala | 18 |
4 files changed, 68 insertions, 28 deletions
diff --git a/src/main/scala/rsacomb/RDFoxAxiomConverter.scala b/src/main/scala/rsacomb/RDFoxAxiomConverter.scala index 3edc908..0a79823 100644 --- a/src/main/scala/rsacomb/RDFoxAxiomConverter.scala +++ b/src/main/scala/rsacomb/RDFoxAxiomConverter.scala | |||
@@ -1,36 +1,39 @@ | |||
1 | package rsacomb | 1 | package rsacomb |
2 | 2 | ||
3 | import org.semanticweb.owlapi.model.{OWLAxiom, OWLSubClassOfAxiom, OWLEquivalentClassesAxiom} | 3 | import org.semanticweb.owlapi.model.{OWLAxiom, OWLSubClassOfAxiom, OWLEquivalentClassesAxiom, OWLObjectPropertyExpression} |
4 | import org.semanticweb.owlapi.model.OWLAxiomVisitorEx | 4 | import org.semanticweb.owlapi.model.OWLAxiomVisitorEx |
5 | 5 | ||
6 | import tech.oxfordsemantic.jrdfox.logic.{Rule, BodyFormula} | 6 | import tech.oxfordsemantic.jrdfox.logic.{Rule, BodyFormula} |
7 | import tech.oxfordsemantic.jrdfox.logic.{Atom, Term, Variable, Literal} | 7 | import tech.oxfordsemantic.jrdfox.logic.{Atom, Term, Variable, Literal} |
8 | import tech.oxfordsemantic.jrdfox.logic.{TupleTableName} | ||
8 | 9 | ||
9 | import scala.collection.JavaConverters._ | 10 | import scala.collection.JavaConverters._ |
10 | 11 | ||
11 | import rsacomb.SkolemStrategy | 12 | import rsacomb.SkolemStrategy |
12 | import rsacomb.RDFoxRuleShards | 13 | import rsacomb.RDFoxRuleShards |
13 | import org.semanticweb.owlapi.model.OWLSubObjectPropertyOfAxiom | 14 | import org.semanticweb.owlapi.model.OWLSubObjectPropertyOfAxiom |
15 | import org.semanticweb.owlapi.model.OWLObjectProperty | ||
14 | 16 | ||
15 | object RDFoxAxiomConverter { | 17 | object RDFoxAxiomConverter { |
16 | 18 | ||
17 | def apply(term : Term, skolem : SkolemStrategy) : RDFoxAxiomConverter = | 19 | def apply( |
18 | new RDFoxAxiomConverter(term, skolem) | 20 | term : Term = Variable.create("x"), |
19 | 21 | skolem : SkolemStrategy = SkolemStrategy.None, | |
20 | def apply(term : Term) : RDFoxAxiomConverter = | 22 | unsafe : List[OWLObjectPropertyExpression] = List() |
21 | new RDFoxAxiomConverter(term, SkolemStrategy.None) | 23 | ) : RDFoxAxiomConverter = |
24 | new RDFoxAxiomConverter(term, skolem, unsafe) | ||
22 | 25 | ||
23 | } // object RDFoxAxiomConverter | 26 | } // object RDFoxAxiomConverter |
24 | 27 | ||
25 | class RDFoxAxiomConverter(term : Term, skolem : SkolemStrategy) | 28 | class RDFoxAxiomConverter(term : Term, skolem : SkolemStrategy, unsafe : List[OWLObjectPropertyExpression]) |
26 | extends OWLAxiomVisitorEx[List[Rule]] | 29 | extends OWLAxiomVisitorEx[List[Rule]] |
27 | { | 30 | { |
28 | 31 | ||
29 | override | 32 | override |
30 | def visit(axiom : OWLSubClassOfAxiom) : List[Rule] = { | 33 | def visit(axiom : OWLSubClassOfAxiom) : List[Rule] = { |
31 | // Skolemization is needed only for the head of an axiom | 34 | // Skolemization is needed only for the head of an axiom |
32 | val subVisitor = new RDFoxClassExprConverter(term,SkolemStrategy.None) | 35 | val subVisitor = new RDFoxClassExprConverter(term,SkolemStrategy.None, unsafe) |
33 | val superVisitor = new RDFoxClassExprConverter(term, skolem) | 36 | val superVisitor = new RDFoxClassExprConverter(term, skolem, unsafe) |
34 | // Each visitor returns a `RDFoxRuleShards`, a tuple (res,ext): | 37 | // Each visitor returns a `RDFoxRuleShards`, a tuple (res,ext): |
35 | // - the `res` List is a list of atoms resulting from the conversion | 38 | // - the `res` List is a list of atoms resulting from the conversion |
36 | // of the axiom. | 39 | // of the axiom. |
diff --git a/src/main/scala/rsacomb/RDFoxClassExprConverter.scala b/src/main/scala/rsacomb/RDFoxClassExprConverter.scala index 58bee44..227c25b 100644 --- a/src/main/scala/rsacomb/RDFoxClassExprConverter.scala +++ b/src/main/scala/rsacomb/RDFoxClassExprConverter.scala | |||
@@ -10,14 +10,17 @@ import tech.oxfordsemantic.jrdfox.logic.{Atom, Term, Variable, Literal, Datatype | |||
10 | 10 | ||
11 | import rsacomb.SkolemStrategy | 11 | import rsacomb.SkolemStrategy |
12 | import rsacomb.RDFoxRuleShards | 12 | import rsacomb.RDFoxRuleShards |
13 | import org.semanticweb.owlapi.model.OWLObjectPropertyExpression | ||
14 | import org.semanticweb.owlapi.model.OWLObjectProperty | ||
13 | 15 | ||
14 | object RDFoxClassExprConverter { | 16 | object RDFoxClassExprConverter { |
15 | 17 | ||
16 | def apply(term : Term, skolem : SkolemStrategy) : RDFoxClassExprConverter = | 18 | def apply( |
17 | new RDFoxClassExprConverter(term, skolem) | 19 | term : Term = Variable.create("x"), |
18 | 20 | skolem : SkolemStrategy = SkolemStrategy.None, | |
19 | def apply(term : Term) : RDFoxClassExprConverter = | 21 | unsafe : List[OWLObjectPropertyExpression] = List() |
20 | new RDFoxClassExprConverter(term, SkolemStrategy.None) | 22 | ) : RDFoxClassExprConverter = |
23 | new RDFoxClassExprConverter(term, skolem, unsafe) | ||
21 | 24 | ||
22 | def merge(rules : List[RDFoxRuleShards]) : RDFoxRuleShards = { | 25 | def merge(rules : List[RDFoxRuleShards]) : RDFoxRuleShards = { |
23 | rules.foldLeft(RDFoxRuleShards(List(),List())) { | 26 | rules.foldLeft(RDFoxRuleShards(List(),List())) { |
@@ -31,7 +34,7 @@ object RDFoxClassExprConverter { | |||
31 | 34 | ||
32 | } // object RDFoxClassExprConverter | 35 | } // object RDFoxClassExprConverter |
33 | 36 | ||
34 | class RDFoxClassExprConverter(term : Term, skolem : SkolemStrategy) | 37 | class RDFoxClassExprConverter(term : Term, skolem : SkolemStrategy, unsafe : List[OWLObjectPropertyExpression]) |
35 | extends OWLClassExpressionVisitorEx[RDFoxRuleShards] | 38 | extends OWLClassExpressionVisitorEx[RDFoxRuleShards] |
36 | { | 39 | { |
37 | 40 | ||
@@ -46,7 +49,7 @@ class RDFoxClassExprConverter(term : Term, skolem : SkolemStrategy) | |||
46 | // OWLObjectIntersectionOf | 49 | // OWLObjectIntersectionOf |
47 | override | 50 | override |
48 | def visit(expr : OWLObjectIntersectionOf) : RDFoxRuleShards = { | 51 | def visit(expr : OWLObjectIntersectionOf) : RDFoxRuleShards = { |
49 | val visitor = new RDFoxClassExprConverter(term,skolem) | 52 | val visitor = new RDFoxClassExprConverter(term, skolem, unsafe) |
50 | // TODO: maybe using `flatMap` instead of `merge` + `map` works as well | 53 | // TODO: maybe using `flatMap` instead of `merge` + `map` works as well |
51 | RDFoxClassExprConverter.merge ( | 54 | RDFoxClassExprConverter.merge ( |
52 | expr.asConjunctSet.asScala.toList | 55 | expr.asConjunctSet.asScala.toList |
@@ -75,22 +78,33 @@ class RDFoxClassExprConverter(term : Term, skolem : SkolemStrategy) | |||
75 | // TODO: variables needs to be handled at visitor level. Hardcoding | 78 | // TODO: variables needs to be handled at visitor level. Hardcoding |
76 | // the name of the varibles might lead to errors for complex cases. | 79 | // the name of the varibles might lead to errors for complex cases. |
77 | val y = Variable.create("y") | 80 | val y = Variable.create("y") |
78 | val (fun,term1) = skolem match { | 81 | val prop = expr.getProperty() |
79 | case SkolemStrategy.None => (List(),y) | 82 | // Computes the result of rule skolemization. Depending on the used |
80 | case SkolemStrategy.Constant(c) => (List(), Literal.create(c, Datatype.IRI_REFERENCE)) | 83 | // technique it might involve the introduction of additional atoms, |
84 | // and/or fresh constants and variables. | ||
85 | val (head, body, term1) = skolem match { | ||
86 | case SkolemStrategy.None => (List(), List(), y) | ||
87 | case SkolemStrategy.Constant(c) => (List(), List(), Literal.create(c, Datatype.IRI_REFERENCE)) | ||
88 | case SkolemStrategy.ConstantRSA(c) => { | ||
89 | val lit = Literal.create(c, Datatype.IRI_REFERENCE) | ||
90 | if (unsafe.contains(prop)) | ||
91 | (List(Atom.create(TupleTableName.create("internal:PE"),term,lit), Atom.create(TupleTableName.create("internal:U"),lit)), List(), lit) | ||
92 | else | ||
93 | (List(), List(), lit) | ||
94 | } | ||
81 | case SkolemStrategy.Standard(f) => | 95 | case SkolemStrategy.Standard(f) => |
82 | // At the time of writing the RDFox library does not have a | 96 | // At the time of writing the RDFox library does not have a |
83 | // particular class for the "SKOLEM" operator and it is instead | 97 | // particular class for the "SKOLEM" operator and it is instead |
84 | // a simple builtin function with a special name. | 98 | // a simple builtin function with a "special" name. |
85 | (List(BindAtom.create(BuiltinFunctionCall.create("SKOLEM",term),y)),y) | 99 | (List(),List(BindAtom.create(BuiltinFunctionCall.create("SKOLEM",term),y)),y) |
86 | } | 100 | } |
87 | val classVisitor = new RDFoxClassExprConverter(term1,skolem) | 101 | val classVisitor = new RDFoxClassExprConverter(term1, skolem, unsafe) |
88 | val classResult = expr.getFiller.accept(classVisitor) | 102 | val classResult = expr.getFiller.accept(classVisitor) |
89 | val propertyVisitor = new RDFoxPropertyExprConverter(term, term1, skolem) | 103 | val propertyVisitor = new RDFoxPropertyExprConverter(term, term1, skolem) |
90 | val propertyResult = expr.getProperty.accept(propertyVisitor) | 104 | val propertyResult = expr.getProperty.accept(propertyVisitor) |
91 | RDFoxRuleShards( | 105 | RDFoxRuleShards( |
92 | classResult.res ++ propertyResult, | 106 | classResult.res ++ propertyResult ++ head, |
93 | fun ++ classResult.ext | 107 | classResult.ext ++ body |
94 | ) | 108 | ) |
95 | } | 109 | } |
96 | 110 | ||
@@ -100,7 +114,7 @@ class RDFoxClassExprConverter(term : Term, skolem : SkolemStrategy) | |||
100 | // TODO: again, no hardcoded variables | 114 | // TODO: again, no hardcoded variables |
101 | val vars = List(Variable.create("y"),Variable.create("z")) | 115 | val vars = List(Variable.create("y"),Variable.create("z")) |
102 | val classResult = RDFoxClassExprConverter.merge( | 116 | val classResult = RDFoxClassExprConverter.merge( |
103 | vars.map(new RDFoxClassExprConverter(_,skolem)) | 117 | vars.map(new RDFoxClassExprConverter(_,skolem, unsafe)) |
104 | .map(expr.getFiller.accept(_)) | 118 | .map(expr.getFiller.accept(_)) |
105 | ) | 119 | ) |
106 | val propertyResult = | 120 | val propertyResult = |
diff --git a/src/main/scala/rsacomb/RSAComb.scala b/src/main/scala/rsacomb/RSAComb.scala index a6f237f..62414e9 100644 --- a/src/main/scala/rsacomb/RSAComb.scala +++ b/src/main/scala/rsacomb/RSAComb.scala | |||
@@ -10,7 +10,9 @@ import org.semanticweb.owlapi.model.{OWLAxiom, OWLSubClassOfAxiom, OWLEquivalent | |||
10 | import org.semanticweb.owlapi.model.OWLClassExpression | 10 | import org.semanticweb.owlapi.model.OWLClassExpression |
11 | import org.semanticweb.owlapi.model.OWLOntology | 11 | import org.semanticweb.owlapi.model.OWLOntology |
12 | import org.semanticweb.owlapi.model.OWLOntologyManager | 12 | import org.semanticweb.owlapi.model.OWLOntologyManager |
13 | import org.semanticweb.owlapi.model.IRI | ||
13 | import org.semanticweb.owlapi.model.parameters.Imports | 14 | import org.semanticweb.owlapi.model.parameters.Imports |
15 | import uk.ac.manchester.cs.owl.owlapi.OWLObjectPropertyImpl | ||
14 | 16 | ||
15 | import tech.oxfordsemantic.jrdfox.Prefixes | 17 | import tech.oxfordsemantic.jrdfox.Prefixes |
16 | import tech.oxfordsemantic.jrdfox.client.{ConnectionFactory, ServerConnection, DataStoreConnection} | 18 | import tech.oxfordsemantic.jrdfox.client.{ConnectionFactory, ServerConnection, DataStoreConnection} |
@@ -55,6 +57,11 @@ object RSA { | |||
55 | 57 | ||
56 | val renderer = new DLSyntaxObjectRenderer() | 58 | val renderer = new DLSyntaxObjectRenderer() |
57 | 59 | ||
60 | // Here we need to compute the unsafe roles. This is hardcoded for now. | ||
61 | val unsafe = List( | ||
62 | new OWLObjectPropertyImpl(IRI.create("http://example.com/rsa_example.owl#S")).getInverseProperty() | ||
63 | ) | ||
64 | |||
58 | /* Print TBox axioms */ | 65 | /* Print TBox axioms */ |
59 | println("TBox/RBox:") | 66 | println("TBox/RBox:") |
60 | for { | 67 | for { |
@@ -68,12 +75,12 @@ object RSA { | |||
68 | println("Logic rules:") | 75 | println("Logic rules:") |
69 | for { | 76 | for { |
70 | axiom <- onto.tboxAxioms(Imports.EXCLUDED).collect(Collectors.toList()).asScala | 77 | axiom <- onto.tboxAxioms(Imports.EXCLUDED).collect(Collectors.toList()).asScala |
71 | visitor = new RDFoxAxiomConverter(Variable.create("x"), SkolemStrategy.Constant(axiom.toString)) | 78 | visitor = new RDFoxAxiomConverter(Variable.create("x"), SkolemStrategy.ConstantRSA(axiom.toString), unsafe) |
72 | rule <- axiom.accept(visitor) | 79 | rule <- axiom.accept(visitor) |
73 | } yield println(rule) | 80 | } yield println(rule) |
74 | for { | 81 | for { |
75 | axiom <- onto.rboxAxioms(Imports.EXCLUDED).collect(Collectors.toList()).asScala | 82 | axiom <- onto.rboxAxioms(Imports.EXCLUDED).collect(Collectors.toList()).asScala |
76 | visitor = new RDFoxAxiomConverter(Variable.create("x"), SkolemStrategy.Constant(axiom.toString)) | 83 | visitor = new RDFoxAxiomConverter(Variable.create("x"), SkolemStrategy.ConstantRSA(axiom.toString), unsafe) |
77 | rule <- axiom.accept(visitor) | 84 | rule <- axiom.accept(visitor) |
78 | } yield println(rule) | 85 | } yield println(rule) |
79 | 86 | ||
diff --git a/src/main/scala/rsacomb/SkolemStrategy.scala b/src/main/scala/rsacomb/SkolemStrategy.scala index 9df167f..bcf6828 100644 --- a/src/main/scala/rsacomb/SkolemStrategy.scala +++ b/src/main/scala/rsacomb/SkolemStrategy.scala | |||
@@ -29,7 +29,7 @@ object SkolemStrategy { | |||
29 | def genFunctionString(str : String) = "f_" ++ str.hashCode.toString | 29 | def genFunctionString(str : String) = "f_" ++ str.hashCode.toString |
30 | } | 30 | } |
31 | 31 | ||
32 | /* Functional skolemization | 32 | /* Constant skolemization |
33 | * | 33 | * |
34 | * From | 34 | * From |
35 | * A ⊑ ∃R.B | 35 | * A ⊑ ∃R.B |
@@ -42,5 +42,21 @@ object SkolemStrategy { | |||
42 | def apply(axiom : String) = new Constant(genConstantString(axiom)) | 42 | def apply(axiom : String) = new Constant(genConstantString(axiom)) |
43 | def genConstantString(str : String) = "internal:c_" ++ str.hashCode.toString | 43 | def genConstantString(str : String) = "internal:c_" ++ str.hashCode.toString |
44 | } | 44 | } |
45 | |||
46 | /* (RSA) Constant skolemization | ||
47 | * This is a special skolemization option to introduce additional atoms for RSA | ||
48 | * checking algorithm. | ||
49 | * | ||
50 | * From | ||
51 | * A ⊑ ∃R.B | ||
52 | * to | ||
53 | * 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. | ||
55 | */ | ||
56 | case class ConstantRSA(const : String) extends SkolemStrategy | ||
57 | object ConstantRSA { | ||
58 | def apply(axiom : String) = new ConstantRSA(genConstantString(axiom)) | ||
59 | def genConstantString(str : String) = "internal:c_" ++ str.hashCode.toString | ||
60 | } | ||
45 | } | 61 | } |
46 | 62 | ||