Search code examples
sparqlrdfjenasemantic-webontology

how to convert model checking logic query to SPARQL query?

Suppose I have the following RDF data:

@prefix : <urn:ex:>

:m  :A  "a"
:m  :A  "b"
:m  :A  "c"
:m  :B  "a"
:m  :B  "b"

What SPARQL query could I use to check whether the RDF model satisfies the following logical formula?

∀x A(X) → B(x)
Solution

  • SPARQL doesn't have conditionals or universal quantification, but does have existentials (does anything match this?), (implicit) conjunction and negation (in the 'absence' sense).

    So rewrite the question:

    ∀x A(x) → B(x) ⇒
∀x ¬ ( A(x) ∧ ¬ B(x) ) ⇒
¬ ∃x A(x) ∧ ¬ B(x)

    and that's something SPARQL can do, pretty much:

    # Is there anything of type A but not B?
ASK {
  { ?x a :A } MINUS { ?x a :B }
}

    This query returns true if there are any violations of the constraint.