Dan Connolly's tinkering lab notebook

Equality and inconsistency in the rules layer

In the working group that originally did RDFS, there wasn't enough confidence to standardize things that could express inconsistencies, such as disjointness of classes, nor to do equality reasoning a la foaf:mbox. The 2004 versions of RDF and RDFS are now properly grounded in mathematical logic, and OWL specifies owl:disjointWith and owl:differentFrom as well as owl:InverseFunctionalProperty and owl:sameAs.

I have gotten quite a bit of mileage out of N3 rules that capture at least some of the meaning of these constructs. If we feed this to cwm or Euler:

{ ?p a owl:InverseFunctionalProperty.
?u ?p ?w.
?v ?p ?w.
} => { ?u = ?v }.

:Dan foaf:mbox <>;
foaf:name "Dan C.".
:Daniel foaf:mbox <>;
foaf:name "Daniel W. Connolly".

foaf:mbox a owl:InverseFunctionalProperty.

then they will conclude...

:Dan = :Daniel.

And we can use cwm's equality reasoning mode or explicit substitution-of-equals-for-equals rules a la { ?S1 ?P ?O. ?S1 = ?S2 } => { ?S2 ?P ?O } to conclude...

:Dan     = :Dan,
foaf:mbox <>;
foaf:name "Dan C.",
"Daniel W. Connolly" .

To capture owl:disjointWith, I use:

{ [ is rdf:type of ?x ] owl:disjointWith
[ is rdf:type of ?y ] }
=> { ?x owl:differentFrom ?y }.

Taking an example from the DAML walkthru that I worked on with Lynn Stein and Deb McGuinness back in 2000:

    :Female     a rdfs:Class;
daml:disjointWith :Male;
rdfs:subClassOf :Animal .

... and adding :bob a :Male. :jill a :Female gives :bob owl:differentFrom :jill. And from :pat a :Male, :Female, we get :pat owl:differentFrom :pat which is clearly inconsistent.

It's pretty straightforward to write rules to express these features; the axiomatic semantics from Fikes and McGuinness in 2001 represents them in KIF. It's much less straightforward to be sure there are no bugs, such as the inconsistency reported by Baclawski of the UBOT project. So I think ter Horst's paper, Completeness, decidability and complexity of entailment for RDF Schema and a semantic extension involving the OWL vocabulary is a particularly interesting contribution. My study of his rules is in owlth.n3. In many cases, the rules are the ones I have been using for years:

# rdfp1
{ ?p a owl:FunctionalProperty.
?u ?p ?v.
?u ?p ?w.
} => { ?v = ?w }.

But the semantics he gives does not always interpret owl:sameAs as identity; I'd like to understand better why not. He looks for clashes of the form ?v owl:differentFrom ?w; owl:sameAs ?w and ?v owl:disjointWith ?w. ?u a ?v, ?w; isn't it enough to just look for ?x owl:differentFrom ?x and reduce owl:disjointWith to owl:differentFrom by the rule I gave above?