how to convert model checking logic query to SPARQ

问题:

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)

回答1:

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.