- From: pat hayes <phayes@ihmc.us>
- Date: Thu, 15 Jan 2004 13:59:53 -0600
- To: Sheila McIlraith <sheila@cs.toronto.edu>
- Cc: Michael Kifer <kifer@cs.sunysb.edu>, Bijan Parsia <bparsia@isr.umd.edu>, public-sws-ig@w3.org
>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