Re: some x has only y

I almost put formalizing "Not all eccles cakes are made in Eccles" on  
a third year exam...not a good idea ;)
On 12 Mar 2008, at 09:23, Matthew Pocock wrote:

> I'd like to convert something like

It's that "something like" which is a pita.

> "beer causes karaoke"

I don't think you can get the causal flavor into OWL with any ease.  
That's really the first thing to face.

> into OWL that a) is
> semantically accurate and b) is represented with the minimum of  
> artifice.
>
> The noob error would be to make statements like:
>
>   beer < causes some karaoke
>   beer < causes only karaoke
>
> But, of course, this is placing the quantifier in the wrong place.  
> It says in
> the first case that every beer [drinking experience] causes a karaoke
> [singing experience], and in the second case, that beer causes  
> exclusively
> kraoke.

I think you are making the gensym fallacy here, since I don't think  
that relation is going to remotely resemble causation, no matter what  
we do with it ;)

> We know, of course, possibly from personal experience that beer leads
> to many things other than embarasing public displays of singing and  
> also that
> we don't burst into tune each and every time we down a beer.

There's a regularity and a lawlikness and defeasibility (causes "all  
things being equal"). It'll be true in vacuous cases (where no beer  
exists), but in a funny way (it could be that no beer exists and it's  
false, e.g., if beer doesn't cause karaoke).

> So, we could in our a-box create a 'whitness' model. This would  
> need beer,
> causes and karaoke in the t-box, but no t-box assertions between them.
> Instead, we would add this to the a-box:
>
>   b1 causes k1 ; b1 instanceof beer ; k1 instanceof karaoke
>
> Now, when the ontology is fully classified and all individuals  
> placed, we will
> get an inconsistency if somehow we have made it impossible that  
> beer causes
> karaoke in at least one possible case.

There's no modality to your witness at the logical level. Of course  
you can treat what you're doing as an encoding, but, eww. :) For  
example, how do you distinguish between the witness and the fact that  
(at the moment) no beer is actually causing any karaoke (cause  
there's no beer)?

(This was the problem with the Eccles cake modeling...I was after  
that it's not part of *what it is* to make an Eccles cake that you  
make it in Eccles, thus you *could* make an Eccles cake outside of  
Eccles, and its done often. But at some moment, all the existing  
eccles cakes might have, by chance, been made in Eccles.)

> However, this seems like an ugly way
> forward.

At the very least, you'll want a hell of a lot more either implicitly  
or modeled up.

So, absent an application, I'd tend to start modeling up some theory  
of events/casues/etc.

I suspect it's not what you want :)

> Firstly, we are using these 'whitness models' in a schematic way,
> rather than to represente real examples of things. Secondly, we get  
> the wrong
> kind of error. It will tell us that this a-box is wrong because it  
> clashes
> with the t-box, when in fact it is the t-box which is wrong.
>
> Another way to do this would be to introduce a sub-class of beer  
> [drinking
> experience] called something like "beer drinking that leads to  
> karaoke".
>
> "beer drinking that leads to karaoke" < "beer drinking experience"
> "beer drinking that leads to karaoke" = causes some "karaoke singing
> experience
>
> However, while this gets arround the problems with the a-box  
> approach, this
> has introduced a new named class with a necesarily ugly name.

Is it? Do you need the name? Not in OWL. You can write:

	causes some "karaoke singing experience < "beer drinking experience"

directly.

> It feels like
> we now need extra documentation to allow a user or editor to know  
> that we are
> using subsumption assertion to represent "some" in "some beer leads to
> karaoke" and therefore to tell us more about beer, rather than as a  
> mechanism
> to say something about a specific sub-type of beer. I guess what  
> I'm groping
> towards is 'anonymous sub-classes' so that I could say something like:
>
> subclassof(_ intersection(beer, causes some karaoke))

I don't see why you want this instead of the GCI.

> where _ is a new class identifier, globally unique, each and every  
> time it is
> used.

Why?

> This would require this (anonymous) concept to be satisfiable,

You want to check that its satisfiable? Is that the reason you aren't  
using a GCI? In swoop, you could see such class expressions when they  
were unsatisfaible (with a bit of work). You could add your witness  
instance to the class expression easily to trigger the inconsistency.  
Heck, it wouldn't be that hard to add this as service (though you  
might want to be able to annotate class expressions, which is the  
same thing as your naming bit).

> but
> removes the need to make the ugly names. Fairly trivial tooling  
> could flip
> this into 'some x ...' statements, for user interaction.
>
> I hope that made sense. So is there a standard way to handle 'some'  
> placed at
> this point in an assertion? A design pattern? An idiom? Or should I  
> go with
> ugly whitness instances or with these 'some' named subclasses and just
> document things very carefully?

There's no standard way, certainly. You could annotate such axioms  
and then have tooling check the lhs for satisfiability...that might  
be reasonably minimal. You could also just check every LHS and RHS of  
an axiom for satisfiability (as a generalization of class  
satisfiabiilty checking).

Pushing to a service makes it weaker, i.e., the information that it  
*should* be unsat is out of band.

Cheers,
Bijan.

Received on Wednesday, 12 March 2008 21:36:53 UTC