Re: LANG: closing issue 4.6 (was Re: ADMIN: Draf agenda for July 25 telecon)

[...]
> Well, an approach where the above passes just involves
> the RDF Core model theory plus a few horn-clause rules:
>
> { :x = :y } log:implies { :y = :x }. # symmetric
> { :x = [ = :z] } log:implies { :x = :z }. # transitive
> { :x :p :y. :x = :z. } log:implies { :z :p :y }.
> { :x :p :y. :p = :q. } log:implies { :x :q :y }.
> { :x :p :y. :y = :z. } log:implies { :x :p :z }.

fully agreed

> (taken from http://www.w3.org/2000/10/swap/test/sameThing.n3,
> lightly edited)
>
>
> My experience with this approach is pretty positive.
> Our implementation is kinda slow, but it's tolerable.
>
>
> I don't have any experience with an approach where
> that test doesn't work.
>
>
> [hmmm... Jos, I see a rule for reflexivity of
> equivalentTo in
>   http://www.agfa.com/w3c/euler/owl-rules
> but not one for transitivity nor symmetry,
> let alone substitution-of-equals-for-equals.].

[I've added those, but we have indeed trouble
with on-the-fly substitution-of-equals-for-equals...
right now we have a pre-flight one, but we should
definitely have a more dynamic unification method...]

-- ,
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/