From ec76d6cfbf5410fc90060667612461c1e8f3c111 Mon Sep 17 00:00:00 2001 From: Federico Igne Date: Fri, 4 Dec 2020 14:00:21 +0000 Subject: Rework skolemization strategies In particular `ConstantRSA` has been removed, since it was *not* a skolemization strategy. The case for extra atoms generation previously handled by `ConstantRSA` is not dealt with inside the RSA check. --- .../scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala | 22 ++-- .../scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala | 15 +-- .../cs/rsacomb/converter/RDFoxAxiomConverter.scala | 6 +- .../converter/RDFoxClassExprConverter.scala | 38 +++--- .../ox/cs/rsacomb/converter/RDFoxConverter.scala | 62 +++------- .../ox/cs/rsacomb/converter/SkolemStrategy.scala | 134 ++++++++++----------- .../uk/ac/ox/cs/rsacomb/converter/package.scala | 9 ++ 7 files changed, 125 insertions(+), 161 deletions(-) create mode 100644 src/main/scala/uk/ac/ox/cs/rsacomb/converter/package.scala (limited to 'src/main/scala/uk/ac/ox/cs') diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala index bcc336a..c605e51 100644 --- a/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala +++ b/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala @@ -24,12 +24,7 @@ import tech.oxfordsemantic.jrdfox.logic.expression.{ IRI } -import uk.ac.ox.cs.rsacomb.converter.{ - SkolemStrategy, - RDFoxConverter - // RDFoxAxiomConverter, - // RDFoxPropertyExprConverter -} +import uk.ac.ox.cs.rsacomb.converter._ import uk.ac.ox.cs.rsacomb.suffix._ import uk.ac.ox.cs.rsacomb.util.RSA @@ -114,10 +109,8 @@ class CanonicalModel(val ontology: RSAOntology) { val (facts, rules) = { val term = RSAOntology.genFreshVariable() val unsafe = ontology.unsafeRoles - val skolem = SkolemStrategy.None - val suffix = Empty ontology.axioms - .map(CanonicalModelConverter.convert(_, term, unsafe, skolem, suffix)) + .map(CanonicalModelConverter.convert(_, term, unsafe, NoSkolem, Empty)) .unzip } ( @@ -245,10 +238,9 @@ class CanonicalModel(val ontology: RSAOntology) { case a: OWLSubClassOfAxiom if a.isT5 => { val role = axiom.objectPropertyExpressionsInSignature(0) - if (unsafe contains role) { - val skolem = SkolemStrategy.Standard(a.toString) - super.convert(a, term, unsafe, skolem, Forward) - } else { + if (unsafe contains role) + super.convert(a, term, unsafe, new Standard(a), Forward) + else { val (f1, r1) = rules1(a) (f1, r1 ::: rules2(a) ::: rules3(a)) } @@ -256,9 +248,9 @@ class CanonicalModel(val ontology: RSAOntology) { case a: OWLSubObjectPropertyOfAxiom => { val (factsF, rulesF) = - super.convert(a, term, unsafe, SkolemStrategy.None, Forward) + super.convert(a, term, unsafe, NoSkolem, Forward) val (factsB, rulesB) = - super.convert(a, term, unsafe, SkolemStrategy.None, Backward) + super.convert(a, term, unsafe, NoSkolem, Backward) (factsF ::: factsB, rulesF ::: rulesB) } diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala index a965ef9..8fae4c8 100644 --- a/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala +++ b/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala @@ -50,7 +50,7 @@ import org.semanticweb.owlapi.dlsyntax.renderer.DLSyntaxObjectRenderer import tech.oxfordsemantic.jrdfox.logic._ import org.semanticweb.owlapi.model.OWLObjectInverseOf -import uk.ac.ox.cs.rsacomb.converter.{RDFoxConverter, SkolemStrategy} +import uk.ac.ox.cs.rsacomb.converter._ import uk.ac.ox.cs.rsacomb.suffix._ import uk.ac.ox.cs.rsacomb.sparql._ import uk.ac.ox.cs.rsacomb.util.{RDFoxUtil, RSA} @@ -163,16 +163,16 @@ class RSAOntology(val ontology: OWLOntology) { ): Shards = (expr, skolem) match { - case (e: OWLObjectSomeValuesFrom, SkolemStrategy.Constant(c)) + case (e: OWLObjectSomeValuesFrom, c: Constant) if unsafe contains e.getProperty => { val (res, ext) = super.convert(e, term, unsafe, skolem, suffix) - (RSA.PE(term, c) :: RSA.U(c) :: res, ext) + (RSA.PE(term, c.iri) :: RSA.U(c.iri) :: res, ext) } - case (e: OWLDataSomeValuesFrom, SkolemStrategy.Constant(c)) + case (e: OWLDataSomeValuesFrom, c: Constant) if unsafe contains e.getProperty => { val (res, ext) = super.convert(e, term, unsafe, skolem, suffix) - (RSA.PE(term, c) :: RSA.U(c) :: res, ext) + (RSA.PE(term, c.iri) :: RSA.U(c.iri) :: res, ext) } case _ => super.convert(expr, term, unsafe, skolem, suffix) @@ -183,10 +183,7 @@ class RSAOntology(val ontology: OWLOntology) { /* Ontology convertion into LP rules */ val term = RSAOntology.genFreshVariable() val datalog = axioms - .map(a => { - val skolem = SkolemStrategy.Constant(a.toString) - RSAConverter.convert(a, term, unsafe, skolem, Empty) - }) + .map(a => RSAConverter.convert(a, term, unsafe, new Constant(a), Empty)) .unzip val facts = datalog._1.flatten val rules = datalog._2.flatten diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxAxiomConverter.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxAxiomConverter.scala index 93d8f8c..1fbf28a 100644 --- a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxAxiomConverter.scala +++ b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxAxiomConverter.scala @@ -44,7 +44,7 @@ object RDFoxAxiomConverter { def apply( term: Term, unsafe: List[OWLObjectPropertyExpression], - skolem: SkolemStrategy = SkolemStrategy.None, + skolem: SkolemStrategy = NoSkolem, suffix: RSASuffix = Empty ): RDFoxAxiomConverter = new RDFoxAxiomConverter(term, unsafe, skolem, suffix) @@ -63,7 +63,7 @@ class RDFoxAxiomConverter( override def visit(axiom: OWLSubClassOfAxiom): List[Rule] = { // Skolemization is needed only for the head of an axiom val subVisitor = - new RDFoxClassExprConverter(term, unsafe, SkolemStrategy.None, suffix) + new RDFoxClassExprConverter(term, unsafe, NoSkolem, suffix) val superVisitor = new RDFoxClassExprConverter(term, unsafe, skolem, suffix) // Each visitor returns a `RDFoxRuleShards`, a tuple (res,ext): // - the `res` List is a list of atoms resulting from the conversion @@ -121,7 +121,7 @@ class RDFoxAxiomConverter( val term = RDFoxIRI.create(ind.asOWLNamedIndividual().getIRI.getIRIString) val cls = axiom.getClassExpression val visitor = - new RDFoxClassExprConverter(term, unsafe, SkolemStrategy.None, suffix) + new RDFoxClassExprConverter(term, unsafe, NoSkolem, suffix) val shard = cls.accept(visitor) List(Rule.create(shard.res.asJava, shard.ext.asJava)) } else { diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxClassExprConverter.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxClassExprConverter.scala index 4ededf9..9551c61 100644 --- a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxClassExprConverter.scala +++ b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxClassExprConverter.scala @@ -39,7 +39,7 @@ object RDFoxClassExprConverter { def apply( term: Term, unsafe: List[OWLObjectPropertyExpression] = List(), - skolem: SkolemStrategy = SkolemStrategy.None, + skolem: SkolemStrategy = NoSkolem, suffix: RSASuffix = Empty ): RDFoxClassExprConverter = new RDFoxClassExprConverter(term, unsafe, skolem, suffix) @@ -58,8 +58,8 @@ object RDFoxClassExprConverter { class RDFoxClassExprConverter( term: Term, unsafe: List[OWLObjectPropertyExpression], - skolem: SkolemStrategy, - suffix: RSASuffix + skolem: SkolemStrategy = NoSkolem, + suffix: RSASuffix = Empty ) extends OWLClassExpressionVisitorEx[RDFoxRuleShards] { import uk.ac.ox.cs.rsacomb.implicits.RDFox._ @@ -106,18 +106,14 @@ class RDFoxClassExprConverter( // technique it might involve the introduction of additional atoms, // and/or fresh constants and variables. val (head, body, term1) = skolem match { - case SkolemStrategy.None => (List(), List(), y) - case SkolemStrategy.Constant(c) => (List(), List(), c) - case SkolemStrategy.ConstantRSA(c) => { - if (unsafe.contains(prop)) - (List(RSA.PE(term, c), RSA.U(c)), List(), c) - else - (List(), List(), c) - } - case SkolemStrategy.Standard(f) => { + case NoSkolem => (List(), List(), y) + case c: Constant => (List(), List(), c.iri) + case s: Standard => { ( List(), - List(BindAtom.create(FunctionCall.create("SKOLEM", f, term), y)), + List( + BindAtom.create(FunctionCall.create("SKOLEM", s.literal, term), y) + ), y ) } @@ -152,18 +148,14 @@ class RDFoxClassExprConverter( // technique it might involve the introduction of additional atoms, // and/or fresh constants and variables. val (head, body, term1) = skolem match { - case SkolemStrategy.None => (List(), List(), y) - case SkolemStrategy.Constant(c) => (List(), List(), c) - case SkolemStrategy.ConstantRSA(c) => { - if (unsafe.contains(prop)) - (List(RSA.PE(term, c), RSA.U(c)), List(), c) - else - (List(), List(), c) - } - case SkolemStrategy.Standard(f) => { + case NoSkolem => (List(), List(), y) + case c: Constant => (List(), List(), c.iri) + case s: Standard => { ( List(), - List(BindAtom.create(FunctionCall.create("SKOLEM", f, term), y)), + List( + BindAtom.create(FunctionCall.create("SKOLEM", s.literal, term), y) + ), y ) } diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxConverter.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxConverter.scala index 7fd4dbe..1c8374c 100644 --- a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxConverter.scala +++ b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/RDFoxConverter.scala @@ -38,7 +38,7 @@ import tech.oxfordsemantic.jrdfox.logic.datalog.{ } import tech.oxfordsemantic.jrdfox.logic.expression.{Term, IRI, FunctionCall} import uk.ac.ox.cs.rsacomb.RSAOntology -import uk.ac.ox.cs.rsacomb.suffix.{RSASuffix, Inverse} +import uk.ac.ox.cs.rsacomb.suffix.{Empty, Inverse, RSASuffix} import uk.ac.ox.cs.rsacomb.util.RSA /** Horn-ALCHOIQ to RDFox axiom converter. @@ -144,7 +144,7 @@ trait RDFoxConverter { case a: OWLSubClassOfAxiom => { val (sub, _) = - convert(a.getSubClass, term, unsafe, SkolemStrategy.None, suffix) + convert(a.getSubClass, term, unsafe, NoSkolem, suffix) val (sup, ext) = convert(a.getSuperClass, term, unsafe, skolem, suffix) val rule = Rule.create(sup, ext ::: sub) @@ -202,7 +202,7 @@ trait RDFoxConverter { case i: OWLNamedIndividual => { val cls = a.getClassExpression val (res, _) = - convert(cls, i.getIRI, unsafe, SkolemStrategy.None, suffix) + convert(cls, i.getIRI, unsafe, NoSkolem, suffix) ResultF(res) } case _ => Result() @@ -309,32 +309,18 @@ trait RDFoxConverter { case e: OWLObjectSomeValuesFrom => { val cls = e.getFiller() val role = e.getProperty() - // TODO: simplify this: - // Computes the result of rule skolemization. Depending on the used - // technique it might involve the introduction of additional atoms, - // and/or fresh constants and variables. - val (head, body, term1) = skolem match { - case SkolemStrategy.None => - (List(), List(), RSAOntology.genFreshVariable) - case SkolemStrategy.Constant(c) => (List(), List(), c) - case SkolemStrategy.ConstantRSA(c) => { - if (unsafe.contains(role)) - (List(RSA.PE(term, c), RSA.U(c)), List(), c) - else - (List(), List(), c) - } - case SkolemStrategy.Standard(f) => { - val x = RSAOntology.genFreshVariable - ( - List(), - List(BindAtom.create(FunctionCall.create("SKOLEM", f, term), x)), - x - ) + val varX = RSAOntology.genFreshVariable + val (bind, term1) = skolem match { + case NoSkolem => (None, varX) + case c: Constant => (None, c.iri) + case s: Standard => { + val func = FunctionCall.create("SKOLEM", s.literal, term) + (Some(BindAtom.create(func, varX)), varX) } } val (res, ext) = convert(cls, term1, unsafe, skolem, suffix) val prop = convert(role, term, term1, suffix) - (prop :: head ::: res, body ::: ext) + (prop :: res, ext ++ bind) } /** Existential class expression (for data properties). @@ -354,27 +340,17 @@ trait RDFoxConverter { // Computes the result of rule skolemization. Depending on the used // technique it might involve the introduction of additional atoms, // and/or fresh constants and variables. - val (head, body, term1) = skolem match { - case SkolemStrategy.None => - (List(), List(), RSAOntology.genFreshVariable) - case SkolemStrategy.Constant(c) => (List(), List(), c) - case SkolemStrategy.ConstantRSA(c) => { - if (unsafe.contains(role)) - (List(RSA.PE(term, c), RSA.U(c)), List(), c) - else - (List(), List(), c) - } - case SkolemStrategy.Standard(f) => { - val y = RSAOntology.genFreshVariable() - ( - List(), - List(BindAtom.create(FunctionCall.create("SKOLEM", f, term), y)), - y - ) + val varX = RSAOntology.genFreshVariable + val (bind, term1) = skolem match { + case NoSkolem => (None, varX) + case c: Constant => (None, c.iri) + case s: Standard => { + val func = FunctionCall.create("SKOLEM", s.literal, term) + (Some(BindAtom.create(func, varX)), varX) } } val prop = convert(role, term, term1, suffix) - (prop :: head, body) + (List(prop), bind.toList) } /** Maximum cardinality restriction class diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/SkolemStrategy.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/SkolemStrategy.scala index 0d72226..587db91 100644 --- a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/SkolemStrategy.scala +++ b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/SkolemStrategy.scala @@ -1,78 +1,76 @@ package uk.ac.ox.cs.rsacomb.converter +import org.semanticweb.owlapi.model.OWLAxiom import tech.oxfordsemantic.jrdfox.logic.Datatype import tech.oxfordsemantic.jrdfox.logic.expression.{Literal, IRI} sealed trait SkolemStrategy -object SkolemStrategy { - // TODO: might want to use something else other than `hashCode` as a - // function to generate a fresh function/constant +/** No skolemization. + * + * @example role `R` from + * {{{ + * ∃R.A ⊑ B + * }}} + * to + * {{{ + * R(x,y), B(y) -> B(x) + * }}} + */ +case object NoSkolem extends SkolemStrategy - /* No skolemization at all. - * - * From - * ∃R.A ⊑ B - * to - * R(x,y), B(y) -> B(x) - */ - case object None extends SkolemStrategy - - /* Functional skolemization - * - * From - * A ⊑ ∃R.B - * to - * A(x) -> R(x,f(x)), B(f(x)) - * for f, fresh function associated with the input axiom - * - * In RDFox this can represented combining the BIND operator with the - * SKOLEM operator as such: - * A(x), BIND(y, SKOLEM("f", x)) -> R(x,y), B(y) - * The first argument of a SKOLEM call is a literal string (ideally - * identifing the simulated function name). - * - * NOTE: this requirement for the SKOLEM operator is not enforced by - * RDFox, that will fail silently if omitted. - */ - case class Standard(func: Literal) extends SkolemStrategy - object Standard { - def apply(axiom: String) = - new Standard( - Literal.create(genFunctionString(axiom), Datatype.XSD_STRING) - ) - def genFunctionString(str: String) = "f_" ++ str.hashCode.toString - } - - /* Constant skolemization - * - * From - * A ⊑ ∃R.B - * to - * A(y) -> R(x,c), B(c) - * for c, fresh constant associated with the input axiom - */ - case class Constant(const: IRI) extends SkolemStrategy - object Constant { - def apply(axiom: String) = - new Constant(IRI.create(genConstantString(axiom))) - def genConstantString(str: String) = "c_" ++ str.hashCode.toString - } +/** Functional skolemization + * + * The factory object should be used to create new instances of the + * class. + * + * @example role `R` from + * {{{ + * A ⊑ ∃R.B + * }}} + * to + * {{{ + * A(x) -> R(x,f(x)), B(f(x)) + * }}} + * for `f`, fresh function uniquely associated with the input axiom. + * + * RDFox does not support function symbols. We can still implement + * function symbols combining the `BIND` operator with the `SKOLEM` + * operator as such: + * {{{ + * A(x), BIND(y, SKOLEM("f", x)) -> R(x,y), B(y) + * }}} + * The first argument of a `SKOLEM` call '''must''' be a literal string + * (ideally identifing the simulated function name). + * + * @note this requirement is not enforced by RDFox, that will fail + * silently if a string argument is omitted. + */ +class Standard(var axiom: OWLAxiom)(implicit toString: (OWLAxiom) => String) + extends SkolemStrategy { + def dup(a: OWLAxiom) = new Standard(a)(toString) + lazy val literal = + Literal.create(s"f_${toString(axiom)}", Datatype.XSD_STRING) +} - /* (RSA) Constant skolemization - * This is a special skolemization option to introduce additional atoms for RSA - * checking algorithm. - * - * From - * A ⊑ ∃R.B - * to - * A(y) -> R(x,c), PE(x,c), B(c) - * for c, fresh constant associated with the input axiom and PE an internal predicate. - */ - case class ConstantRSA(const: IRI) extends SkolemStrategy - object ConstantRSA { - def apply(axiom: String) = - new ConstantRSA(IRI.create(genConstantString(axiom))) - def genConstantString(str: String) = "c_" ++ str.hashCode.toString - } +/** Constant skolemization + * + * The factory object should be used to create new instances of the + * class. + * + * @example role `R` from + * {{{ + * A ⊑ ∃R.B + * }}} + * to + * {{{ + * A(y) -> R(x,c), B(c) + * }}} + * for `c`, fresh constant '''uniquely''' associated with the input + * axiom + */ +class Constant(var axiom: OWLAxiom)(implicit toString: (OWLAxiom) => String) + extends SkolemStrategy { + def dup(a: OWLAxiom) = new Constant(a)(toString) + lazy val iri = IRI.create(s"c_${toString(axiom)}") } diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/converter/package.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/package.scala new file mode 100644 index 0000000..0484153 --- /dev/null +++ b/src/main/scala/uk/ac/ox/cs/rsacomb/converter/package.scala @@ -0,0 +1,9 @@ +package uk.ac.ox.cs.rsacomb +package object converter { + + import org.semanticweb.owlapi.model.OWLAxiom + + implicit def axiomToHashedString(axiom: OWLAxiom): String = + s"${axiom.toString.hashCode}" + +} -- cgit v1.2.3