Re: TEST: Functional and InverseFunctional tests for approval

From: "Jos De_Roo" <jos.deroo.jd@belgium.agfa.com>
Subject: Re: TEST: Functional and InverseFunctional tests for approval
Date: Thu, 5 Sep 2002 09:50:28 +0200

> [...]
> 
> > > 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

Received on Thursday, 5 September 2002 08:30:37 UTC