Inférences et Contraintes

En MSL générale la contrainte de type s'écrit (en détail)

\begin{array}{l}
\forall p \forall x \forall y \forall V, C, S, A, P, V', C', S', A', P' \\
S(x, p, y, V, C, S, A, P) \\
\land S(p, \texttt{property constraint }, \texttt{type constraint }, V', C', S', A', P' ) \\
 \to \\
\exists t  \exists V'', C'', S'', A'', P''  S(y, \texttt{instance of}, t, V'', C'', S'', A'', P'' ) \\
 \land \texttt{contains}(\texttt{getClass}(A'), t)
\end{array}

si on veut trouver les x p y qui ne satisfont pas la contrainte il faut une requête du genre

SELECT ?x ?p ?y
WHERE {
  ?x ?p_p ?s_0 . ?s_0 ?p_ps ?y . 
  ?p p:property constraint ?s_1 . ?s_1 ps:property constraint :type constraint
     ; pq:annotationJ ?A .
 FILTER NOT EXISTS {
   ?y instance of _:1 . _:1 instance of ?t  FILTER(extfn:contains(extfn:getClass(?A), ?t) }

Donc il suffit

• de remplacer le CONSTRUCT par un SELECT sur les variables du body
• de mettre dans le FILTER NOT EXISTS tout ce qui est à droite du -->

======> Proposition d'extension du langage de règles

• La tête de la règle peut contenir plusieurs statements et conditions
• Les variables qui n'apparaissent que dans la tête sont des variables existentielles

Une règle du genre

P(x, y) -> Q(x, z), R(z, y)

s'interpréterait comme

\forall x \forall y \exists z \ P(x,y) \to Q(x, z) ∧ R(z, y)

On peut ensuite s'en servir en inférence avec

CONSTRUCT { ?x p:Q _:1 . _:1 ps:Q _:z . _:z p:R _:2 . _:2 ps:R ?y } WHERE { ?x p:P _:3 . _:3 ps:Q ?y FILTER NOT EXISTS { ?x p:Q _:1 . _:1 ps:Q _:4 . _:4 p:R _:2 . _:2 ps:R ?y } }

Ça correspond bien à l'idée que les noeuds blancs représentent des variables quantifiées existentiellement.

On peut aussi s'en servir en mode validation avec

SELECT ?x ?y WHERE { ?x p:P _:3 . _:3 ps:Q ?y FILTER NOT EXISTS { ?x p:Q _:1 . _:1 ps:Q _:z . _:z p:R _:2 . _:2 ps:R ?y } }