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

>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.
>
>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.

Or something similar. Its not clear that you need 
full 2nd-order - FO plus recursion is probably 
somewhere in between 1st and 2nd -  and you 
certainly don't need it to use them 
constructively (which I think was your point 
also, right?).  SCL lets you *almost* define 
iteration or tail-recursion (you can't prove all 
of their meta-properties in the language) and it 
is strictly first-order. It does require a rather 
sexy unification algorithm, however, in order to 
handle sequence variables properly.

>  I think definition of like
>constructs would be 2nd order in any language. 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.

Tacky, IMO :-) and in any case this surely isn't 
a practical way to do reasoning unless k is kept 
rather small.  You can generalize this by 
allowing your FO language to contain numerals 
(think of them as a datatype) and having 'k' be 
schematic. Its still FO, as long as you never 
quantify over k inside another quantifier, but 
you don't need to have a single uniform limit.

Pat

>
>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
>>
>>
>>
>>
>>


-- 
---------------------------------------------------------------------
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

Received on Thursday, 15 January 2004 15:12:32 UTC