aboutsummaryrefslogtreecommitdiff
path: root/src/main/scala
diff options
context:
space:
mode:
authorFederico Igne <federico.igne@cs.ox.ac.uk>2020-08-04 11:11:57 +0100
committerFederico Igne <federico.igne@cs.ox.ac.uk>2020-08-04 11:11:57 +0100
commite8518528a77edf6a28449a57bd96048a6232a5db (patch)
tree1dca0e5f8cb1b465e85096f4e5699dd75e77b0f0 /src/main/scala
parent88597503975804e3cb83d116f3cc9a3f12c57461 (diff)
downloadRSAComb-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.scala21
-rw-r--r--src/main/scala/rsacomb/RDFoxClassExprConverter.scala46
-rw-r--r--src/main/scala/rsacomb/RSAComb.scala11
-rw-r--r--src/main/scala/rsacomb/SkolemStrategy.scala18
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 @@
1package rsacomb 1package rsacomb
2 2
3import org.semanticweb.owlapi.model.{OWLAxiom, OWLSubClassOfAxiom, OWLEquivalentClassesAxiom} 3import org.semanticweb.owlapi.model.{OWLAxiom, OWLSubClassOfAxiom, OWLEquivalentClassesAxiom, OWLObjectPropertyExpression}
4import org.semanticweb.owlapi.model.OWLAxiomVisitorEx 4import org.semanticweb.owlapi.model.OWLAxiomVisitorEx
5 5
6import tech.oxfordsemantic.jrdfox.logic.{Rule, BodyFormula} 6import tech.oxfordsemantic.jrdfox.logic.{Rule, BodyFormula}
7import tech.oxfordsemantic.jrdfox.logic.{Atom, Term, Variable, Literal} 7import tech.oxfordsemantic.jrdfox.logic.{Atom, Term, Variable, Literal}
8import tech.oxfordsemantic.jrdfox.logic.{TupleTableName}
8 9
9import scala.collection.JavaConverters._ 10import scala.collection.JavaConverters._
10 11
11import rsacomb.SkolemStrategy 12import rsacomb.SkolemStrategy
12import rsacomb.RDFoxRuleShards 13import rsacomb.RDFoxRuleShards
13import org.semanticweb.owlapi.model.OWLSubObjectPropertyOfAxiom 14import org.semanticweb.owlapi.model.OWLSubObjectPropertyOfAxiom
15import org.semanticweb.owlapi.model.OWLObjectProperty
14 16
15object RDFoxAxiomConverter { 17object 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
25class RDFoxAxiomConverter(term : Term, skolem : SkolemStrategy) 28class 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
11import rsacomb.SkolemStrategy 11import rsacomb.SkolemStrategy
12import rsacomb.RDFoxRuleShards 12import rsacomb.RDFoxRuleShards
13import org.semanticweb.owlapi.model.OWLObjectPropertyExpression
14import org.semanticweb.owlapi.model.OWLObjectProperty
13 15
14object RDFoxClassExprConverter { 16object 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
34class RDFoxClassExprConverter(term : Term, skolem : SkolemStrategy) 37class 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
10import org.semanticweb.owlapi.model.OWLClassExpression 10import org.semanticweb.owlapi.model.OWLClassExpression
11import org.semanticweb.owlapi.model.OWLOntology 11import org.semanticweb.owlapi.model.OWLOntology
12import org.semanticweb.owlapi.model.OWLOntologyManager 12import org.semanticweb.owlapi.model.OWLOntologyManager
13import org.semanticweb.owlapi.model.IRI
13import org.semanticweb.owlapi.model.parameters.Imports 14import org.semanticweb.owlapi.model.parameters.Imports
15import uk.ac.manchester.cs.owl.owlapi.OWLObjectPropertyImpl
14 16
15import tech.oxfordsemantic.jrdfox.Prefixes 17import tech.oxfordsemantic.jrdfox.Prefixes
16import tech.oxfordsemantic.jrdfox.client.{ConnectionFactory, ServerConnection, DataStoreConnection} 18import 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