next up previous
Next: SCENARIOS Up: Composition rules and KL-structures Previous: Instantiated decomposition methods

Rule II

extends the definition of an IDM by assigning an instantiated method (IM) to one of its uninstantiated subtasks.

A. Constituents

tex2html_wrap_inline1327
tex2html_wrap_inline1329

B. Compatibility conditions

1. tex2html_wrap_inline1331

2. For every tex2html_wrap_inline1333 and partially instantiated input axiomgif in which tex2html_wrap_inline1191 arguments intervene it holds that either

a. tex2html_wrap_inline1339 , if the input axiom is of the form
tex2html_wrap_inline1335 ; or
b. tex2html_wrap_inline1343 , if the input axiom is of the form
tex2html_wrap_inline1345

C. Extended KL-structure

tex2html_wrap1397
instantiations tex2html_wrap_inline1349
import tex2html_wrap_inline1351
input axioms and program ofgif tex2html_wrap_inline1359

Example We describe one step in the construction of the instantiated decomposition method mechanical advise from a reusable KL-component (the generic decomposition method sequential execution, defined in section 2.1) and a simpler KL-structure (the instantiated resolution method identify hypothetical causes, defined above). In particular, we show how the instantiated method identify hypothetical causes is assigned to one of the uninstantiated subtasks, tex2html_wrap_inline1361 , of the instantiated decomposition method mechanical advise.

As we have shown already, the formal descriptions of KL-components and KL-structures can be formally manipulated by mathematical operations. Our composition rules constitute a particular type of such operations, which allow connecting, disconnecting and substituting KL-components and KL-structures within other KL-structures. There are also other types of operations, which can be used to generalize or specialize the formal descriptions of KL-components and KL-structures. We show below how a specialization operation can be applied to the generic decomposition method sequential execution (which handles an arbitrary number m of subtasks, see its definition in section 2.1), in order to make it fit into the binary task decomposition and arguments of the instantiated resolution method at hand.

First, the definition of sequential execution is specialized by setting the values of the parameters tex2html_wrap_inline1365 . We set tex2html_wrap_inline1367 , and tex2html_wrap_inline1369 . The formal description of the resulting specialized sequential execution decomposition method is as follows.

tex2html_wrap1243
predicates sequentialexecution
variables tex2html_wrap_inline1373
metavariables tex2html_wrap_inline1375
axioms tex2html_wrap_inline1377
program tex2html_wrap_inline1379
tex2html_wrap_inline1381
tex2html_wrap_inline1239

Then, the instantiated method identify hypothetical causes is assigned to the uninstantiated subtask, tex2html_wrap_inline1361 , of the specialized version of the decomposition method sequential execution, through the application of composition rule II.

A. Constituents

tex2html_wrap_inline1387

B. Compatibility Conditions

1. tex2html_wrap_inline1389
2. There are no instantiated input axioms yet.

C. Extended KL-structure

tex2html_wrap1401
instantiations tex2html_wrap_inline1393
import tex2html_wrap_inline1395


next up previous
Next: SCENARIOS Up: Composition rules and KL-structures Previous: Instantiated decomposition methods

jsierra@cs.stanford.edu