Re: Expressiveness question

Hi Pat,


On Tue, 20 Jan 2004, pat hayes wrote:

> Hi Sheila
>
> >.....we are asking whether  we can axiomatize a situation
> >calculus [2] domain theory in SWRL.
>
> In a word, no.


We figured this! :)


> On the other hand, if were were to go into a bit more
> detail, maybe you could get something done in SWRL that would do a
> lot of what you want to do.
> .....


This is precisely what we were hoping for, together with intuitions
as to what would have to be added to SWRL to make this possible.
In a previous message, Drew McDermott pointed out the lack of
function symbols in SWRL as one problem.


> >To this end, the following is an example of an axiom we would like
> >to encode:
> >
> >Forall x. Forall s.
> >   holding(x,do(a,s)) iff
> >     [(a=pickup(x)) V (holding(x,s) & (a neq putdown(x))]
>
> The real killer here is the iff with a disjunction on one side of it.
> If we pick this apart, some of it fits into SWRL with a bit of work
> (never mind the foralls):
>
> (a=pickup(x)) OR (holding(x,s) AND (a neq putdown(x) )  IMPLIES
> holding(x, do(a,s))
>
> splits into two Horn clauses
>
> (a=pickup(x))  IMPLIES holding(x, do(a,s))
>
> (holding(x,s) AND (a neq putdown(x) )  IMPLIES holding(x, do(a,s))
>
> both of which can be got into SWRL with a bit of tweaking. (The
> equations and embedded terms would need to be made into relations.)
> The other way round, however, gives a non-Horn case:
>
> holding(x, do(a,s)) IMPLIES (a neq putdown(x) )
>
> is OK, but
>
> holding(x, do(a,s)) IMPLIES ((a=pickup(x)) OR (holding(x,s) )
>
> isn't, and isn't ever likely to be stateable in any rule language.


For the other direction, I get something a little different (partly
just rewriting what you have above), which is still non-Horn, but
makes the rules seem more intuitive.

holding(x, do(a,s)) AND NOT holding(x,s) IMPLIES a=pickup(x)

holding(x, do(a,s)) AND (a neq pickup(x)) IMPLIES (a neq putdown(x))


> Now, my instinct at this point is to ask you whether you really,
> really must have the full 'iff' here, or whether there might be a way
> in which you could live with some weaker way of using the effect of
> the back-implication. It is needed for the frame-problem-solving
> stuff which Ray's technique uses, but maybe you can instead treat
> that as an external constraint on an action application.


This sounds plausible.


> I have to
> say, personally I have never believed that genuine iff laws are
> really practical for realistic examples of action descriptions in any
> case: and there are other, alternative ways of handling the
> frame-style reasoning, even the use of circumscription-style
> reasoning if really necessary.

Well, I differ with you regarding whether iff's are practical,
but I guess we shouldn't tackle this issue here, or we'll descend
into the depths of your other ongoing thread on nomonotonic reasoning.

Let me simply say that these iff's have their origins in a
circumscription-based solution to the frame problem.  Indeed the iff
simply reflects the relationship between circumscription and predicate
completion for certain syntactically restricted theories.
These are generally realized using the completion semantics of
logic programs in Prolog or the like, and (to me at least) are
quite practical.


> Or, in the cases where you really
> require this kind of reasoning so as to use a GOLOG engine, maybe,
> you could code up suitable categories so as to avoid the explicit
> disjunctions, and connect them to the existing concepts by DL
> reasoning expressed in OWL (?? The only way to tell would be to see
> some more realistic examples of the kind of problems you are
> tackling.)

I've never thought about it that way.  Interesting.  I don't quite
see how this all falls together. Can you show me how I would encode the
problem I presented above using your DL strategy?

> Well, anyway, if you want an off-the-shelf answer, it has to be
> negative.  But we can give you about 75% of what you want, it seems.
> Maybe that will get you somewhere (?)

Thanks for the response, Pat.


Sheila


>
> Pat
>
> --
> ---------------------------------------------------------------------
> IHMC	(850)434 8903 or (650)494 3973   home
> 40 South Alcaniz St.	(850)202 4416   office
> Pensacola			(850)202 4440   fax
> FL 32501			(850)291 0667    cell
> phayes@ihmc.us       http://www.ihmc.us/users/phayes
>
> --
> [To unsubscribe to this list send an email to "majdart@bbn.com"
> with the following text in the BODY of the message "unsubscribe daml-process"]
>


Sheila McIlraith
Department of Computer Science
University of Toronto

Received on Sunday, 25 January 2004 18:02:10 UTC