- From: Michael Kifer <kifer@cs.sunysb.edu>
- Date: Fri, 16 Jan 2004 01:59:33 -0500
- To: Sheila McIlraith <sheila@cs.toronto.edu>
- Cc: public-sws-ig@w3.org
Sheila McIlraith <sheila@cs.toronto.edu> writes:
>
>
> On Thu, 15 Jan 2004, Michael Kifer wrote:
>
> > >>>>> "BP" == Message from Bijan Parsia <<bparsia@isr.umd.edu> > writes:
> >
> > BP> We're especially
> > BP> interested if people have *problems* with this approach.
> >
> > Situation calculus is not sufficient for process modeling. You need
> > something like Golog. But Golog is *second order*, not first order.
>
> I would not eliminate situation calculus/Golog for this reason.
>
> The situation calculus is actually second order -- one of the
> foundational axioms of the situation calculus is second
> order (the axiom that defines the branching structure of the tree
> of situations). This is used for proving formal properties. It's
> there because researchers took the time to axiomatize what situations
> look like so that they could prove properties of the system. There are
> theorems that show that reasoning can be done in a first-order subset of
> the theory. Also, domains are only axiomatized in first-order logic.
I was primarily trying to address two misconceptions that I thought were
lurking in Bijan's message:
1. That sitcalc is first-order
2. That "first-order" \equiv "good"
> Indeed, certain constructs in Golog are second order, but these are
> things like while loop constructs, or iteration. You need an induction
> axiom to define such constructs formally. I think definition of like
> constructs would be 2nd order in any language.
Maybe, but recursion can do the same thing in slightly different ways, and
for that you don't need second order.
> In work we did not
> semantic web services using Golog [1], we defined a restricted version of
> Golog where these type of constructs had a limit on the iteration "k", for
> some k. By doing this, while loop and iteration (with a k limit) now
> become first order.
But I suspect that the size of the first-order formula somehow depends on
k. Does it?
--michael
> Sheila
>
>
> [1] McIlraith, S. and Son, T. ``Adapting Golog for Composition of Semantic
> Web Services''. Proceedings of the Eighth International Conference on
> Knowledge Representation and Reasoning (KR2002), pages 482-493, April,
> 2002.
>
> >
> > I believe that Concurrent Transaction Logic satisfies your needs and fits
> > the intuition that Mark had (but couldn't express :-). It is also
> > first-order unless you need default negation.
> >
> > But I also believe that at some level process modeling requires defaults
> > as Benjamin argued in
> > http://ebusiness.mit.edu/bgrosof/paps/beyond-mon-inh-wking-pap-081603.pdf
> >
> >
> > --michael
> >
> >
> >
> > BP> This is to fulfill an action item on me. (I hate those pesky things.)
> >
> > BP> In our last telecon, we discussed a proposal from Mark Burstein for
> > BP> ripping bits of the Semantic Web Rule Language (SWRL, ne้ OWL Rules)
> > BP> proposal and plopping them into OWL KBs that would purport to represent
> > BP> Process Models, in particular, the preconditions and effects of
> > BP> specific processes.
> >
> > BP> In essence, the proposal relies on hanging sets of SWRL Atoms
> > BP> (potentially with variables) off of a property attached to a
> > BP> Process-as-Instance. This would require some sort of Atom quoting
> > BP> mechanism (either reification (Mark's pick), or literals (my pick)),
> > BP> and providing some semantics for these constructs (which would *not* be
> > BP> SWRLy). This was inspired by Drew McDermott's DRS encoding of logical
> > BP> formulas in RDF (or perhaps an attempt to make DRS all SWRLy).
> >
> > BP> In discussion, a number of issues arose, including whether we wanted to
> > BP> "make up our own" language in this way, or see whether SWRL (or a
> > BP> likely RDF Rules) could do the job, perhaps with some extension. If we
> > BP> could identify those extensions, then we could present them to the
> > BP> various groups as requirements.
> >
> > BP> After some discussion (particularly about how to handle delete lists in
> > BP> OWL), we decided that what we knew we knew how to do was encode OWL-S
> > BP> process models in the situation calculus[1]. We also decided to go for
> > BP> a first-order axiomatization (over, say, a non-monotonic one), partly
> > BP> so we could build on SWRL/OWL-Rules, but for an number of other reasons
> > BP> (prior work, familiarity, connection to other efforts such as PSL).
> > BP> Sheila McIlraith put forth the following justification:
> >
> > >> In my mind, the reason for the first-order axiomatization is because I
> > >> view the process model as a specification, and I think it (as a
> > >> specification) should have a "stardard" model-theoretic semantics,
> > >> rather
> > >> than a nonmonotonic interpretation. This enables people who use
> > >> different
> > >> forms of reasoners (monotonic or nonmonotonic) to easily understand
> > >> how to
> > >> map the specification into their implementations.
> >
> > BP> We do intend to produce a mapping from this axiomatization to a
> > BP> non-monotonic one, for implementation purposes. Sheila elaborates:
> >
> > >> In particular, in the situation calculus, the solution to the frame
> > >> problem (encoding that everything stays the same unless it is
> > >> explicitly
> > >> changed by the execution of a process) is encoded using
> > >> "if-and-only-if"
> > >> (iff) axioms. These axioms are easily translated to "if" rules in a
> > >> logic
> > >> programming (i.e., nonmonotonic) reasoner. The completion semantics
> > >> of the logic program ensures that the interpretations of the logic
> > >> program
> > >> are identical to the interpretations of the original first-order
> > >> axiomatization. See [2] for details.
> > >>
> > >> E.g., the first-order logic axiom
> > >> Forall a,s.holding(cup, do(a,s)) iff a=pickup(x)
> > >>
> > >> is translated into the following logic programming rule
> > >> Forall a,s.holding(cup, do(a,x)) <- a=pickup(x)
> > >>
> > >> The interpretation is equivalent.
> >
> > BP> So, we have two classes of issue:
> > BP> 1) How much do we have to add to SWRL to get a language that a) can
> > BP> handle sitcalc and b) is otherwise sufficient?
> > BP> 2) Is the sitcalc the right way to go? What exactly will be it's
> > BP> point? (Sheila has given (some of) her view above. We're especially
> > BP> interested if people have *problems* with this approach.)
> >
> > BP> (Actually, there are other sets of issues, such as it's not clear how
> > BP> to allow full OWL expressiveness into the precondition and effect
> > BP> lists, and thus how to smoothly integrate process descriptions with
> > BP> what one would expect to be the common ontologies and knowledge bases
> > BP> on the Semantic Web. I expect these'll all emerge in subsequent
> > BP> discussion ;))
> >
> > BP> Cheers,
> > BP> Bijan Parsia.
> >
> >
> > BP> [1] Srini Narayanan & Sheila McIlraith , "Simulation, Verification
> > BP> and Automated Composition of Web Services"
> > BP> http://citeseer.nj.nec.com/narayanan02simulation.html
> >
> > BP> This gives a sitcalc based semantics to an earlier version of OWL-S
> > BP> (ne้ DAML-S). This representation has been used subsequently to provide
> > BP> translations to other formalisms and ontologies (e.g., SHOP2, PSL[5],
> > BP> and others).
> >
> > BP> [2] Raymond Reiter 2001 {\it Knowledge in Action: Logical Foundations
> > BP> for
> > BP> Specifying and Implementing Dynamical Systems.} Cambridge, Mass.: The
> > BP> MIT Press
> >
> > BP> [3] OWL-S 1.0:
> > BP> http://www.daml.org/services/owl-s/1.0/
> >
> > BP> [4] SWRL:
> > BP> http://www.daml.org/2003/11/swrl/
> >
> > BP> [5] Michael Gruninger, "Applications of PSL to Semantic Web Services"
> >
> > BP> http://www.cs.uic.edu/~ifc/SWDB/papers/Gruninger.pdf
> >
> >
> >
> >
> >
>
>
>
Received on Friday, 16 January 2004 01:58:59 UTC