Re: [OWL-S] Proposal for Making Progress on Process Modeling esp. Preconditons and Effects

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