- From: Jos De_Roo <jos.deroo.jd@belgium.agfa.com>
- Date: Wed, 26 Jun 2002 22:38:14 +0200
- To: las@olin.edu
- Cc: Dan Connolly <connolly@w3.org>, pat hayes <phayes@ai.uwf.edu>, www-webont-wg@w3.org
[...]
> from
> classExists :a
> and
> classEexists :b
> conclude
> [ owl:oneOf ( :a :a :b ) ] owl:sameClassAs [ owl:oneOf ( :b :a :a ) ] .
>
>
> (where classExists is just a shorthand for a statement that the class
exists,
> either using existing owl vocabulary or through some new mechanism)
OK, got that
> After all, if the classes :a and :b don't exist, what would the
consequent
> statement mean, anyway?
well, :a and :b could be individuals, no?
eg:LogicianClass owl:oneOf ( eg:LynnS eg:LynnS eg:PatH ) .
[...]
> Example 3:
>
> > (forall (?x ?L)
> > (=> (ow:item ?L ?x)
> > (exists (?ex1) (and (rdf:type ?x ?ex1) (owl:oneOf ?ex1 ?L))) )
)
> Restatement:
> pull the existential (as a special predicate) into the antecedent of the
> implication, i.e.
>
> (forall (?x ?L ?ex1)
> (=> (and (classExists (?ex1))
> (ow:item ?L ?x))
> (and (rdf:type ?x ?ex1)
> (owl:oneOf ?ex1 ?L))) ) )
>
>
> Again, if ?ex1 doesn't exist, then what on earth could the original
statement
> mean? (And the existence as a class of ?ex1 could be derived
automatically
> from the existence as a class of each of the elements in ?L....)
Well, this is new...
suppose classExists (eg:Number)
then eg:LynnS would be a eg:Number ???
Anyhow, I've already dropped the rule
{ :rule9o1 . ?L owl:item ?x } log:implies { ?x a [ owl:oneOf ?L ] } .
but we still have similar examples such as
{ :rule9u1 . ?L owl:item ?C . ?x a ?C } log:implies { ?x a [ owl:unionOf
?L ] } .
The only way I know (so far) to rewrite rules with existentials
in consequents is by using Skolem functions ala f(?x,?L)
but it was exactly my point to interpret [ owl:OneOf ?L ]
as a function *term*
-- ,
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
Received on Wednesday, 26 June 2002 16:39:01 UTC