Re: TEST: Functional and InverseFunctional tests for approval

[...]

> > > > I'm indeed not convinced about having
> > > > existentials in inference rule conclusions
> > > > (except for closed lists denoting sequences)
> > > >
> > > > -- ,
> > > > Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
> > >
> > > Could you explain why you don't like existentials in inference rule
> > > conclusions?  (This is a real question, I don't understand why it 
should
> > > matter.)
> >
> > right, quite simply because they require
> > (in any practical setup I've seen so far)
> > a rewrite with Skolem functions of the
> > univars under which scope they fall;
> > of course there could be solutions found
> > (one could e.g. use  ( :sf @uv ) :p :o .
> > with lists as term addresses or some such)
> > but we're not yet there (and maybe we shouldn't
> > be there taking the scope of this WG ???)
> >
> > -- ,
> > Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
>
> Do you mean in any implemented reasoner?  There are several DL reasoners
> that can handle most of OWL, and don't use Skolem functions.
>
> peter-- ,

I see; of course I didn't mean in any implemented reasoner
but some subclass of them

What I forgot to mention was also the point we discussed in
http://lists.w3.org/Archives/Public/www-webont-wg/2002Aug/0203.html

[[[
OK, e.g. we can't have existentials in the conclusion that are
in the domain of an owl:InverseFunctionalProperty because that
property is simply not defined over it's whole range
(lists in the range of e.g. owl:intersectionOf could contain a
mix of resources being classes, properties, classes/properties
and so many of such intersections simply don't exist and in
general we can't give the list constraints in the premis)
]]]

and also DanC's & JeremyC's arguments of course

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

Received on Thursday, 5 September 2002 09:07:16 UTC