Reconfiguration

This scenario shows how the formal KL-model of a simple mechanical adviser software agent can be constructed from a set of reusable formal descriptions of KL-components (defined in the examples of section 2.1). Note that our composition rules can also be used to disconnect (substitute) KL-components or KL-structures from other KL-structures, i.e. to reconfigure formal KL-models.

We continue the process of building up KL-structures from KL-components and simpler KL-structures, initiated in section 2.2, until the construction of our mechanical adviser software agent is completed. See fig. 1 for a global overview of the configuration process. For each composition rule application, constituents, compatibility conditions, and formal description of the resulting extended KL-structure are shown below.

  
Figure 1: Configuration of a mechanical adviser software agent from a set of reusable formal descriptions of KL-components.

First, we describe the construction of the instantiated resolution method suggest observations from a set of reusable formal descriptions of KL-components (see their definitions in section 2.1). The model cause observations is connected to the second argument of the resolution method deduction, and an input relationship (formalized by an input axiom) is established between them through the following application of composition rule I.

A. Constituents

B. Compatibility Conditions

.

C. Extended KL-structure

import
use
axioms

Then, the model observations is connected to the third argument of the resolution method deduction, and an output relationship (formalized by an output axiom) is established between them through a second application of composition rule I.

A. Constituents

B. Compatibility Conditions

.

C. Extended KL-structure

import
use
axioms

Finally, composition rule II is applied to extend the definition of the instantiated decomposition method mechanical advise (constructed in section 2.2), by assigning the uninstantiated subtask, , of its constituent decomposition method sequential execution to the instantiated method suggest observations (constructed above). This second application of rule II shows how compatibility conditions concerning partially instantiated input axioms can be checked.

A. Constituents

B. Compatibility Conditions

1.
2. There is an input axiom partially instantiated by the previous application of rule II (section 2.2)

we have to check that , which in this case is trivial, .

C. Extended KL-structure

instantiations

import