> ` jbjb dd7666^&u&u&u8^uJv^_TZwwwww///"$$$$$$,RP6/;~///P66wwM:/6w6w"J.0"
066/"j66"Nwy&uf
"#<_("6^^DL]^^]The Ontological Stance for a Manufacturing Scenario
Michael Gruninger
Department of Mechanical and Industrial Engineering
University of Toronto
5 Kings College Road
Toronto, Ontario, Canada M5S 3G8
Phone: 416-946-8853
Fax:416-978-7753
gruninger@mie.utoronto.ca
Abstract:
The semantic integration of software systems can be supported through a shared understanding of the terminology in their respective ontologies. In practice, however, we are faced with the additional challenge that few applications have an explicitly axiomatized ontology. To address this challenge, we adopt the Ontological Stance, in which we can model a software application as if it were an inference system with an axiomatized ontology, and use this ontology to predict the set of sentences that the inference system determines to be entailed or satisfiable. We give an overview of a deployment of the Process Specification Language (PSL) Ontology as the interchange ontology for the semantic integration of three manufacturing software applications currently being used in industry -- a process modeller, a process planner, and a scheduler.
Keywords: ontologies, semantic integration, semantic mappings, translation definitions
The Ontological Stance for a Manufacturing Scenario
Michael Gruninger
Department of Mechanical and Industrial Engineering
University of Toronto
gruninger@mie.utoronto.ca
Abstract:
The semantic integration of software systems can be supported through a shared understanding of the terminology in their respective ontologies. In practice, however, we are faced with the additional challenge that few applications have an explicitly axiomatized ontology. To address this challenge, we adopt the Ontological Stance, in which we can model a software application as if it were an inference system with an axiomatized ontology, and use this ontology to predict the set of sentences that the inference system determines to be entailed or satisfiable. This chapter gives an overview of a deployment of the Process Specification Language (PSL) Ontology as the interchange ontology for the semantic integration of three manufacturing software applications currently being used in industry -- a process modeller, a process planner, and a scheduler.
Motivation MOTIVATION
The necessity for software applications to interoperate has become crucial to the conduct of business and operations in organizations. In practice, however, interoperability is difficult to achieve, since each of these applications utilizes information in a different way, and the knowledge representation formalisms inherent to these applications are also differentdiffer. In particular, existing approaches to interoperability lack an adequate specification of the semantics of the terminology used by the software applications, which leads to inconsistent interpretations and uses of knowledge.
The development of ontologies has been proposed as a key technology to support semantic integration. Ontologies are logical theories that provide a set of terms together with a computer-interpretable specification of the meanings of the terms in some formal logical language. In this way, we can support the semantic integration of software systems through a shared understanding of the terminology in their respective ontologies, in the sense that a semantics-preserving exchange of information between ontologies requires mappings between logically equivalent concepts in each ontology. The challenge of semantic integration is therefore equivalent to the problem of generating such mappings, determining that they are correct, and providing a vehicle for executing the mappings, thus translating terms from one ontology into another. The emphasis in this paper will be on the verification of the correctness and completeness of semantic mappings rather than on the specification of the mappings (as in (Giunchiglia et al 2007), (Kalfoglou and Schorlemmer 2003)).
In practice, we are faced with the additional challenge that almost no application hasfew applications have an explicitly axiomatized ontology. To address this challenge, we adopt the Ontological Stance, in which we can model a software application as if it were an inference system with an axiomatized ontology, and use this ontology to predict the set of sentences that the inference system determines to be entailed or satisfiable.
In the first part of this paper, we discuss a set of sufficient conditions that a neutral interchange ontology must satisfy in order to support this approach to the generation and validation of semantic mappings. In the second part of the paper we give an overview of a deployment of the Process Specification Language (PSL) Ontology as the interchange ontology for the semantic integration of three manufacturing software applications currently being used in industry -- a process modeller, a process planner, and a scheduler. The semantic mappings between the applications' ontologies and PSL are semi-automatically generated from invariants (properties of models preserved by isomorphism) and verified prior to integration. The correctness of the application ontologies are validated using the notion of the Ontological Stance.
FORMALIZATION OF SEMANTIC INTEGRATIONFormalization of Semantic Integration
When software applications communicate with each other, there needs to be some way to ensure that the meaning of what one application accepts as input and output is accurately conveyed to the other application. Since the applications may not use the same terms to mean the same thingsconcepts, we need a way for an application to discover what another application means when it communicates. In order for this to happen, every application needs to publicly declare exactly what terms it is using and what these terms mean; this specification is commonly referred to as the applications ontology. Moreover, this specification must be accessible to other software applications. Thus, we require that the meaning be encoded in a formal language, which enables a given application to use automated reasoning to accurately determine the meaning of other applications terms. For example, if application 1 sends a message to application 2, then along with this message is a pointer to application 1s ontology. Application 2 can look in application 1's ontology to see what the terms mean, the message is successfully communicated and the applications task is successfully performed. Complete understanding will occur between the applications only if they share the semantics of all the terminology used in the content of the messages that they exchange or the information sources that they access.
We can therefore say that two software applications will be interoperable if they share the semantics of the terminology in their corresponding ontologies. Sharing semantics between applications is equivalent to sharing models of their ontologies; two ontologies are equivalent if they have isomorphic sets of models. Nevertheless, applications do not explicitly share the models of their theories; instead, they exchange sentences in such a way that the semantics of the terminology of these sentences is preserved.
Formally, we will say that an ontology TA is sharable with an ontology TB if for any sentence A in the language of TA, there exists an exchange that maps to a sentence B such that there is a one-to-one mapping between the set of models of TA that satisfy A and the set of models of TB that satisfy B. We will say that a theory TA is interoperable with a theory TB if any sentence that is provable from TA, there exists an exchange that maps to a sentence that is provable from TB. We make the following hypothesis assumption to restrict our attention to domains in which sharability and interoperability are equivalent:
Interoperability HypothesisAssumption
We are considering interoperability among software applications that are equivalent to complete first-order inference engines that exchange first-order sentences.
The soundness and completeness of first-order logic guarantees that the theorems of a deductive inference engine are exactly those sentences which are satisfied by all models, and that any truth assignment given by a consistency checker is isomorphic to a model. If we move beyond the expressiveness of first-order logic, we lose completeness, so that, for any deductive inference engine there will be sentences that are entailed by a set of models but which are not provable by that engine. We could therefore have two ontologies that are sharable but not interoperable.
VERIFIED ONTOLOGIESVerified Ontologies
For applications to completely understand each other, we require that all of the terms that one application uses are completely understood by the other application. From one applications perspective, the actual meaning of the terms is exactly what is specified by the axioms in the other applications ontology. It cannot know what was in the mind of the human who designed the applications ontology. For successful understanding to take place, this actual meaning of a term has to be the same as the meaning that was intended by the designer of the applications ontology. For convenience instead of the cumbersome phrase: the meaning that was intended by the designer of the applications ontology, we will simply say the intended semantics of the applications ontology. Thus, to achieve complete semantic integration, we need to enable the automated exchange of information between applications in such a way that the intended semantics of the applications ontologies are preserved by the receiving application.
The challenge here is to guarantee that the intended semantics of an ontology is equivalent to the actual semantics of the ontology. The actual semantics is defined by the axioms of the ontology in conjunction with the semantics of the ontology representation language. We must therefore explore the ramifications of explicit formally specified semantics and the requirements that this approach imposes on both the ontology designer as well as the application designer. We need to characterize the relationship between the intended semantics of an applications terminology and the actual semantics of the applications ontology that must hold to support complete semantic integration.
An additional problem is that we cannot directly access the intended semantics of an applications terminology. We can however examine the behavior of the application; this is completely dependent on the inferences it makes, which in turn is completely dependent on the semantics of its axioms. In effect, an applications behavior is constrained by the semantics of its ontology, because any inferences made by the application must conform to the semantics of its internal knowledge together with any information acquired by the application from the environment or other applications. If an application does not do the right thing, or retrieve the right information, or make correct inferences, then it does not share its semantics with other applications. So, while we cannot peek inside an application to directly examine its semantics, we can observe what it does, and infer information about the semantics of the applications terminology.
In this operational characterization of semantics, we must make the link between inference and the semantics of the applications ontology. An applications behavior is characterized by the inferences that it makes, that is, the sentences that can be deduced from its knowledge or the sentences that are consistent with its knowledge. Remember that with a formal ontology, the applications knowledge is specified as a theory, so that a sentence is consistent if there exists a model of the theory that satisfies the sentence and that a sentence can be deduced if it is satisfied by all models of the theory. Therefore, the applications behavior (and hence the semantics of the applications terminology) can be characterized by this implicit set of models, which we will call the set of intended models.
Given this framework, we can say that two applications completely share semantics if their sets of intended models are equivalent. However, applications cannot exchange the models themselves they can only exchange sentences in the formal language that they use to represent their knowledge. We must be able to guarantee that the inferences made with sentences exchanged in this way are equivalent to the inferences made with respect to the applications intended models given some input the application uses these intended models to infer the correct output.
We can use this characterization to evaluate the adequacy of the applications ontology with respect to these intended models. We will say that an ontology is verified if and only if the set of models of the axioms of the ontology is equal to the set of intended models for the applications terminology.
SHAPE \* MERGEFORMAT
Figure 1: Methodology for the evaluation of ontologies.Figure 1: Methodology for the evaluation of ontologies.
Once we have specified the class of structures M and characterized it up to isomorphism, we can formally evaluate an ontology with respect to this specification. In particular, we want to prove two fundamental properties:
Satisfiability: every structure in the class M is a model of the ontology.
Axiomatizability: every model of the ontology is elementary equivalent to some structure in the classM.
Strictly speaking, weWe only need to show that a model exists in order to demonstrate that a theory is satisfiable. However, but, in the axiomatization of domain theories, we need a complete characterization of the possible models. For example, since we are considering the domain of activities, occurrences, and timepoints, to show that a theory is satisfiable, we need only specify an occurrence of an activity which together with the axioms are satisfied by some structure. The problem with this approach is that we run the risk of having demonstrated satisfiability only for some restricted class of activities. For example, a theory of activities that supports scheduling may be shown to be consistent by constructing a satisfying interpretation, but the interpretation may require that resources cannot be shared by multiple activities or it may require all activities to be deterministic. Although such a model may be adequate for such activities, it would in no way be general enough for our purposes. We want to propose a comprehensive theory of activities, so we need to explicitly characterize the classes of activities, timepoints, objects, and other assumptions that are guaranteed to be satisfied by the specified structures.
Note that we are not imposing the requirement that the ontologies themselves be categorical or even complete. The two applications must simply share the same set of models (up to isomorphism). Ambiguity does not arise from the existence of multiple models for an ontology it arises because the two applications have nonisomorphic models, that is, the ontology for application A has a model that is not isomorphic to any model for the ontology of application B.
The purpose of the Axiomatizability Theorem property is to demonstrate that there do not exist any unintended models of the theory, that is, any models that are not specified in the class of structures. By the Interoperability Hypothesis, we do not need to restrict ourselves to elementary classes of structures when we are axiomatizing an ontology. Since the applications are equivalent to first-order inference engines, they cannot distinguish between structures that are elementarily equivalent. Thus, the unintended models are only those that are not elementarily equivalent to any model in the class of structures. By the Interoperability Hypothesis, this is equivalent to saying that every sentence that is provable from the axioms of the ontology is also an inference that the application makes, and conversely, every inference that the application makes is provable from the axioms of the ontology.
These properties of an ontology allow us to make the claim that any inferences drawn by the application using the ontology are faithful to the applications semantics. If an ontology is not verified, then it is possible to find sentences that the application infers based on its intended models, but which are not provable from the axioms of the ontology. For example, automated inference cannot be used to determine that two applications can in fact be completely semantically integrated. In the next section, we will consider in some detail the challenges that must be addressed in achieving semantic integration with unverified ontologies.
It may seem unreasonable to require that verified ontologies be used for complete semantic integration. Unverified ontologies allow for the existence of unintended models that are a potential source of semantic heterogeneity; the critical question is to determine whether or not they prevent semantic integration in a particular application. One may take heuristic approaches in which the applications only need to match their semantics well enough to make good enough decisions based on the information exchanged; however, such approaches implicitly assume metrics for integration, and these metrics arise by considering the possibly unintended models that are allowed by unverified ontologies.
Through the Satisfiability and Axiomatizability Theorems, verified ontologies characterize the relationship between the intended models for the ontology and the actual models of the ontologys axiomatization. This does not address the relationship between the intended models and the original intuitions of the user; it is possible that an ontology can be verified yet the intended models do not correspond to models of the user. What is needed is a methodology for validating the ontology.
THE ONTOLOGICAL STANCE The Ontological Stance
When integrating software applications, we are faced with the additional challenge that almost no application has an explicitly axiomatized ontology. Nevertheless, we can model a software application as if it were an inference system with an axiomatized ontology, and use this ontology to predict the set of sentences that the inference system decides to be satisfiable. This is the Ontological Stance (Gruninger and Menzel 2003), and is analogous to the intentional stance (Dennet 87), which is the strategy of interpreting the behavior of an entity by treating it as if it were a rational agent who performs activities in accordance with some set of intentional constraints.
The Ontological Stance is an operational characterization of the set of intended models for the application's terminology. In this sense, it can be treated as a semantic constraint on the application. It does not directly postulate a specific set of axioms, but rather a set of intended models:
Given an application A, there exists a class of models MA such that any sentence is decided by A to be satisfiable iff there exists M in MA such that M entails .
The ontology of an application can be evaluated with respect to this set of intended models, just as the methodology proposed in the preceding section can be used to evaluate verified ontologies.
The Ontological Stance also addresses the relationship between the intuitions and the intended models; this is, of course, informal, but we can consider the domain intuitions as providing a physical interpretation of the intended models. In this sense, we can adopt an experimental or empirical approach to the evaluation of the class of intended models in which we attempt to falsify these models. If we can find some objects or behaviours within the domain that do not correspond to an intended model, then we have provided a counterexample to the class of model. In response, we can either redefine the scope of the class of models (i.e. we do not include the behaviour within the characterization of the models) or we can modify the definition of the class of models so that they capture the new behaviour.
It is important to realize that the Ontological Stance is not a methodology for specifying semantic mappings between ontologies, nor is it a methodology for designing ontologies for software applications; but rather, it is used to evaluate the correctness and completeness of the any proposed application ontology.
SHAPE \* MERGEFORMAT
Figure 2: Figure 2: We can model a software application as if it were an inference system with a formal ontology, and use this ontology to predict the set of sentences that the inference system decides to be entailed or satisfiable.
DOMAIN THEORIES AND ONTOLOGIES Domain Theories and Ontologies
Although we consider semantic integration from the perspective of the relationship between ontologies, we must be careful to distinguish the ontologies from the domain theories that use them. For example, if two software applications both used an ontology for algebraic fields, they would not exchange new definitions, but rather they would exchange domain theories that consist of sentences that expressed properties of elements in their models. For algebraic fields, such sentences are equivalent to polynomials. Similarly, the software applications that use a process ontology do not exchange arbitrary sentences, such as new axioms or even conservative definitions, in the language of their ontology. Instead, they exchange process descriptions, which are sentences that are satisfied by particular activities, occurrences, states, or other objects.
An n-type for a theory is a consistent set of formulae (each of which has n free variables) that is satisfied by a model of the theory. Domain theories for an ontology are Boolean combinations of n-types that are realized by some model of the ontology. In the algebra example, polynomials are n-types for elements in an algebraic field. In PSL Ontology (Gruninger 2003), formulae that specify the constraints under which subactivities of an activity occur are types for complex activities. In the axiomatization of situation calculus in (Reiter 2001), precondition and effect axioms are types for actions.
This distinction between ontologies and their domain theories has important consequences for semantic integration. Both the inputs and outputs of a software application are axiomatized as domain theories. In the context of the Ontological Stance, we never actually ``see the application ontology, but we can verify that the axiomatization of the inputs and the outputs of the application are the types of elements that are realized in models of the application ontology.
Given a model M, we say that Th(M) is the first-order theory of M, that is, the set of sentences that are entailed by M. A domain theory for an ontology T is a subtheory of Th(M) for some model of T. Using this approach, domain theories can also be considered to be axiomatizations of specific models of an ontology. As a result, we can use the domain theories that are either the inputs or outputs of a software application to represent the intended models that are otherwise implicit.
VALIDATING APPLICATION ONTOLOGIES
If a software application already has an ontology, then the Ontological Stance can be used to evaluate the ontology with respect to the applications intended models. This is distinct from the methodology proposed in the preceding section can be used to evaluate verified ontologies. Even if an application ontology is verified (so that we have a complete characterization of all models of the ontologys axiomatization), the models of the ontology may not be intended models. Using the Ontological Stance, if the models of the application ontology are not equivalent to the intended models, then there are two possibilities.
In the first case, the application ontology is incorrect since the axioms have unintended models. We can formalize this in two ways:
There exists a model M of the ontologys axioms T that is not an intended model.
The intended models entail some sentence that is not entailed by the axioms T.
In the second case, the application ontology is incomplete since there are intended models that do not satisfy the axioms. This can also be formalized in two ways
There exists an intended model M that does not satisfy the axioms of T
The intended models do not entail the axioms of T.
We consider two alternative formalizations because they each give rise to a different set of techniques for evaluation of the application ontology. We can either search for a model (either an intended model or a model of the axioms) that has certain properties, or we can search for a sentence that is supposed to be entailed by either the intended models or the models of the axioms.
Following the discussion of the preceding section, we can use domain theories to axiomatize specific models of the ontology. Thus, rather than search for models with certain properties, we are actually searching for domain theories with the corresponding properties. In regards to application ontologies, domain theories are equivalent to the possible inputs and outputs of the software application.
The second kind of formalization corresponds to the notion of competency questions (Gruninger and Fox 1995), which are classes of queries used to characterize the adequacy of an ontology to support a set of tasks, such as decision support, search, or semantic integration. Essentially, the sentences that are entailed by intended models are competency questions for the application ontologies.
The above conditions can also be rephrased in a more positive way by stating analogues of the Satisfiability and Axiomatizability theorems for verified ontologies. We will say that an application ontology is correct iff any sentence that is entailed by the axioms T is also satisfied by all intended models. We will say that an ontology is relatively complete iff any sentence that is satisfied by all intended models is also entailed by the axioms T. We will say that an application ontology is validated if it is both correct and relatively complete with respect to the intended models of the application.
AXIOMATIZING APPLICATION ONTOLOGIES Validating Application Ontologies
A semantics-preserving exchange of information means that there are mappings between logically equivalent concepts in each ontology. The challenge of semantic integration is therefore equivalent to the problem of generating such mappings, determining that they are correct, and providing a vehicle for executing the mappings, thus translating terms from one ontology into another.
In cases where the software applications do not have explicit ontologies, existing techniques for generating semantic mappings to achieve integration are not applicable. In addition, current work on semantic mapping addresses the generation of semantic mappings between axiomatized ontologies, but they do not emphasize the evaluation of the correctness of the mappings.
One can, of course, axiomatize the application ontologies before specifying mappings between them. Alternatively, we can use an existing mediating ontology as the basis for the axiomatization for the application ontologies; this approach has the advantage that the axioms in the mediating ontology can also play the role of semantic mappings between the application ontologies.
This raises one seemingly obvious question -- what is the terminology whose intended interpretations are being axiomatized? In the methodology of the Ontological Stance, we only focus on the terms that are used in the specification of inputs and outputs; we do not provide axioms for any terms that arise from internal data structures. This technique arises from the demands of semantic interoperability scenarios, in which it is the ambiguity in the sentences exchanged between software applications that cause problems. Communication between software applications consists of their input and outputs, and not their internal data structures.
Translation definitions (Gruninger and Kopena 2004) were originally proposed to specify the semantic mappings between the mediating ontology and application ontologies. Translation definitions have a special syntactic form---they are biconditionals in which the antecedent is a class in the application ontology and the consequent is a formula that uses only the lexicon of the mediating ontology. We can also use translation definitions as the axiomatization of the intended models of the software applications ontology.
We can axiomatize the intended semantics of the terminology that a software application uses to specify its input and output sentences by writing sentences that are conservative definitions of the terminology. In other words, all of the axioms in the application ontology will have the syntactic form
(forall (x1 xn)
(iff (appi x1 xn)
( x1 & xn)))
where appi is an n-ary relation in the lexicon of the application ontology and is a sentence in the language of the mediating ontology. Such sentences have the same syntactic form as translation definitions.
The generation of axioms through the specification of invariant values for models has been implemented in the PSL project's Twenty Questions mapping tool. By guiding and supporting users in creating translation definitions without requiring them to work directly with first order logic, the Twenty Questions tool provides a semi-automated technique for creating axioms. It also captures the application's set of intended models, since the translation definitions generated by the tool together with the mediating ontology define an explicit axiomatization of the application's previously implicit ontology.
Achieving complete semantic integration with this architecture makes several rather strong assumptions. First, the interlingua ontology must be verified. If it is not, then there is no guarantee that the mapping rules are faithfully capturing the intended models of the application ontologies. Thus, that even if it is possible in principle to preserve semantics directly between the application ontologies, the mapping rules will fail to guarantee semantic integration, even though it is logically possible.
The interesting aspect of this architectureapproach is that complete semantic integration does not assume that thealso works in the case where the application ontologies themselvesexist but they are not verified; however, it does require that models of the application ontology together with the semantic mappingstranslation definitions are equivalent to the intended models of the application. In other words, even though there exist unintended models of the application ontologys axioms, if the interlinguamediating ontology is powerful enough, then it can be used to augment the application ontology so that it is verified. In this way, the translation definitions eliminate the unintended models of the application ontology.
Axiomatizing the intended models of the application ontologies requires that the mediating ontology be verified. If it is not, then there is no guarantee that the translation definitions are faithfully capturing the intended models of the application ontologies. Thus, even if it is possible in principle to preserve semantics directly between the application ontologies, the translation definitions will fail to guarantee semantic integration, even though it is logically possible.If on the other hand, the application ontologies are verified, this is not enough to guarantee complete semantic integration. We must in addition, assume that they are conformant with the interlingua ontology. That is, every model of an application ontology can be interpreted within a model of the interlingua ontology. Intuitively, this is related to the intuition that the application and interlingua ontologies cover the same set of concepts.
It is possible that the intended models of the application ontology are definable in the mediating ontology, but the translation definitions are incorrect. In such a case, the translation definitions that axiomatize the application ontologies can be validated using the Ontological Stance. Translation definitions (Gruninger and Kopena 2004) specify the semantic mappings between the interlingua ontology and application ontologies. Translation definitions have a special syntactic form---they are biconditionals in which the antecedent is a class in the application ontology and the consequent is a formula that uses only the lexicon of the interlingua ontology. In fact, one can consider the translation definitions to be the axiomatization of the intended models of the software applications ontology.
The generation of semantic mappings through the specification of invariant values has been implemented in the PSL project's Twenty Questions mapping tool . By guiding and supporting users in creating translation definitions without requiring them to work directly with first order logic axiomatizations, the Twenty Questions tool provides a semi-automated technique for creating semantic mappings. It also captures the application's set of intended models, since the translation definitions generated by the tool together with the interlingua ontology define an explicit axiomatization of the application's previously implicit ontology.
If the application ontologies are axiomatized, then the semantic mappings can be verified by proving that they do indeed preserve the models of the ontologies; otherwise, the correctness of the mappings between an application ontology and the interlingua ontology are evaluated using the methodology of the Ontological Stance. This can be done by demonstrating that the class of models of the application ontology is are axiomatized by the interlinguamediating ontology together with the translation definitions. To verify this axiomatization of the application ontology, the generated translation definitions may be treated as falsifiable hypotheses and tested empirically. By the Ontological Stance, the application decides some sentence to be provable iff the translation definitions and interlinguamediating ontology entails . In this way, it may be evaluated whether or not the attributed ontology correctly predicts inferences made by the software, and consequently whether or not the translation definitions accurately capture the semantics of the application.
One potential problem with this approach is that there may be cases in which the intended models of the application ontology are not definable in the mediating ontology. Intuitively, this is equivalent to the case in which the mediating ontology is not expressive enough to capture all of the concepts in the application ontology.
MANUFACTURING INTEROPERABILITY SCENARIO Manufacturing Interoperability Scenario
In this section, we present the use of an interlingua ontology (the Process Specification Language) for the axiomatization of the ontologies of a set of manufacturing software applications (ILOG Scheduler, SAP ERP data model, and the process planning software MetCAPP). None of the software applications in the scenario had a pre-existing axiomatized ontology. For each of the software applications, we consider a subset of the translation definitions (written using the Common Logic Interchange Format, as specified ISO/IEC JTC 1/SC 32 (2005) ISO/WD 24707 -- Common Logic -- Framework for a family of logic-based languages)) that axiomatize the intended models of the application ontology and discuss how the Ontological Stance was used to evaluate the correctness and completeness of the definitions. This scenario also provides a validation of the PSL Ontology, in the sense that it demonstrates that it is sufficiently strong to specify definable interpretations of the application ontologies.
Semantic Mappings
A semantics-preserving exchange of information means that there are mappings between logically equivalent concepts in each ontology. The challenge of semantic integration is therefore equivalent to the problem of generating such mappings, determining that they are correct, and providing a vehicle for executing the mappings, thus translating terms from one ontology into another.
The approach used in the scenario is known as the Interlingua architecture for semantic mapping. Its distinguishing feature is the existence of a mediating ontology that is independent of the applications ontologies, and which is used as a neutral interchange ontology (Ciociou et al 2001). The semantic mappings between application and interlingua ontology are manually generated and verified prior to application interaction time (Schlenof et al. 1999). This process of creating the mapping between the application ontology and the interlingua ontology is identical to the process of creating a mapping directly between two application ontologies. As such, we can consider the application ontologies to be integrated with the interlingua ontology.
This architecture is much more powerful than specifying direct mappings between application ontologies. We only need to specify one mapping for each application ontology, whereas the direct mapping approach requires a semantic mapping for each pair of application ontologies, making the creation and maintenance of mappings becomes unmanageable. The existence of the pre-defined mappings between the application ontologies and the interlingua ontology enables the automatic generation of the point-to-point mapping between the applications ontologies. If one applications ontology changes, then only one mapping need be affected, rather than one for each application. New applications can subscribe to the community of applications using this interlingua merely by creating a mapping to and from the interlingua. With no changes to their own mappings, all other applications now can translate between their ontology, and the new applications ontology. This was not possible in the manual mapping case because every point to point mapping has to be pre-specified.
Semantic mappings can be expressed as formal definitions or rules between application ontologies and interlingua ontologies. In the interlingua approach, there are two steps in translation: the execution of the mapping from the application ontology to the interlingua, and from the interlingua to the other applications ontology. The translation can be accomplished by applying deduction to the axioms of the interlingua ontology and the formal mapping rules. If these rules have already been verified to preserve semantics between the application and interlingua ontologies, we are guaranteed that translation between the applications also preserves semantics. In effect, a direct mapping rule from one applications ontology to the other applications ontology is inferred from the two separate rules. If run-time translation efficiency is important, then the point to point mapping rules could be cached as explicit rules; otherwise they need only be implicit. When they are implicit, then the otherwise distinct processes of creating and executing a mapping is conflated it happens at the same time, rather than being two separate steps.
If the application ontologies are axiomatized, then the semantic mappings can be verified by proving that they do indeed preserve the models of the ontologies. If the application ontologies have been axiomatized as definitional extensions of a mediating ontology, then the direct semantic mappings between different application ontologies are sentences that are entailed by the application ontologies.
SHAPE \* MERGEFORMAT
Figure 3: Semantic integration using an interlingua ontology. The thin arrows represent manually generated mappings created by the application designers prior to application integration. The thick arrows represent the [possibly implicit] application-to-application mapping that is automatically generated.
Process Specification Language
The Process Specification Language (PSL) (Bock and Gruninger 2005; Gruninger and Menzel 2003; Schlenoff et al. 1999) has been designed to facilitate correct and complete exchange of process information. information. The primary purpose of PSL is to enable the semantic interoperability of manufacturing process descriptions between manufacturing engineering and business software applications such as process planning, scheduling, workflow, and project management. Additional applications of PSL include business process design and analysis, the implementation of business processes as web services, and enterprise modelling. PSL has been published as an International Standard (ISO 18629) within the International Organisation of Standardisation. The full set of axioms in the Common Logic Interchange Format is available at http://www.mel.nist.gov/psl/ontology.html.
The PSL Ontology is a modular set of theories in the language of first-order logic. All core theories within the ontology are consistent extensions of a theory referred to as PSL-Core, which introduces the basic ontological commitment to a domain of activities, activity occurrences, timepoints, and objects that participate in activities. Additional core theories capture the basic intuitions for the composition of activities, and the relationship between the occurrence of a complex activity and occurrences of its subactivities.
The PSL Ontology is verified the models of all core theories within the ontology have been characterized, and the Satisfiability and Axiomatizability theorems have been proven for these theories. A fundamental structure within the models of the axioms of the PSL Ontology is the occurrence tree, whose branches are equivalent to all discrete sequences of occurrences of atomic activities in the domain. The basic structure that characterises occurrences of complex activities within models of the ontology is the activity tree, which is a subtree of the legal occurrence tree that consists of all possible sequences of atomic subactivity occurrences; the relation (root ?s ?a) denotes that the subactivity occurrence s is the root of an activity tree for the activity a. Elements of the tree are ordered by the min_precedes relation; each branch of an activity tree is a linearly ordered set of occurrences of subactivities of the complex activity. In addition, there is a one-to-one correspondence between occurrences of complex activities and branches of the associated activity trees.
The fundamental intuition in the ontology of process plans is the notion of a partial ordering that is embedded within the activity trees of a complex activity. Different classes of process plans are defined by characterising the relationship between the partial ordering and the set of possible occurrences of a process plan.
Three new relations are introduced to specify the relationship between the partial ordering (referred to as the subactivity occurrence ordering) and the activity tree. The relation (soo ?s ?a) denotes that the activity occurrence s is an element of the subactivity occurrence ordering for the activity a. The relation (soo_precedes ?s1 ?s2 a) captures the ordering over the elements.
There are three basic classes of process plans, each of which impose different occurrence constraints on the elements of the partial ordering:
strong poset activities, in which there is a one-to-one correspondence between branches of the activity tree and the linear extensions of the partial ordering;
choice poset activities, in which there is a one-to-one correspondence between branches of the activity tree and the maximal chains in the partial ordering;
complex poset activities, each of which is the union of the strong poset activities corresponding to a set of linear extensions for suborderings of the partial ordering.
Two relations are introduced that allow one to specify whether or not two incomparable elements in the partial ordering correspond to subactivities that occur in any order or whether they are subactivities that never occur on the same branch of the activity tree. The same_bag relation is used to specify the sets of subactivity occurrences that are elements of strong poset activity trees that are subtrees of the activity tree. The alternate relation is used to specify the sets of subactivity occurrences that can never be elements of the same branch of the activity tree.
SHAPE \* MERGEFORMAT
Figure 4: Examples of poset activities in PSL.
The partial ordering in Figure 4(a) has four linear extensions, which correspond to the branches of the strong poset activity tree in Figure 4(c). The partial ordering in Figure 4(a) has four maximal chains, which correspond to the branches of the choice poset activity tree in Figure 4(b). the activity trees in Figure 4(d) and 4(e) are complex poset activities.
There are three basic classes of process plans, each of which impose different occurrence constraints on the elements of the partial ordering:
strong poset activities, in which there is a one-to-one correspondence between branches of the activity tree and the linear extensions of the partial ordering;
choice poset activities, in which there is a one-to-one correspondence between branches of the activity tree and the maximal chains in the partial ordering;
complex poset activities, each of which is the union of the strong poset activities corresponding to a set of linear extensions for suborderings of the partial ordering.
Two relations are introduced that allow one to specify whether or not two incomparable elements in the partial ordering correspond to subactivities that occur in any order or whether they are subactivities that never occur on the same branch of the activity tree. The same_bag relation is used to specify the sets of subactivity occurrences that are elements of strong poset activity trees that are subtrees of the activity tree. The alternate relation is used to specify the sets of subactivity occurrences that can never be elements of the same branch of the activity tree.
ILOG Scheduler
ILOG Scheduler (ILOG 2008) consists of an extensible library of C++ classes and functions that implement scheduling concepts such as activities and resources. The library enables the representation of scheduling problems as a collection of scheduling constraints, such as activity durations, release dates and due dates, precedence constraints, resource availability, and resource sharing. These constraints in turn are used as input for ILOG Solver, which can solve the constraints to provide schedules, in which activities are assigned to resources over different time intervals.
Translation Definitions
There are three main classes within ILOG Schedulers ontology:
IlcActivity
IlcResource
IlcSchedule
An instance of the class IlcSchedule is an object that represents a schedule. Any schedule is associated with a time interval, during which all activities in the schedule must occur.
(forall (?a)
(iff (IlcSschedule ?a)
(forall (?o)
(if (occurrence_of ?o ?a)
(and (or (permuted ?o)
(folded ?o))
(ordered ?o)
(amorphous ?o)
(uniform ?o)
(universal ?o)
(schedule ?o)
(strong_poset ?a)))))) (EQ 1)
The class IlcActivity is the root class for all activities that may occur in a schedule. All activities have a start time and an end time; the duration of an activity is the difference between these times.
(forall (?a)
(if (iff (nondet_res_activity ?a)
(primitive ?a))
(iff (ilcActivity ?a)
(activity ?a)))) (EQ 2)
ILOG Scheduler provides two predefined classes of activities: IlcIntervalActivity and
IlcBreakableActivity. An instance of IlcIntervalActivity is an activity which occurs without interruption from its start time to its end time and which requires the same resources throughout its occurrence. An instance of IlcBreakableActivity is an activity whose occurrence can be interrupted.
(forall (?a)
(iff (ilcIntervalActivity ?a)
(uninterruptable ?a))) (EQ 3)
(forall (?a)
(iff (ilcBreakableActivity ?a)
(interruptable ?a))) (EQ 4)
(forall (?occ1 ?occ2)
(iff (getSchedule ?occ1 ?occ2)
(subactivity_occurrence ?occ1 ?occ2))) (EQ 5)
Activities within a schedule satisfy precedence constraints, which are used to define orderings over the occurrences of the activities. The translation definitions for the complete set of precedence constraints defined in ILOG Scheduler is shown below:
(forall (?occ1 ?occ2 ?d ?a)
(iff (endsAfterEnd ?occ1 ?occ2 ?d ?a)
(exists (?s1 ?s2)
(and (leaf_occ ?s1 ?occ1)
(leaf_occ ?s2 ?occ2)
(soo_precedes ?s2 ?s1 ?a)
(= ?d (delay ?s1 ?s2)))))) (EQ 6)
(forall (?occ1 ?occ2 ?d ?a)
(iff (endsAfterStart ?occ1 ?occ2 ?d ?a)
(exists (?s1 ?s2)
(and (leaf_occ ?s1 ?occ1)
(root_occ ?s2 ?occ2)
(soo_precedes ?s2 ?s1 ?a)
(= ?d (delay ?s1 ?s2)))))) (EQ 7)
(forall (?occ1 ?occ2 ?d ?a)
(iff (startsAfterEnd ?occ1 ?occ2 ?d ?a)
(exists (?s1 ?s2)
(and (root_occ ?s1 ?occ1)
(leaf_occ ?s2 ?occ2)
(soo_precedes ?s2 ?s1 ?a)
(= ?d (delay ?s1 ?s2)))))) (EQ 8)
(forall (?occ1 ?occ2 ?d ?a)
(iff (startsAfterStart ?occ1 ?occ2 ?d ?a)
(exists (?s1 ?s2)
(and (root_occ ?s1 ?occ1)
(root_occ ?s2 ?occ2)
(soo_precedes ?s2 ?s1 ?a)
(= ?d (delay ?s1 ?s2)))))) (EQ 9)
(forall (?occ1 ?occ2 ?a)
(iff (endsAtEnd ?occ1 ?occ2 ?a)
(exists (?s)
(and (leaf_occ ?s ?occ1)
(leaf_occ ?s ?occ2)
(soo ?s ?a))))) (EQ 10)
(forall (?occ1 ?occ2 ?a)
(iff (endsAtStart ?occ1 ?occ2 ?a)
(exists (?s)
(and (leaf_occ ?s ?occ1)
(root_occ ?s ?occ2)
(soo ?s ?a))))) (EQ 11)
(forall (?occ1 ?occ2 ?a)
(iff (startsAtStart ?occ1 ?occ2 ?a)
(exists (?s)
(and (root_occ ?s ?occ1)
(root_occ ?s ?occ2)
(soo ?s ?a))))) (EQ 12)
(forall (?occ1 ?occ2 ?a)
(iff (startsAtEnd ?occ1 ?occ2 ?a)
(exists (?s)
(and (root_occ ?s ?occ1)
(leaf_occ ?s ?occ2)
(soo ?s ?a))))) (EQ 13)
Domain theories for the ILOG Scheduler Ontology consist of conjunctive formulae consisting of precedence constraints that use the above eight relations.
Validation of Translation Definitions
The reasoning problem associated with ILOG Schedule is schedule existence: an executable schedule is the output of the software application iff the following sentence is consistent with the application ontology and the domain theory that axiomatizes the input to the software application:
SHAPE \* MERGEFORMAT
The first attempt at providing translation definitions between ILOG Schedule and the PSL Ontology was described in \ref{} (Ciociou et al 2001). Through the methodology of the Ontological Stance, however, these definitions have been shown to be incorrect. In particular, the translation definitions did not capture the correspondence between possible schedules and branches of the activity trees that satisfied the precedence constraints; as a result, none of the domain theories were consistent, even though schedules were generated by ILOG Scheduler.
It is also instructive to see how a slight modification of the above translation definitions would also be incorrect. For example, consider the following:
(forall (?occ1 ?occ2 ?d ?a)
(iff (startsAfterStart ?occ1 ?occ2 ?d ?a)
(exists (?s1 ?s2)
(and (root_occ ?s1 ?occ1)
(root_occ ?s2 ?occ2)
(soo_precedes ?s2 ?s1 ?a)))))
This sentence is incorrect, since there exist models of domain theories using this precedence relation that are not schedules produced by ILOG Schedule, namely, those in which the subactivity occurrences dto not satisfy the delay constraint.
The final translation definitions were tested by the generation of random sets of precedence constraints. By the Ontological Stance, ILOG Schedule produces a schedule for these constraints iff the corresponding domain theories for the ontology are consistent; furthermore, there should be a one-to-one correspondence between solutions of the precedence constraints and branches in the activity trees that are axiomatized by the domain theories.
It should be emphasized that the experiments with random precedence constraints are used to evaluate the translation definitions; they are not used to generate the translation definitions. In general, the methodology for generating translation definitions requires more sophisticated techniques to elicit the sentences that are satisfied by intended models of the application ontology.
SAP Flow Models
SAP ERP (SAP 2008)is an enterprise resource planning solution that among many other capabilities can be used to design manufacturing processes and manage manufacturing operations. In this context the SAP ERP system can be viewed as the central repository for manufacturing process information. Production orders in the ERP system are used to represent the enterprise's demand on manufacturing operations to deliver a certain quantity of a specific product to be available by a give date and time.
Translation Definitions
The central construct in the SAP application ontology is the SAP production order. A production order can contain multiple ``sequences'' of operations. The sequences can be of three types: simple sequence, alternate sequence or parallel sequence. A simple sequence is a linearly ordered sequence of operations (see Figure 5(b)). Each production order has a main simple sequence called the standard sequence; branching off from the standard sequence can be parallel or alternate sequences. Each parallel or alternate sequence consists of a simple sequence, and it also has start and end branch points to indicate the subsequence of the standard sequence with which it is parallel or alternate (see Figure 5(b) and Figure 5(c)). Parallel sequences occur in parallel with the corresponding standard subsequence, but alternate sequences, if they are chosen for execution, will occur instead of the corresponding subsequence of the main sequence.
(forall (?a)
(iff (production_order ?a)
(or (simple_sequence ?a)
(parallel_sequence ?a)
(alternate_sequence ?a)))) (EQ 14)
Any activity tree for a simple_sequence process plan consists of a unique branch. None of the operations within a sequence overlap, there is no iteration, and all activity trees have the same structure.
(forall (?a)
(iff (simple_sequence ?a)
(forall (?o)
(if (occurrence_of ?o ?a)
(and (simple ?o)
(rigid ?o)
(ordered ?o)
(amorphous ?o)
(uniform ?o)
(universal ?o)
(unrestricted ?o)
(strong_poset ?a)))))) (EQ 15)
Any activity tree for a parallel_sequence process plan consists of branches that are combinations of occurrences of the operations within a set of sequence process plans.
(forall (?a)
(iff (parallel_sequence ?a)
(forall (?o)
(if (occurrence_of ?o ?a)
(and (permuted ?o)
(rigid ?o)
(ordered ?o)
(amorphous ?o)
(uniform ?o)
(universal ?o)
(unrestricted ?o)
(strong_poset ?a)))))) (EQ 16)
Any activity tree for an alternate_sequence process plan consists of a set of branches, each of which corresponds to the activity tree for a sequence process plan.
(forall (?a)
(iff (alternate_sequence ?a)
(forall (?o)
(if (occurrence_of ?o ?a)
(and (simple ?o)
(rigid ?o)
(nondet_ordered ?o)
(amorphous ?o)
(uniform ?o)
(universal ?o)
(unrestricted ?o)
(choice_poset ?a)))))) (EQ 17)
SHAPE \* MERGEFORMAT
Figure 5: Examples of SAP process plans.
Domain theories for this application ontology consist of formulae that specify the branch points between different sequences within the production order. Two relations are used to specify these domain theories next_op (which is the ordering relation among elements of the same sequence) and branch_point (which is the ordering relation between elements of different sequences).
(forall (?o1 ?o2 ?a)
(iff (next_op ?o1 ?o2 ?a)
(exists (?a1)
(and (subactivity ?a1 ?a)
(simple_sequence ?a1)
(soo_precedes ?o1 ?o2 ?a1)
(soo_precedes ?o1 ?o2 ?a)))) (EQ 18)
(forall (?o1 ?o2 ?a)
(iff (branch_point ?o1 ?o2 ?a)
(exists (?a1 ?a2)
(and (subactivity ?a1 ?a)
(subactivity ?a2 ?a)
(simple_sequence ?a1)
(simple_sequence ?a2)
(not (= ?a1 ?a2))
(soo ?o1 ?a1)
(root_soo ?o2 ?a2)
(soo_precedes ?o1 ?o2 ?a))))) (EQ 19)
Validation of Translation Definitions
The reasoning problem associated with the SAP Ontology is executability a production order in the software application is executable iff the following sentence is consistent with the application ontology and the domain theory for the production order P:
SHAPE \* MERGEFORMAT
Since the class of production orders is axiomatized by a class of poset activities in the PSL Ontology, production orders in experiments were generated by the construction of random comparability graphs (which are a class of graphs that correspond to partial orderings). The initial set of translation definitions was found to be incorrect, since the production orders are actually restricted classes of poset activities. In particular, the second activity occurrence argument in the branch_point relation must be the initial element of the corresponding simple sequence subactivity. This error led to domain theories that did not correspond to production plans, that is, domain theories for which the above sentence is consistent, yet which the software application determined to be unexecutable.
MetCAPP
MetCappTM (MetCAPP 1994) is a computer-aided process planning system that generates process plans, given a set of workstations, machines, setups, routing sequences, and generic part feature data. A machining capability database provides automated capabilities of cutting tools selection, speed and feed calculations, processing time estimation, and operation sequencing. In this paper we are primarily be concerned with the operation sequencing concepts.
Translation Definitions
A routing in MetCAPP is a resource path whose underlying topology is a complex poset.
(forall (?a)
(iff (routing ?a)
(and (resource_path ?a)
(complex_poset ?a)))) (EQ 20)
An operation is an activity that satisfies the following conditions:
An operation is the superposition of a processor activity and a setup activity for the unique possibly reusable resource of the processor activity.
All subactivities of the processor activity require the same possibly reusable resource.
An operation is also a resource path composed of feature activities, with the topology of a strong poset activity.
(forall (?a1)
(iff (operation ?a1)
(exists (?a2 ?a3 ?a4 ?r)
(subactivity ?a3 ?a1)
(subactivity ?a1 ?a2)
(processor_activity ?a3)
(possibly_reusable ?r ?a3)
(subactivity ?a4 ?a1)
(setup_activity ?a4 ?r)
(resource_path ?a3)
(strong_poset ?a3)
(routing ?a2)
(forall (?a5 ?r2)
(if (and (subactivity ?a5 ?a3)
(processor_activity ?a5)
(possibly_reusable ?r2 ?a5))
(= ?r2 ?r)))))) (EQ 21)
The next_operation relation is the coo_precedes relation of complex posets restricted to the operation subactivities of a routing.
(forall (?occ1 ?occ2 ?a)
(iff (next_operation ?occ1 ?occ2 ?a)
(exists (?s1 ?s2 ?a1 ?a2)
(and (coo_precedes ?occ1 ?occ2 ?a)
(routing ?a)
(operation ?a1)
(operation ?a2)))) (EQ 22)
The concurrent_operation relation is the same_bag relation for complex posets, restricted to the operation subactivities of a routing.
(forall (?occ1 ?occ2 ?a)
(iff (concurrent_operation ?occ1 ?occ2 ?a)
(exists (?s1 ?s2 ?a1 ?a2)
(and (coo_parallel ?occ1 ?occ2 ?a)
(routing ?a)
(operation ?a1)
(operation ?a2)))) (EQ 23)
An alternate activity is a choice poset activity composed of operations.
(forall (?occ1 ?occ2 ?a)
(iff (alternate_operation ?occ1 ?occ2 ?a)
(exists (?s1 ?s2 ?a1 ?a2)
(and (coo_alternate ?occ1 ?occ2 ?a)
(routing ?a)
(operation ?a1)
(operation ?a2)))) (EQ 24)
Domain theories for this ontology specify routings, and consist of conjunctive sentences using the above three relations.
Validation of Translation Definitions
The reasoning problem associated with MetCAPP is equivalent to the consistency of the existence of an occurrence of a routing consisting of a set of operations:
SHAPE \* MERGEFORMAT
As with the SAP application ontology, routings in MetCAPP are axiomatized by poset activities, so that experiments to verify the translation definitions can be designed by randomly generating comparability graphs, which can then be translated into partially ordered sets.
Generation of Semantic Mappings
Using the above axiomatizations of the application ontologies, we can use the PSL Ontology to generate direct semantic mappings between the application ontologies. Since all translation definitions are sentences in PSL, we can entail sentences that characterize the relationships between concepts in the different application ontologies. In this section, we present some of the sentences that are entailed by the translation definitions in the scenario described above.
First, we can show that process plans in MetCAPP can be exported to SAP by showing that the following sentences are entailed by the translation definitions. Note that the sentences have the special property that the antecedent is a relation in the MetCAPP ontology, while all of the relations in the consequent in each formula are in the SAP ontology.
(forall (?a)
(if (routing ?a)
(or (simple_sequence ?a)
(parallel_sequence ?a)
(alternate_sequence ?a)))) (EQ 25)
(forall (?a)
(if (operation ?a)
(or (simple_sequence ?a)
(parallel_sequence ?a)))) (EQ 26)
(forall (?occ1 ?occ2 ?a)
(iff (next_operation ?occ1 ?occ2 ?a)
(next_op ?occ1 ?occ2 ?a))) (EQ 27)
We can also show that the process plans in the SAP ontology can be exported to ILOG Schedule:
(forall (?occ1 ?occ2 ?a)
(if (next_op ?occ1 ?occ2 ?a)
(exists (?d)
(startsAfterEnd ?occ1 ?occ2 ?d ?a)))) (EQ 28)
(forall (?occ1 ?occ2 ?a)
(if (next_op ?occ1 ?occ2 ?a)
(exists (?d)
(or (endsAfterEnd ?occ1 ?occ2 ?d ?a)
(endsAfterStart ?occ1 ?occ2 ?d ?a)
(startsAfterEnd ?occ1 ?occ2 ?d ?a)
(startsAfterStart ?occ1 ?occ2 ?d ?a)
(endsAtEnd ?occ1 ?occ2 ?d ?a)
(endsAtStart ?occ1 ?occ2 ?d ?a)
(startsAtStart ?occ1 ?occ2 ?d ?a)
(startsAtEnd ?occ1 ?occ2 ?d ?a))))) (EQ 29)
In general, not all SAP process plans can be mapped to MetCAPP routings, and not all ILOG activities can be mapped to SAP process plans. The precise relationships between these classes of processes is still an open problem.
LIMITATIONS
At the beginning of this paper, we introduced the Interoperability Hypothesis, by which we are considering interoperability among complete first-order inference engines that exchange first-order sentences. There are, of course, many knowledge-based systems that use nonmonotonic reasoning (such as logic programming) rather than first-order entailment. The Ontological Stance must be extended in order to work with such software applications. The primary problem in this case is that the semantics of logic programming systems requires second-order logic to fully characterize the intended models, whereas we restrict ourselves to first-order logic because it is sound and complete.
Summary SUMMARY
One approach to the semantic integration of software applications is through the generation of semantics-preserving mappings between their respective ontologies. In practice, this approach does not succeed due to several problems the applications do not have explicit ontologies, or if they do, then the ontologies are often incomplete, and the existence of unintended models prevents the specification of semantic mappings. Furthermore, there has been little work done to validate the proposed semantic mappings.
In this paper, we have addressed these challenges by using an interlingua ontology and the methodology of the Ontological Stance to axiomatize the implicit ontologies of software applications. The correctness and completeness of the axiomatization with respect to the intended models of the application ontology is achieved since the interlingua ontology is verified. The correctness and completeness of the axiomatization with respect to the software application, as well as the correctness and completeness of the semantic mappings, is demonstrated through the use of the Ontological Stance -- any sentence that is satisfiable or entailed by the axiomatization and semantic mappings must be a possible output of the software application.
GLOSSARY
Axiomatizes: A set of sentences in a logical language axiomatizes a class of structures iff every model of the sentences is in the class of structures and every structure in the class satisfies the set of sentences. A class of structures is axiomatizable in a language L iff there exists a set of sentences in L that axiomatizes the class.
Completeness (of a logic): A representation is complete if for any sentence S and theory T, if S is satisfied by all models of T, then S is provable from T by some inference procedure. Equivalently, a representation is complete if for any sentence S and theory T, if S is consistent with T then there exists a model of T that satisfies S.
Definitional extension: A theory T1 is a definitional extension of a theory T2 if all sentences in T1 are biconditionals that define the terms in the lexicon of T1.
Elementary equivalence: Two interpretations are elementary equivalent iff they satisfy the same set of first-order sentences.
Entailment: A theory T entails a sentence S iff S is satisfied by all models of T. A set of models entails a sentence S iff it is satisfied by all of the models in the set.
Interpretation: An interpretation M of a first-order language L consists of the following:
a nonempty set D, called the domain of the interpretation;
for each constant symbol in L, the assignment of an element in D;
for each n-ary function symbol in L, the assignment of a mapping from Dn to D;
for each n-ary predicate symbol in L, the assignment of a truth value to sets of elements in Dn.
Lexicon: The set of relation, function, and constant symbols in the terminology of an ontology.
Model: An interpretation M is a model for a theory T if the truth value for each sentence in T with respect to M is true.
Satisfiable: A theory T is satisfiable if there exists a model for T.
Soundness (of a logic): A representation is sound if for any sentence S and theory T, if S is provable from T by some inference procedure, then S is satisfied by all models of T. Equivalently, a representation is sound if for any sentence S and theory T, if there exists a model of T that satisfies S, then S is consistent with T.
ReferencesREFERENCES
Bock, C. and Gruninger, M. (2004) PSL: A semantic domain for flow models, Software and Systems Modeling}.
Ciocoiu, M., Gruninger M., and Nau, D. (2001) Ontologies for integrating engineering applications, Journal of Computing and Information Science in Engineering}, 1:45-60.
Dennet, Daniel C. The Intentional Stance. Cambridge, MA, The MIT Press, 1987.
Gruninger, M. (2003) Ontology of the Process Specification Language, pp. 599-618, Handbook of Ontologies and Information Systems, S. Staab (ed.). Springer-Verlag, Berlin.
Gruninger, M., and Fox, M.S. (1995) Methodology for the Design and Evaluation of Ontologies, Workshop on Basic Ontological Issues in Knowledge Sharing, IJCAI-95, Montreal.
Gruninger, M. and Kopena, J. (2004) Semantic Integration through Invariants, AI Magazine, 26:11-20.
Gruninger, M. and Menzel, C. (2003) Process Specification Language: Principles and Applications, AI Magazine, 24:63-74.
Giunchiglia, F., M. Yatskevich, and F. McNeill, (2007) Structure preserving semantic matching. In: Proceedings of the ISWC+ASWC International workshop on Ontology Matching (OM), pages 1324, 2007.
Kalfoglou, Y. and Schorlemmer, M., (2003) Ontology Mapping: The State of the Art, The Knowledge Engineering Review, vol. 18, iss. 1 pages 1-31, 2003.
ILOG Scheduler 6.3 Reference Manual, ILOG, Inc., 2008.
MetCapp Utilities Manual, The Institute of Advanced Manufacturing Sciences, Cincinnati, Ohio, 1994.
SAP Library. Retrieved on November 17, 2008 from http://help.sap.com/saphelp_erp60_sp/helpdata/en/e1/8e51341a06084de10000009b38f83b/frameset.htm
Schlenoff, C., Gruninger, M., Ciocoiu, M.. The essence of the Process Specification Language, Transactions of the Society for Computer Simulation vol.16 no.4 (December 1999) pp 204-216.
Available at http://ats.nist.gov/psl/twenty.html.
PSL has been published as an International Standard (ISO 18629) within the International Organisation of Standardisation. The full set of axioms in the Common Logic Interchange Format is available at http://www.mel.nist.gov/psl/ontology.html.ddddddddddddd
5I `
a
b
k
ǽkZIk3*HhŊFhPhPCJ$ۊF*!HhFhPhPOJQJ!HhFhPhPOJQJ6HhFhPhPCJ$F*CJOJQJHhFhPhPCJ$HhFhPOJQJHhFhP6HhFh='EhPHhFhPHhۊFhPCJ$HhŊFhPCJ$HhǊFhPHhƊFhPHhƊFhPCJ$45G{ooooG$C$EƀǊFa$G$C$EƀƊFa$
_a
g"DC$EƀFO$C$EƀۊFa$gdPoۊFG$C$EƀŊFa$a
b
eLC$EƀۊFgdPoۊFLC$EƀFgdPoۊF
6LfqaDC$EƀƊF$a$T$C$EƀFa$gdPoۊFd&$a$
fpq
>PVɼɰɦɘvc_LB_HhqkҦhP%hPhcHdhdhdhqkҦhP%hPhPcHdhdhdhȊF&HhƊFhPhPȊF*HhFhPOJQJHhFhPOJQJHhFhPHhFhP6HhFh='EhPHhFhPHhȊFhPHhƊFhP%hPhPcHdhdhdhǊF
hPCJ$q;<fg]^jhffffffffPC$EƀȊFgdPoȊFd&FDC$EƀFCeaf^R"""""ùִ֬֬|rִhX֬OGhPOJQJhPH*OJQJhPcHdhdhdh]fHh]fhPHhzjҦhP%hPhcHdhdhdhzjҦ%hPhPcHdhdhdhȊFHhȊFhPhPOJQJ hP6HhqkҦhP%hPhcHdhdhdhqkҦhPHhjҦhPOJQJHhjҦhPHhjҦhhP^" # R"&&&h'i'))))--002434Y7Z799::::"""""###<#>####6$8$T$V$X$Z$$$$$$$$$$$$%0%2%T%V%%%%%&&)&4&?&&&&>hwhPhcHdhdhdhrkҦTc҆*56hwhPTc҆*56HhrkҦhPOJQJ-hPhOJQJcHdhdhdhrkҦhPOJQJhPOJQJhPH*OJQJhPOJQJhPOJQJ.&&&&'h'9)=)))))++++X,a,H7W7.:6::::::::::лзukuYQujhPU"jhPUmHnHsHtHuhPmHnHsHjhPUmHnHsH hP6%hPhPcHdhdhdhɊFHhɊFhPhPOJQJHhrkҦhPhP)Hh]fhwhPTc҆*6hwhPTc҆*6hwhPTc҆*56HhrkҦhwhP56::P;Q;1<2<}<<<AACC!G"GIIcLdLONPN~N$QRST
&F
h^`
o\fd&F:::;; ;O;P;;;;2<@<U<_<a<}<<<<<<<<X=a=f=Ͽ϶}i}iRDRDHhskҦhPOJQJ-hPhOJQJcHdhdhdhskҦ'hPOJQJcHdhdhdhXUF$hhPOJQJwjҦ*6HhXUFhPH*OJQJHhXUFhPOJQJhPOJQJhP5OJQJHh&\fhPmHnHsHHh\fhP+hPcHdhdhdh\fmHnHsHhPcHdhdhdh\ff=g=ACCCCEE$FNNONPNgN}N~NGOLOOPRSSSŷܟqZG$hwhPOJQJTc҆*6,hwhPOJQJTc҆*6OJQJ$hwhPOJQJTc҆*6hPOJQJ%hPhPcHdhdhdhɊFHhɊFhPHhmkҦhPOJQJHhtkҦhPOJQJ-hPhOJQJcHdhdhdhtkҦhPhPOJQJ-hPhOJQJcHdhdhdhskҦSS
S6S8S:S@SBSDSSSSSSSSSSTaXXнЪr_нЪKC5HhRFhPOJQJhPOJQJ'hPOJQJcHdhdhdhRF$hwhPOJQJTc҆*6=hwhPOJQJcHdhdhdh3\fTc҆*61Hh3\fhwhPOJQJTc҆*6$hwhPOJQJTc҆*6$hwhPOJQJTc҆*6,hwhPOJQJTc҆*6OJQJ/hwhPH*OJQJTc҆*6OJQJTWYY9Y#Z$Z%ZcZ]`accduffKgRhijFjk
&F
h^`
&F
h^`
o \fd&FXXXXXXYYY4Y5Y6Y7Y8Y9YCYJYKYMYqYvY"Z#Z$Z%ZDZǽǫǽsojoaWMCHhʊFhPHhRFhPHhRFhPhP5OJQJ hP6hP+hPcHdhdhdh \fmHnHsHhPcHdhdhdh \fHh \fhPjhPU"jhPUmHnHsHtHuhPmHnHsHjhPUmHnHsHHhRFhPOJQJhPOJQJ'hPOJQJcHdhdhdhRFDZbZcZ[[aaaaobsb~bbLcPc`ccccddffఢxndnVHHhPSFhPOJQJHhRFhPOJQJHhʊFhPHhRFhPHhiSFhPOJQJHhhSFhPOJQJHhgSFhPOJQJHhfSFhPOJQJHhHSFhPOJQJ'hPOJQJcHdhdhdhRFHhukҦhPOJQJhPOJQJhP%hPhPcHdhdhdhʊFfggggg+gIgKghhhhPhiijEjFjjjkʼvhZL>HhaSFhPOJQJHh`SFhPOJQJHh_SFhPOJQJHhSSFhPOJQJHhVSFhPOJQJHhRFhPOJQJHhUSFhPOJQJHhRSFhPOJQJHhRSFhPOJQJHhQSFhPOJQJ0HhQSFhPOJQJQSF*OJQJHhTSFhPOJQJHhQSFhPOJQJkkkklmmnnnnnnpppBqCqDqhqsqǹsesWSI9hPcHdhdhdhRFHhˊFhPhPHhRFhPOJQJHhZfhPOJQJHh^SFhPOJQJHhXSFhPOJQJHh_SFhPOJQJHhxjҦhPOJQJHh^c҆hPOJQJHhUFhPOJQJHhjSFhPOJQJHheSFhPOJQJHh`SFhPOJQJHhcSFhPOJQJkYmnCqDqqq s
s}t~tuu~xxzz{{{{||}}BC@Asqqq suuvv~wwwwww1x}xzz{/{x{{{{||ĺΒ~t~jXjJHhO[fhPOJQJ#HhO[fhPP[f*H*HhO[fhPHhM[fhPHhN[fhPHhI[fhPHhL[fhPHhC[fhPHhA[fhPHh@[fhPHhZfhPHhZfhPHhiUFhPhPcHdhdhdhUFhP%hPhPcHdhdhdhˊF||.|0||||}}0}}ACˀЀoۻxtdTDT4T4ThPcHdhdhdhLUFhPcHdhdhdhfM&hPcHdhdhdhS[fhPcHdhdhdhKUFhPHhiUFhPHhR[fhPHhFhPHhQ[fhP4HhQ[fhPOJQJQ[f*OJPJQJHhQ[fhPOJQJ#HhP[fhPR[f*H*HhP[fhP4HhO[fhPOJQJP[f*OJPJQJotAB\`ltuӂiz3>G03ۻ˧˧ۍۍۃyۃo_M"hP6cHdhdhdh]fhPcHdhdhdh]fHhkc҆hPHhSUFhPHhS[fhPhPcHdhdhdh2UFHh2UFhPHh1UFhPHhUFhPhPcHdhdhdhUFhPcHdhdhdh1UFhPhPcHdhdhdhS[fhPcHdhdhdhLUFAhiLMәԙdeUV3i
!,>jsiYOG7OhPcHdhdhdh6]fhPOJQJHh6]fhPhPcHdhdhdh5]fHhjc҆hP%hPhwcHdhdhdhjc҆hPhPcHdhdhdhW[f,jhP0JUcHdhdhdhUFhPcHdhdhdhUFHh]fhPhPcHdhdhdh]fHh]fhPHhQUFhPhPcHdhdhdh]fLÕV\]^sҙe| %{vvl^T^hPmHnHsHjhPUmHnHsHHhcc҆hP hP6HhUFhPHhHSFhPHhGSFhP%hPhPcHdhdhdhFHhFhPhPHhFhPHhRFhP%hPhPcHdhdhdhˊFHhˊFhPHh]fhPhPhPOJQJklʳ˳DC$Eƀcc̪҆ͪΪЪܪުwjʬlYL?5HhFhPHhFhPhPHhFhPhP%hPhPcHdhdhdhF2jhPhP0JUcHdhdhdhF%hPhPcHdhdhdhF%hPhPcHdhdhdhFHhFhPHhZfhPHhPUFhPhPhPmHnHsHjhPUmHnHsHjDhPU"jhPUmHnHsHtHuj]^ +UV͵صFGVnȷɷef&źκSTUlmnopxy2жжڧsHh"]fhPmHnHsHjhPU"jhPUmHnHsHtHuHh"]fhPjHh"]fhPUHh*\fhP6Hh*\fhPOJQJHh*\fhPHh%\fhP hP6%hPhPcHdhdhdhFhP-)ɷfSTq;ؾ6u
o.\fd&F
o&\fd&F
&F
h^`23:;ؾ7@uLVcn 3gt&0ǳǳǳǡǡǝ|||Hh]fhPHh]fhPhPOJQJ hP6hP"hP6cHdhdhdh*\f'hPOJQJcHdhdhdh*\fhPcHdhdhdh*\fHh,\fhPHh.\fhPHh#]fhPHh-\fhP.uRS`x
1WXY'(5Xk
&F
h^`"#0Ouv12/0Ls!J^YZ23'Vct{ IJK,ϳϥwghPcHdhdhdh#]fHh#]fhPHh]fhPHh!]fhPhPcHdhdhdh!]f
hPEHjhPU"jhPUmHnHsHtHuhPmHnHsHjhPUmHnHsHHh]fhPHh]fhPhPHh]fhP(^{#7Tm-Fd()Bet/Gde~ p^p`@^@,-$AZ|}op-.}~$a$,M,|/:<=TUVWX`coW^翵}siHh\fhPHh \fhPHh!\fhPHh"]fhPHh\fhPj$hPU"jhPUmHnHsHtHuHh\fhPjHh\fhPU hP6Hh]fhPHh%]fhPhPHhRFhPHhRFhP%%:J\p ^`$6Ja-.;Yh;<Y
o\fd&F o\fd&$3C]tussssiii ^`DC$Eƀdc҆DC$Eƀcc҆
79.01234ٽٯٽjbhPUHh]fhPHh]fhPhPOJQJ hPH* hP6
hPEHjhPU"jhPUmHnHsHtHuhPmHnHsHjhPUmHnHsHHh]fhPhPHhcc҆hP21H_r&'/0$a$ ^` p^p`ghz10aIW
&F
h^` ^`]&'Ag .X ^` ^``%?cqOu56FGg>?$a$ ^` ^``45EGg.9<BB
C
D
ȺȲrdZPZHhRFhPHhRFhPHhRFhPOJQJ1HhRFhwhPOJQJ_c҆*6HhRFhPHhdc҆hP%hPhPcHdhdhdh̊FhPOJQJHh]fhPOJQJHh]fhPOJQJHh̊FhPHh]fhPCJHh]fhPhP
hPEH,@[MNg7^LMN.:;<FC$Eƀdc҆C
D
>?lmEoRFd&F
&F
h^`
&F
h^`oRFd&
&F
h^`oRFd&h^hh^hoRFd&FD
P
]
=?UVWRYlm{DEįĥě|r|WIHhRFhPOJQJ4HhRFhPOJQJRF*OJPJQJHhZfhPHh8UFhP)Hh;UFhwhP_c҆*6Hh;UFhPHh`c҆hP)HhZfhwhP_c҆*6HhZfhPHhRFhPHhRFhPOJQJ1HhRFhwhPOJQJ_c҆*6<G`$ҧvfX?1HhBUFhwhPOJQJ_c҆*6HhBUFhPOJQJHhBUFhP6OJQJHhbc҆hPHhac҆hP$Hhac҆hwhP6OJQJHhBUFhP<hPOJQJcHdhdhdhRFRF*OJQJHhRFhPH*HhRFhPOJQJHhRFhPHhRFhPHhRFhPH*XYPJ>JoRFd&h^hh^hOC$Eƀac҆oRFd&h^hMhC$Eƀac҆^hoRF
h^hoRF$a$$123gijt~#9!%ELͺ~fNf6.HhjҦhhPB*OJPJQJph.HhjҦhhPB*OJPJQJph.HhjҦhhPB*OJPJQJphHhjҦhP)Hh^c҆hwhP^c҆*6Hh^c҆hP hP6hPHhڊFhP%hPhPcHdhdhdhڊFhPCJOJ QJ Hhdc҆hPCJOJ QJ HhBUFhPHhBUFhPOJQJghij9gdPoRFd&FKC$Eƀdc҆oRFoRFd&h^h9pRC$EƀjҦgdPojҦd&EEƀjҦIC$Eƀ^c҆gdPLXYv5^_`踮|xsxYOx=Ox#hPB*CJPJmHnHphsHjhP0JU3hPB*CJOJPJQJ_HmHnHphsHtH hP6hP2HhjҦhhPB*OJPJQJ_Hph.HhjҦhhPB*OJPJQJphHhjҦhP.HhjҦhhPB*OJPJQJph.HhjҦhhPB*OJPJQJph.HhjҦhhPB*OJPJQJph1RC$EƀjҦgdPojҦd&{
&0`
P@1$7$8$EƀjҦH$gdPojҦd&
0`
P@1$7$8$H$w^_
gdPoFd&FlC$EƀjҦgdPojҦd&
&0`
P@1$7$8$H$ѷ3hPB*CJOJPJQJ_HmHnHphsHtHhP#hPB*CJPJmHnHphsH0HhFhPB*CJPJmHnHphsH/ =!"#$%n79DLb m64PNG
IHDRH_PLTE.obKGDHcmPPJCmp0712HsIDATx^흍*
;/zhLEC癞vmA^QcI
gRAX*Σ4G)pT2V(JƪpQXuΣ8*NyG%ci8Rd:
Q
Uުgk8rǽCO3͵pasRIDATczfW3ε
>^k'8y8oםοvf
pvsͺ$\ebñv}
q48@җBWv~V-g;9e.NVb#I-2
*'x
!^BӞi, Op ـ\1k^(N`^yOyf;7LLw78S3J3C*ЅOq5{T??&B:q}otPS#;vKÐ}2;A3b`ON[^lgH20ϕ$$I!aL9٧Q^9L~pΞk gI3hz{:'l㰫ITw!ǽcJX*RʥU457TWΛkgG
֭'ZYO xArKB3̪ ]hr[T(Ή`x]p>\[AWéOoymI/yD@DA8ܼ.A݊d}StN+W)+к6pf{~ MwP`qh۞euV 7Ϗ|0&'8}65l3pF}k.
2>vBcu:xG4t4hݯem 5v/TbB$F' dM&M(+4'&?Y-8ju
*P!̝#pZ1,.=)x6yb3?|??W
~P?%JpzʌܽNϳhE>Z
NTė؏߹<,BY㢼]+!p8h g}2(M(YeS`xҮ}Dm2w'8o^B^@0IDAT8)wN0
l$iBJdsJ_
W I&5:G6HxM6nSv^֎E1V\A*$[]:A,?]ʍʶ?)H^DJUJ>FluLWʷ#|l2'2绛ˈg婔'{*Q̸{&!tW%rf1BdlTpξ.֘VVpRx8q4]|ZuZubmp+ONb`SscN;⍜
Z.%G$쎊
(wSeȞFPL]9Rymk9y5'Y9R㉾g)_w&ΗepoA3y}}lgO.!T,%"»uY^&n9rk%E]̭rh?4x g',cc#=Dڶg'Hcg,YyDhNbDR 6Չ#(ۖ8[,4I^oTcN*lNx}q8UbI>%UXHZ ;w@;aNl&t[Qi-zب:[-)m%c{es'۽ｔx] vRTn#|oEž)\]+F؊Ĵ^P·ɱ$;ǎoo3
g:|?44pjԾyrUg:sIDATeȥFU7W P3;0Χᬝ|>!G
pVed0|~XoT&(>D?t!FZp,VB[[6.^kD!$^)qTҲӄGk>JH!]",2l}K5jϊn>_>/
eŐbEq*诛8n\[S{J4%/u!D^_*%fB&ߔJ_@_MGoIDAT9dE܄s?݇=j9xZU`_\ciY<.
a?Ou:r8i$M\t>8dA A`d4wJ|}pl&-n r&[@7XAvY&%δ=
ʵDN^hPNowOY5GyqVec0fkЕgьb1J;[|4/
.HpۆzvyuTpƑ$ò>]i
pKy@ƨy=)Sj庢:e ,
bS9EdLi<:)m+ʑtGhp>[L[I%8WɊdX]`vɤ);sC(_opVfI.ws0\jv_ͳ/9Rgfu)+ԑ˪yX"=41Fxfr'oIq;je64yRÉ:[
'^FK7TbP2epSbOζFE9O_Dyd;;xÉhrqC<ӭegxm+?=_pL.) Ap>d8akP;!!]t?ۢQ:1y (Ƙg[Nw0gQc%h 16Tʠ<ጂTNeP@$*gIͶc>WDgTȸWnmu
3*_Kpzt
3*8T7a!x.Nfhޮ03}NN8)Y^{Eψd/%ѯGM zkOdi`8節vAnV
#LjK\KJժoNFE<
'd%g9^Eiwá72+n(p3Q
Z8IDATi;VH5FpՃnkIik&^7nlIdkM3f
vnN\l&[)|C
PTLD|"J\H=1 rNOn\gTpp0w3[N<`8`}MrV6mc:#3\KyCߟ6&e;_=#ޗaFȱogа{5c8bN.qY!$fpc&q丹5\ofhjy(Cg`lTS2RQ&Nkis*VF5lgb2k)G<ơZ&
5Ę)r;<{>q~+rĒu2Pq%qjB
$,gPdq>g':#wȒkaHᘘ9,jP*(%^on|X+ vM,f_XPW^nI`,VL\6@Œ`Z\of2VTD̎L#
t;*PF3R!`b'F5TB;1P1`b'
5L@K'F5LH)0#CdGH;0T1`b
6U
"$}`
3\1Nh℉}+ss=W:x)'s̓6HBWK5h8Cz죊e܃$<IiHr.7@^NqpMx3'~7; 3|?v&ֆ}HN+
9\&!e7ٗ25`/|
ֆ'C{$r\1>$T̅>؇5=TIf"k9f^7j@ZH6dPeY]!-dsb{<13>ryr2;KfeT:c]exWGtcھFoq+Ő(yWEnuLkyyL"]q;. "
}{/B*dBUU,rK;hNBZ'^JѼQú~uL76(!yt}jK|=Hxg^6qυt?͍7\:fT{^([ίZ;WnX҄G)avaij-jʭ{oixȑá(Y\{uual5+=5j;*(<,_C3qݵe9q}F7Q]GQ*O,_CB&+:KK*pnVo;#~ײ|ADܥ$VĹqOMo(?"?$Ĺi 5~eƕhĈ:\&/>Ŏ&dll$r~GuK?Y<1qH;X.i/yf2wT/屏ْey &IםnښH%p\;h79N -M~֔-T =o5P!np
!CO9͐k Dxu8xRvmo@ޮw$)vD`"h&`"h&`"h&`"h&`"h&`"h&`"h&`"h&`"h&`"h&`"hK/;_ى/,Wٲ7fz{,W_벹Mt^[J_5qoi:%m`U.oǎ76t2Q^gd{~wg3&e
yN&xzᑎs디gO
}^lflŲ
au4C6?e֗AOYg&ZEzw:{M̓IMO}}n9u_)ϔWkal1#\;u"u3#(0,3eoYh5붹VC^ƹ(܈z$9~=[~_/.7OMy/Zsj/[IX˕7>,͛hȅS,7!gvzuv ObD huPSCqLdjWV40bZ-^,cuB!`"h&`"h&`"h&`"h&`"h&`"h&`"h&`"h&`"h&`"h&`"h&`"h&`"h&`"h&`"h&`"h&`"h&`"h&`"h&`"h&`"h&`"h?udK{IENDB`nG$[%^C9רҽPNG
IHDRHlPLTET=bKGDHcmPPJCmp0712HsIDATx^흋ӥ\, `]!ZU0
H"!h#$ 6@+H"h#$ 6@+H"h#$ 6@+H"h#$ 6@+H"h#$eMsIDAT 6@+H"h#$ 6@+H"10k#Bsa?E$?Ik%5Hr$r$Hb9hIc9l$Ic9t$Ic9|I,@"i, $r*$\$}4Nk7\~?Ȣ&I%qpgi֠;!l[>2s>ñ)sF^LKxk/&@~;88SWQjY-Gb>P-sV1B.n%|_-6YS,JfͣE!U|vLƮDeyP>_U\g:>&.$$t=$yWBİ'3jbrd}+_EOZ\H;vïgJbnMm3+Lͱ;`Z1ED8OtE)p6G^? q8CT п\&FHsA H| s
h[u{sp۩؋(<8"1'wlO$B1.2
' E(b-B$'żaOmke#2 IUC5ۯuUM|+-d
]ĕ05{41܇f|MW1}KO.U&"AfHq!`!A_ɺ8Lk($8nvsD`!q]w$]V,"[jF+!P"$֦Rl8ZkB\/HV'#۩[<53ͦP.܇{H[}_fS2~ɞs8.$?v-6>@#j.J**8FbzDb5%2{*u.W1~IDATxp_ٖ*">p_#!
34ܲ"ݷ1iw*ZEAȦ;n!x^$IpUsG݇p|m=IٿW$VSXX3aEIk~_%@1&Ff:q_?1!'J J$fdx+'-F=;
Ģ֩,\!aq{ZP7qc@C=nNPDiHP71҉@1ꋐxY}1*z**>pH p"^+N!%"Y}nXL.0]K,[g%Ac~aRCJĀuAep4hkOvb7uYD|M:qWƕGU{m*p%WAoYDUuxɜ+:0k@)nΞ'o~pH"UM<\fz#rmm,i`&f_QT;F"5bșC<0G ?։nLjOlf}I6>@Xd;8Awf&.DbfWBԴ8;])1}36DcfEAʷwauq1XHxe$-R]낮.(!1\U)z8I{kBe$vNSXKՎj}3rkK0®9q)vLc8i4/S }m1DbbW6%oi{IDATm?p
Gi3Fe\W{+β5V/&5{
e|tToyq>-Q_6Mr-x*!9Gnm8e,<
nGFٷfGؖM$|=Ĩi|zfFN. 3$C>]T26OwS&-P;sjsxŹBDeYjO__cFlCa Jb=UfW|g#j`f>]Qqc2Z0php$M.ijW<$q႘5y-2wlnuWk5dhV5_PVgϷ#Bx}?T~G2; |~ûE}˛;1?CX$>@=P\iVPBrAɈP"+R|Jyl+zɋrxZ&_L3y.kKau<beJ:t*^
a,:fͣ?B~ިΤKVF?si|-MQmVӏ4f|RwK5(Sw5PФѐ[66vobԲ%E$&vi}n<ۆ01835k
0>!eI,bi$8&7{4!O4yI"IgI<&^{J{D8>3cy`MN"q8I,|XARHb)B|}NH8sRHb)B|}NH8sRHb)B|}NH8sRHb)B|}NH8sRHb)B|}NH8[%}ofXOgDp_ѭlTpP&LaM0u
s|9/pwAX٪ϔkFΌnC;!N,6gf@4^o~5gQ-YlOθhCvkg*m{b{zFD[b\'t87?^KGըIR_;IDAT"̮j0`CaU@!^En`X9+ĲDQPES6~!F(rR~h۰.tn?o?ÑH4ć"2EvkVuأ"Pvbu~7|{g4s'X;hъR^LO#Fo'ԈPi2z*žrfSzh@)A',bũ* %Yc;69OLIhY,lx?Yj6߽c˖eͩ.jU:Â)(W<L[ʾLF^>,&on_ڝrRdP5yO#u:``fS ٪,]
"9E0J}XP#<`MUy=溳k8AU։^sP{.{`C&Lr7:"0[#4?+B7/vTij gq>_~5;m
``^uܔtg?˱Kw[O@ CZxx'-Y4έ'NO\0X &[+x_ƹE{?%۞77<,uk);CdVWdݹ3ICrFB$P8ٝ{Ӧ0%5 "bEt0IDATT\ur \w8J* ur \w8L,À] ][z0J*Gr} }[y4L,
= =[t8d~pKIuo
~;LD܈
Iw~_\9TۣRMDlލ$ykWzil~YFtk\INuTD=.]9=s>VAĽm}kYڱ(*k⾑]cvcjC٘17G^H8Xhj,Kb{iysz1)L@&Ư[I̢#xzm_s'&xJ$:vRܝ됶ebGC5#b#bI.%͵ON`}h&7$~3D3!$q$I
!$L*>nI(COh$:Ds-7gZ\sS,ILL{ZdQ?dRMjqhvM6n*?_1jA|D_ɿ?
V+vb^$-̚ݹ]oIQ?,D\w|j4s/38ZݹM Xgzw]Ub#gwhX$b&5Q`͉k,Iq=M"QY1yށ$tt*UMIDATADAIQGlM26hrSk@M
@X(6PG^eY vJ=4@_DW=BrDMlX߭0p<ƐX"`~H8tuVC\E#:7k"7.
M3)^S0>
*75eqBVA@ DbnH0%Eu,51p,i
3y#.
Su:;&Dc:R;5{iA[?dX̶}g;6(ŬHKx! bz֣<{8VȣEb
uxDؙ6,= uB
FmGԢU+?
i@@1%ƨ1G"oDrcRj+'(05I$[Uql$amԙ2V:&<4>XS0(`!VIh3 J"͝'xaFw
IDATPE1kٚ츅hgŶuPՊ<϶Wth0T5Mi]?=ۡUyz'4rO:}sMh9(֊C 3(Kwh~_`>ZDC%zjbyx
Z
3sEHet\5 .ҝcƯ5geEy}l4kѪװVF~j"Yy7u7vzKzR4[m]lb$h1XA\;CX8jQZb W:eT$CDA3HeEN2XZM^Ek_~*3X4fπ5IiS_qwqS,֛2-Q(Ce5ɡj-lْɕ٩_D_kxvgqBkV+WDYA7ldrlU(0MBA3$sp%1b.E1‧k*[OxF cIV8^I\l_xԧQX{3@-,[c:K5xN<˜y
+H^pY}3o}Wis| ğ/ַ" &nY^Os\7_q"38s80^[Tz'!|CU%/P90@vS$N
>D
AwwH)YTϘXAܝ$"!ѪmXj5EaeӋi#@Zv(D[NdAԅqfql?Oݙݹr$$ԫ$^tƓDCRH?Dxf%ܧ*$I$EG@3]b%ƒ7`IDATt\0#*pׁ.얍_o
_+?%[ΧhߔÆm,c*5$$^( tE*k#wH]$$%1\/]D<aZC?'<7fђ=I劽
k"kbzM$ ȉAD<\YmzPb=̓;[_4gwE55&nw2#FE'w`C>u0Z늡<í3okB*tXXY1Rn!M]0IsȟhKfυikKoh?PpV͚XWȡ\0ωY]sQba/?àϿF19L!{Mj"K
a?c2ŕ~^I{sg$q|ZܮI\+_ﵖ$7kyF{%Zĵ^kI{sg$q|ZܮI\+_ﵖ$7kyF{%Zĵ^kI{sg$q|ZܮI\+_ﵖ$7kyF{%Zĵ^kI{sg$q|ZܮI\+_ﵖao&>IDAT$7kyF{%Zֽ%"XIENDB`n^wV@N`V,PNG
IHDRU$gAMABO pHYs$tEXtSoftwareQuickTime 7.5.5 (Mac OS X)53yf9992H >4Fr@AH#}i ecr{;FqGyN2LQHY7Fnn6t#pI!P}@rj;a1Vw,- )//#>L&+!(H:n:\"Z[[+**%&&6@[xݔF} y111wENN+c@qWOe^")DcȠ
o|MZWTgb0ʩT"+%{/WEyiw͚5ۯ_4"횄$t#|
dxŋIj)Du_G<渠K.(͟?ժU?#%99
͐s\ruڅ$XUUUYYYQQr˞ߝHX?Kϒe>jxEs\^>/u{ٹs'uCCCOg3yźS|9QaVLBf@@J8osCB̅Mq%Q QGUTTPpJ|/^477oȦs\P;s?SAKRRғ'O,Xv"B̙3hC\6]rL&IN2eȑ~~~"8拠6$$#++KSS3;;wDRrE%%%?rֈ#lv]]fllܦgჅE^;w,%;'O{"""&N;.P
(INN^ti=VXp{ݩ=myy9sP7>EMrrr~G99N:5|p%E"/_ɓkעćʴFIJJoj˗/D]fEEݻw/++C!5ҭ[p(rb뇒ܹsee8jӦMQQQ7nhHEiiA^^^ILC5/Ɛ(R}Q&8p`||S4!{駟={&ІZ:wܹs*Dc`p]+++ԁAٳgQ2Z[nuuu566NMMZ}dd$J菠
]a|H~;x apݻ'9z)))W^͛7vBxT\t
wD5]֧OUl4}^ X{o9cƌ-$$iq˖-NB&
EX:FEEy{{^:++u0qcǎ̞=[AAի"~*pkmmW^^NRϟ?/FN~Pw-{{{-PJUSS'R r!!!cǎE[5//[CCw\U<λdVzʸEs i״@բ|Q[`ɼp·Aʕ+t|# yyի222.]:f͒ćihh(֍~IRSSQȒ,7nL6
}233O<9rHA J娗:Vumr}78 I38/
6}iIر ~qٻwcĠ:u6]RUXXog̙Ѹѣ***ɭy0kA[ABHGG<|/={\vӧOh
mMF]>}҈A+nz;
3668p{߽{'DɢoTTTs[ ''GQoS:wjjjgر#DӤI._laaqy5w˖-^T] >i$Kt!:t--ӧ?c`l̘1111vppV(_77'3&'p\:tx*Dkjj[
aquHzfYD@}-Pxĉ$̙3p8'%'M;ӲŅuuuQe
v'-
O%9ڲ̨S&:L&Gx#^233Cwu8kڤBINiw * HFӍnýNNN/^X;vŋ8pet˴i;.fBY#g$#5dKPmȑ,Ru&&&۶m[{gϞU6aa1hN?/\`0ۧ6~xTԈnj"{JJJMBpС
>)I tD
5jԐ!C9fHjy7KOOOuuuO@͊>}:*vv`
;֯_Vz"##gϞVºn<8,,wtTX
Gfff{̘1gF?ܽ{;wޚgΜ@}dAIYY١C
CCC+++qG$@}aaa[1!!ڬ*<<|^ڸq/ҵkWA+V@\ToǏ\(u}ׯ_߷o_AEE
߽{woYfff˖-suucx_|hcǞ;wCA`zz:ɇf̘
+W|,w=șMA:xgϴMMMM;h'NTSS
%***(ۣ~?!#~*//طo_.]P3|YYX#իW&MBӓ\VV6k,$%[܉}Л*22rYYYݻwTKrrrPŷj*m%pllltŋh+^tѣGk~~>,%%wAԩSHH)z " 5jT```rr2ʆ#FXp;ܿ^
uȑ#422*((h[UpN.ҤKUUL&_zw85z}ua6(pСǎ+// *))OM?~\EEW^ܹsCAxܼysԩ}ݵk۷oÇQ
%;yccceddpE" Җ.]ڳg5k={hhh={k:Ԝs֭ۍ7#m`诿0a͛ǌ#^N\+_UZZj``oJd!I4]p1(G귴RYYioo7!jjj6$>v!C:O>2ThhCn766;zhP=z4zEY?aDԝ;wf͚ջwm۶ݽ{ 9֧Be9s`VիWwڵb
*p%-|if0ubŊ/>freIr<hSꢤY7 jl6zӧO~.pI$2Z\@C}fsx(**@%[-(tYPzj"OlD\*z3ff퓔ɓFr,v!aL"a;PDd/SBmW)֬YtFd1kGTPP#Vv A"reJ3E£X!ĉeeeeddzԪ[Xaqzz,EVn|a:}"y%;lN݄dgCCIj߉@sbO+[䬐NJsoBptwzjNT KeOOOTΛ7oժU-?zxg~EHO>`@NV}aT2dK[jr[+|ҜMpڒN:)jz=3, *YEC Y"&P
XӧOsvvvuhxE
N~^"үHA'阉#3bI0%͊)$H:zcdAudpJVW3- _
8ۏŠJŠ;PDyN"AW$`Cĸ*O/v9]ez)зL*4Fr@AH#}i >4Fr@AH#}i >4Fr@AH#}i >4Fr@AH#}qeL&M-dLnPkƍդ\Ή\'Y}\R~r
>L&+ANۆ
]XԶSV@$ ݙF&Φ␕Sv6Ah9ԣF؉uz}C(d@"5EvS?֭[L6ʥL.)Oe7K$)*&Sٵy~ե> #ٱW6{9G0_ic؆>@F9J]daĘmd756K&Å68mG+v-$ז'q^@Cjy J5ǥ{P39^dz۞꾯pX@4%&&'/trR_z7D7\.+>x$Z&I^^^{UʙgAeG4EVVXåepjmBkQM;ܑQIIT6Ҁ6- <nۺfm;b熄.jk/⛺ F111(/;vر#pr%8> e*++o~ر' }AS7ݺuTRj%b4U;uleH4uoDWDDk$2P}RQQyCCC}qOOS7";;廗/_}Ο?)㢰<4fsw8j<|͚5yyyo2vl͔qS72{nLLpDs_yyn$+[8e\$n P)))VVVFFF۵kWTuܸqS7[m6___ܱ}{M;ݻw˖-IHHpԍuTVVz{{
2$==B#G0`++VPQQA4w8[r,ǎNҒ}e˖HT͛7w8`t9i&}^tCCHLH|@:EGG=:..!u_rrʕ+eddn)=6\6m\YRc9~x``)֪'uttt4iݻw!A'e4"'Ԉ//Jd~1??ܸqK2s_HHȐ!C>|:˖-Cuc0rss&g`a @^fݮoy/nZfMqqǌ; ET y³8bNͺC.]U Gr`?m۶uI@\DZ3Q;Cv,NR]z{گ_?iTT#n2T4ʳ,!}}xbÆ
iii333zd@ڵ[bcc:lK\S0zOn,IRTF`3驯o``cH|v8`KJֹ `22]̝yRǟ=7!FE^Av.Jxn}aæM3|P]Hٜj5BX\ZψfTWZZAB4Qi_E uߧᳱ].ڵʕ+x,3&a,s\J6,3jh=3b_$_kטLfO @New7.>#HݺuvC,z߯.*
ưˌH ;]Dפf|Ȑ!ﷶZHB:Jw*8X>(,[l9uvIι3Lqzr^z:::Jdn
zz```>Gci?MyoDoǎW:"'M?[%LYE%xЁdKNN9s&#ci7mt-9sG`ki^g%%%x
}
H;
6lO>f">o2%<<{.w0tٳgπ>|;op۫W/e7GԈ|d&s\,,,/^6|C~KVQQ5/_}7n۷}СCÆ
---{@"ݨQ!4bP_QQ~ԑ}UUU}[
?~=wFFFsXə:u*$ۄ-{⧟~*((NEEE|C IDAT;w߿?j4 էu9, aD*o۶MRG6yUBM;MH#Akcr_`` SoWVV3"##xge/2C!ۻwo~q"233MMM]I%N\[Pj=TOZZZ^^^o߾m ЁCObeF;/^ ?'k
'L>>|m/BRPFFky +:o|;vsڛ7oPEfiG%/Ͽio
i
8kkkAuߓ'Ob-h Dm9~KOO1cƂv%oKQӰ&H={rl
۲b0r===d+5ޥa?x,\w,⥥$iվ݈~=Q>8p@9sgz^o7I? JCYrqҥ1cE|@1*:ͱPtu;s6uz1ƴmc̡C._f]:`C-E$NEEzOxw,bB8F2S|(ŸbHqϭfĹXm/sgg"?xӦMGҥ?ZMܞuhlLݞ%F4iRQQp#x? [pc/3j73oqI۞/iA_N6HpxY2Cȇ5 [lk6 h oTŒKisg뤤$}}ORVVT =/M0jJ0+ޮ]fbbcǎ?t n6nbU_y:A,msgx؟װ%(I
*X@ٳܹs?X$$ם{dn_=M2$sF2n,G|z?ڵk@S;,W0@ĵˌ!M<D7=,хpwn!xܜ̘뉰hupl#qq@wgna]rss=8@; d
߸qcĈ|rxF9Jdsea
@V!~~~SN} :0MP͙3͛7&Mw^߾}
r}̘H}v=5z1LWWWZ
VTp
%LҡCcm6r17tR.\nn!܇t ;RRR\]]M7={6f̘,ሽʸ 9m+taoM(^;w3g3Xyyykk*++9wD{8㬍4FA4TOd٭%ٳvDϛ7OWWݻw8.'lv.܇ddddS
]x_ʕ+!!!'MeZ#.0P͈Go%!y())̝;wܸqf4>}ւ8P[:ְ:pUՅ`]3l@]$MM)1rxoyy.A5|7?~p ^|9~ &E
vG?fxLˉt
/.xфLA#A8f|FY>JMM</
yN6pOcbbFy%4VU;kמ^cf=Dܻ/fS7b'_%%%wӧ0!*st~8q`Ϡ*̙3۶mKOrY]H%.*0uVq뭬M{a4%:sЌ3&99LOOA尞_uI+ ]D/#QeO '$Ía{f?lZM
ÙUNG1g7쇷xyh`#$$qܸqG~o;vݻ߿,Eɂ$rsGԞm ~Ն
xs߁Nɝ;wp#TVVV3gΜ={6:Hd!Q(--5jԎ;^YYYXX3j^](W^UVV߹\.X.//oҥ}dX8Q}ׯQ/ZO<̙5nJqd>P]]TTdfffddRX}֯_>۶mCUp:qcΝaaak
h{umPKOO?aRf+hSP*]pзoׯ[ZZΝL6tPԱEIθocJJJѼ7rX7Ta_nݰaFO jƨm%b럍
$˃/_ܱAYY:@KPWGOOݻp=5K.rEyyyll,ǎv:u͛7\jE5WvQat.@u:0lF;w8qpu,}Hʇ矓&MRPP3foޯml] '|AmaC
477RBKACm3_7++aQOgQv+=lo{;-%/0Бl巪`Ѩ
Œ ~!FDD>o~l"HJM/Wv8:5?䌌LE]Ns1Q\AD>e\63%x]n&5'oo̽{H
6⥓ŵanB,*9:#"t6pQpU<:ARQҬk֬A)y& `w
m%RIa+FN0b֡{GSs~
55˗38&P p2<(
Wv:88-BӅպz;S/?~,##
@+\A^'&4tw~GzJ[[{PN`OT.[l3+fbĥ
3LUqC0URϞ=۹sgDDc-HBCLM"##?>i$ )իW7nܸ~za#}@1T۟8qB SNݻwǚeeeCBr_3348@#bp%lmJ\ؾ};wnݺrJ99)q®_~m--wP u_(h=ߩTofoo߹$ u_(hQFEԺr劶Ç9EP&{FF]+rka]%ڸF}
aÆA(9l67V?cTTTpppHHȠA+++<z.aUѿbqeIxG54!4J Yo
67q} law'i ЍJd\JJuZ+$=Zcǎ~zGb1dF>C*{J;C;vvMC2"vAaB2$s YEG/)d~mT" 22]̝yR"yIQ95'%wHmUjOn|ɿ9seq<)~7oTWW///oQ4F@cT2WcPRFPCk%| D:cv;#bQ;Cp#3?ǡ%@) bcF&SՏ
숎:}vP=OiC`jj**Em$42|A^vJҜO&6Qܥi57sfyQJ"B_h\BLb7GDҩs)vZ fYiNq$V[GW\/l8k Hh҄P[bTJY0 9ź3y[RORnbrYmQ"Kt!7Pd=^vN&H^vOmT5+dt~ՊښpS,ϳS?GPkgB/# ?CĹ\5_3εXSBI tD*+}\lCbDלˎ4o;<ߑM!PP/]{9A-̝yesrbEҔjl.Aj6O7tյXXb ZUSZB:8-k[\?ιlw[W-.dtjK+@cJM$}SCZi| ԍ'KDI27sS5[x;t{h}%Q2SMII
))57[ą79(OHlr,&G~i'w(hڼI/)ʒ>E؆G4E~$>$Im)<1M'0Gtc*9bk&żU43$5YwSC4iٯxIݺ@@H'}i >4Fr@AH#}i >4Fr@AH#}i >4Fr@AH#}i >4Fr@AH#}i >@kpl&@@9ɘ3
=u3r %薄rI!9$kClKBqUa5YY
ipX}^a
,~x~@wf@Sv6AHH1%gv zt$3N_"6Vxvp%A4Luu5mАMQ/Y}Ӳ%Kg%V4`ʮMI#l6WN>n84>hc=l7*rÏ>`PBJ?3QN(%i$<'s1&>,ص`yR9{iw *]s\JE<#9ܞuhlL!\@<<}ΎZa~W~8myn&_r,&G^= TBpQWYYgϞ;v]&%ͳ ɲ#rIKd'4%u-=={
'Nh̰vLJ̨𤊡c
%# \G]ŷ|rH ,Yү_oÑ@0hpww733۸qcdd$$>;;AGA'p6qm@\v<;pyۀXx358X();;nckU{Qe0Ep\tiذa
?ć
b %%eϞ=rUU!!2ATw7CqAWr^P۷o[xYcccPwN>}k֒9.?ޡSUUE$>uڽ{wAA-[.\йsgtL0nNKק(www1q^RUU^eey:v܃aʉ
+5җgrC)D:uCYYe=h.$'o;}ဖ@>9rdzzzǏ@hx]A-!.`':c
_r%228wI2$s M/)a܇ǫW6mڤgώ9wP]&y[<"po^^@s [NNða*++Ҏ;6h A{ݰa縌5j
)))MIJk~2g~5_`a~/耠$$$7̻4e9.CE)SMvmтT?5BX\Rɶ /?Ν;}d2m۶}^pŠ18gGRiլoG<ЯTUU ;b9I}ٹ+-GQFHi{###MLL>?}"iT?[[GxܹsGFIHoIDATr_-V#% Hv\^`Ƨ}HHȈ#rE
k{Foyɓ'L:JD}?˗1`ҤIcƌ,իׯ$\fNP
/JІX֞F}
- k֬Y~=S-\h{
y4Gs_ںŵ+j͒3IpD*--EYAAAjo33[5J@
:;ǅd&##i%Qnq٣{|@`bccuuuUpQRRڹs/Pz̙s݊L0$qwۯ ґ 9x&Lh $( 8cqG- l6IUUڵkBnɓCE+++y -Ņ!3ݜ@
L
//14д{fľ0BI^>|y`.BU>:N:-Yn`2̵rq'v"p[肺-hTJ\qý=lذCfq?@pR/>>~ƌ}ݳg:a:}Xa-ȆJrzknڴi֭L/bS|%ٳ5kӅhϟO0ŋciU-By?/
Q,Z͛7<@rt8vfX1HFӍ>|Fǌŋ'&&n@WbGT>;3g ԩpDS͊9J~A6up9-vի=z$''7+@:8/:,' 5w.0[r$]Ο說Μ93cƌcǎmܸw,"w@.xapss2c'qDαԴӧ\"6Α4yXf*_;lP'Ç}x#)
2Y}u8 5Mݹv[PP`ll=XG}N4f"x8CNNN7or@ik_%Bs3Td&0gĬFu_ppiӎ9EY#FqA=Sh@ C
m߾ԩSiH! fabz1ѣG4
8"FHuŲqFbb"$>_ˍKKkر{i``)@ QΜ9sذa+ksi'''___ܱ GR---[e6@fϞmnn-Q`.]\6!dIrr!7l744tɇ>|xRRRQQQ^^p%ϩy*~~|POOM7NNN.\X|{UUpگ0>kӶHV& 侚Ex=;v}-O?ѣ;wqGq~x~\1Y9ykI29mhB:%%7oO__ٳcǎQk}ZA$±1hC 'Dr.8o Wo6lKkOݠeg(
VwcCd%np>njfnS`Q ̙u IOF9Jds*:ͱPtƗVzJ44uz1Tr
vrDˈDGHڷ((//_rARSSqҬ7o˨$( 4Z1QCv}
8V3\,2.`,F2$âi@tdr@@p+,,ܸqw}6-as-G `҇
f0$1}t\Kڝ5" 1fSdF$#? Pb
6;ϟ?Gɩa1h9>> ئbŇbI!LYe|7Dьrss1Fh"}}>}dgg߿_UUmXn6no!Y%$JY&qٷo͛78(((={CC+W?|6]v}qjEGe&76 faR:MGF3Y/#'SUۼysEE7W`sr\xΝ)SeeeiT:wn1FZZZffرcQ·
ѣܼXmݸqz3gγg6l
@3Q~)@UVVZe|.:4 @h&lCRSS?u
CmI|o>~=!Js(
6%>P3ÇR
#Fx&Y
ԛ2e
z@-OUQQqA9rÇf͒W5_:`N>ӳZbJ"!-x
8u{UTTP:4Me3-GX,O>}msssAZ$=*gϞ
33"+phs·P(d2ԩSwS#b(K8*wލg\\_$>vee;/_,%+A#,=q#ӇX-3)͛~MQQqѢEs=v:alH\4Z?H0P[m3+srrٳ+?!D0a˗/qｼ444_~7ndtd&xsS54/P'OFZ;6VUUgT^pw,h۷ں#qqT\狹U8dɒRlPWGFFf֭NNNWf%g/䖽~Y[[ŋ gΜ>|x&Iuxsc ʀ1
ܵk>&F{W0%%ݻwiii,֮]}rrǿ;A60rXְQuN'N,^xݺu,o3ϯ8y$7@"++kҥ[lAupt[[[Tԣw,>ӧF|-XUGi}ǎ胁; ϟWVVvuu-//}M`bb"wm|+ZfΜ9iҤ~!//ݽgϞ0{ԴѣGp]SQQٶmhVӛb}m5&&t8H'OgݰB=Fikŋ7NO8>XuiC'Cu%;,_6EX7GY2b"$Nv蒱ď,nTc
"1X0
(STpז 鸙BQPaHWa_)ak/iy}9Yů̙3JDDDh0AkLݿxܷo_+W6&Yf͙CtqqwaL,]F+%)o)--e!6 ^ŴHh:B,M,ǽPGFH,MsO:hE>u{!OM7ol??8*gQZ>=`P\?ʖ{.7%*YDT*MJJ"6.^sN-r'1WʇdS Sճ'qewd&rhmM)+lg+sbg7S^n.}bo
8|PԵv:#=bboo\^^GEت8Nlf.ADC&-<{9\ϮDz2磟 HB1]Kb2϶jwARbt
#fǘ.S{цT\x4?XL̻߇W[XR MvlsyWfG"2Nkx^);Zlu{Dɕ[Aիiii1p`QU\ڮ!w2S?{nhri+-RaDqqcbbȶ
w}}WڠEy' 4
#*%<ګNza~J"jLV^gmk+啛f8c%ʉ{a:9|!*E#ueq4ѣG1۷om1a8kԓ]x]=<b[`YR8`|D)9n<V*kr݉MރoBPL{IeիW5tUe"pB.WLֹ,6YPՋ2$g~YD6Cѵ7oLfCD~|P]vٳgv+ |%\e]c-:t]?vѻ'z"9BөH$db%&Ԩzj5@aхQ/-x0ϯۺ\]
=ӧ5[a=!nuii'Qpjj*d[P-Ueh?3v5y]پ?%Rar6(
]o7))i۶m(ljm{1JOYﰮSpR!㘭 GCCCiii\.ԩSd[PC(eo|^e)톼~~~~2Qՙnnnd[,~"Bʹ!*65ӀH$
RLXXؤkNG>===)))@8:::>>Rok?E>iqerǳ766K)[l~U:bZN;Ȝh&yB6XH$2맲[ zR\)R(rq,B:
9ve,=V:ZE6ºu._\WW
60LQ1bX8=9h" 궟Vz"*;um&)=0t#W6G!<A.}ookݺuK,oܸxxx%V`kۂ
C('QҤy1Mdh[VTT5!H}g&kuH_A7z)<`QYYYcccjjwjJ
hqguj`.Q VU);ܡ:(,unY2ZD;^Zz0ƼTSN:o?,P?yc^*aR?ʋu8l@hk/850[Ƽ"}"}"}"}"}"}"}"}"QHi-hIENDB`0TW}
GKaA
W}
GKaA
'kxTnD>6ٲ
AbıS^h/kkv"T ^w@x`߂'pfƉQf<}d<;lox\
e;3"xEӼC}-dށG;Ǘ3o tV
#{-unX"/3Ғ? tK7}xx$= C#Q3-R1dbt5@o8?i|+B3dk{{ijXkTn kw?;)%C5D,FQx9csX,ΐs4 k<K}²pEl[^Ap7lb(^\,9-xZӤoK5_nt9J2VRjo.f940 ]+Zd2~^p :2O>Pd57K٢d2HTו]7EkE;^J@ttǯYB@z<+++lp^:mjqԩfff˗/\ ;m4}Çggg+++kjjǏ߸qcСo"""<طo_
2EQEEǵN81qN>UUW_}~ww`Hv @6)htǎivTTTc000+,,$=o߾YPHRWWoKb?_hg_i8]Sd[jՐ!C>#T z[nuFfGߟ2eߴ4IOl۶ܜfggg߰aHHz8ΚoIIKjjDRBw
oٳg Yy6zCRАBdÇ_lDȈ Y$vvvt\ccCCCIJ[?TRR(L}ժUO>% &]h?GYf֬Y"'$gxM2\ۼy3oΞ=iӦ2Ν;W
g:rsĉSL!8{lُEbÍg.urUUUEEE˖-_N8q9۷?~d:=za+++ee}Eٝ}i<<z袢"P$]6q?|Ŋxq8SNUTTݹs?$kjjEwr͒GSMEәv8)g|aO}dLS]U+ꔧO_Lg32I9[tr|,Q^ʒ-U>muV2y r5χU?v@yHݙcDd֊y?8}Z),eƩ,L!Mc4-
[BYY,81K NJ_xctR[o^]]-rz6+{R;Z@O>-o돌d;07C - 7lJ[$\埖Xh
mmmJb m-`yxWBBB$D^UI&y)g!L)No~;M~.o3[NdH҃[^gSep&g2eJrr+682V$F,ȞqӦM"{FVඛ>d/Sxe؋?""BT/kD21(F\zN%[JoPXf:Hђʊ{;MlgK(HTIFt`߾}܆0
ȽHYs{8wWoglM3(<h\E^,>Wncz2ZSrEElv666jϾiV,y}9'
srXr*`}7]J*97:*m;tcR::wg}.ߗa֕T
h~}]k2z$/_cBM֭[,dfdd\v̙3'N.躐w߭]1,,ĄK/͛:::#UUUKK7njpH۸kO>$I"ԣG۷oүWU#ZZZ$ɸ6$"y<EɱL+prr2bhd0p¹sȸ/11Mݻ@{9r$UPH7fmm}ԩovͣFUO;?$#E]@3 }ȱ011Yd7 Çуdٳg?ǏϚ5K__t݀?#22rʔ)l6I1cՋZ-Z<455srr>}jaa}vrdHCCChhonEBOO>B,LA2{.]DѣhɉSN
8͛7nXvеdFӒr
˗+++!#УϯpǏB()NNNW^%0gΜiӦ]T=ycƌB,|A2JG~~èQ|}}kjj.J?neeURRbV\A2JƪUmm۶q\qƅĵ\@ gϞQQQdmiiIRCדsss?
+xsHF233###G1bNwEAkjjnݺ矫]@`4mFxx8".
Xe˖q8{䕠03?srrzw.]ZUUEwE7իEP$HF:/_@SSFlB/z=28ps={F}3(eEqq1\_reͤyVWYpu2|VQQٷoСC.@"%==/<Ņr&88~ںuܹse6: f͚O?tʔ)999tWԬtdCC,bC2ʢӧvrrZdi,$c~;wXt eAAI>yD'Oݻ$2igΜIϟ4h #2{L&|>Ϗ|kذaKBC{&?XB3M#7^|?Ǫi}||EXO aZSSs̘1O$sIfddڵ], 0'7onNr/^g~iXXؐ!Csssšg>I1#;vx{{3/dwo oﯩY|k_HFHchϨ8kenfl%g'
Fӊ_w߯A͢#jfsbYOlt.@gTXU97o2(
$ªH4EF94?
fQaCs<&dĚGFZJj=SqmV&^jZtWrwOKmu9]uaIkZDbMKͺMʲJ6/ֈ@o^OM-Uә<ÖzɏHdLV#ӟ3UTOR;~~__6`Bzf&F-rwZcfaTN15E\9Omlռ XC&39"U94@Ggq1~Q.LRg!Ú3Y!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!)555]HXŀO[rt&ݕ<JC垆FcT[UQE}+Gw!d2^;1]ϟ=@._
UCϨ2c{(7&.մ-,,|}}gΜϬ6v|op1HzFEVup7+%'ݓbI،O>r,`ڴi)))|TWװHfb=.ѲN9Eo;'Ԉ"
Ž&Ŷtك
D/T{#zFE?le+̫jroV\d$cbbbHZ;---E/j3Sk!A\OQq*ˡ.9֑Z_[}zj2jVWW'}"B3fxvƜ_PԶɊttZN=0L&.((hѢE T_[]z.m'}[oEw-
>cܒvU]zF9VQQQTTT\\Lnhiiuw/88xyjjjtWY7Mŋ;:::88.\Pb7novСٳG輳rH
(C2Jճg8`ff~ҥ]F8>>ʕ+&&&k֬(@2JilllǏUMicccoܸAZc˗_t.HFixQ;vo#G"!c:;;qK.{.EQL2w\?ՕS|A2Jʝ;wH 7n yyysEp3HF0`@QQ:EdQ?~jiisrrBBBuFwQ2է8;{,i
+C2۷oYnnwmhhHwQr@KKd|M:9s8;;7oLիt]>7Y?^|֭dHwEgꅅji-/_`0$cA_``JDD]"hlleXzzzsT?A $xݰ>rGNNIƶ j}}ׯD 5a3gW2F,uHy~CYYAcΟ??cƌ+Viii]?}IvMM
3d|?5|K.
4_g|aO}dLS]U+zs8-.`DxJ^^ܸwbݣz:\h/+K`4/o>䋜ёX|wujت9ӱd3w$_a1L%%E-NO]>Ini̜3bĈǏi;&oFMvٛ#\+5?ؑɬ,%y//+Wbd/T씘MMMuuu`|7l6eJr%W
0)j[8===Yh
hIDATIWLfFRS~̗.4Hzƶt2xep8qqqƍ366iSee;Gz6]KvӒYLgbL6-%%T}{<>e<Sg7v880i첋,:~KKK___dENyةKt5uٺt)+yղZ}ļ6'APkVtGq#Fp^/K^_IVJ9tugTXXډ99dmɅ&^izmR)NNNǏohhxlVs)dA8ddƒ/|H
b&%%(Ќ48GMNN&=KK˸8&:)22mڧOd:;dȐ$TVVի˗هdaNNNiii6m
ttttɓ?mҤI|"tW=0R䵽nݺAmٲttW$ӲBBB\dw|[Hw˫Օt@s:3ܾ}{̙&L -vqqo9hD,$#z|||
.]ZQQAwQ"77w#G$o.:::k'7Hi===J+VPPEdѣGDDDVVVMM֭[WRHo8oQFw,Harʍ7LMM%%%,'
իuFwQ HFxC N:qℵu||pΝŋ1o߾g\nNbkk/|7C=}4ٽ{>3!!!mOI
b裏oܸqʕH|||HwޝdMtDQHF77Ξ=>
UTT1mm=z]HIYYyy?~q<==KJJ.*++⋁䄇ՋHF?uuu__bKKK;;e˖UUU+W$766}{ǎtA2[.??_KKkРAk֬yPV._VMMMPPD.K2q].
hdٳoy}3332>H^쬬ݻwݛ@& AyoҥK]#"H|嗤jk{-o\;Ǐ755=z(Ǐq{0w2߰ad,XPRR"9<ϟxG>x'O> ͱ>**j]'O^~$4#PHFOz֑5 GiKwW_M8dx3Lj]Cڅz~ҊFDDX/ F,B{gڔCII&Af``Й''!_3&$$ں3]
zFMICBz:
uuu===]]ݺ:CCCr;w.!!d Ēoڵ蓤zyy9rÆ
CuBWd9H.3|O5LA2o"|-L\m܌. F ?uw5/:f6'[A3*>or*FmUCSEuV"PXHFEZGE|ЬүG*6e|Q%㏻Y~ѴBIT9ibbp3]nP/$8a[#z+EdT$D/PUS_u^wT!mk9:;ˡ4
t6Aa4@sD2ɃC\RNF]}#"HWC9bDs>EY'U?_\O3APJG}A睗:7uKa݄:QPO[rɨ8ԴZk͘:_@x}nm6f5C?Ù:[F2PsjϏE]֮ޙ5)[:OTDh3kF?|ͬd3W:ߺIQexPRWժlZ'P@. OŹPN]E+@2*!=Jvt>*5plڦU W0V0Kϱ.i̲E@ !!!!!!!?6_^EIENDB`0T3c]FRZNYBc]FRZNYBvxTMo@)F*FXI48RʡR9V*n:B%H8'fwĕΛ7o5d{}xlNar
`nZ<]}%/<UwޞwD0`;xdHqd?pW>\OtKƳX<$8INڰhP{4 ,lKP2l]VbPs^"P}hT@c(Xb6l9W%I>CY:;ұk5LDa;BΎ VcsI}tVމSύm,qyæ̶ cPcH$+B
3B4u̅b~&ț}F;
yk#Əc}61]4KB~HoܞGO9rlFV*LvÄyHε)g)PΎ^?C<[o(r,9ӢRTɪ^GV5
tB2A$ Mu>d2))F@HFN[+ KOęF-cP*+6MqWϵיk[
2;6:l;쭭ntfBdoD*E4*
YVIVl68,
iJy,/%zǞzzqVs0st9HhJ
[43B;lEoGĽ3#[2,s=ܣh+{C3_K 1z4oإqo.XAv&ܹHdW8+|jƨѱ.>f#usD`\"Q1tGص
} ݆
0ݮC+녘ɔOLTA)f,x'Ƿ;"2#j=-uHkkW]\_7o=9(9CY~4x&)ZeXΎ eqD:]Faƶe2%Ñް^\xfr($7kLJYDe8-%X "oTs)Z9.gYR(G!:,ǌ*KHEHaJfHq
DA@DDefault Paragraph Fontdi@dTable Normal.a44l44l(k@(No ListOFree Form AE$$$d*$1$@& ]^`$a$-DM
Y568:;<7S*CJOJPJ
QJ@mHphsHH*>*KHEHfHq
O
Heading 1 A AE$$$d*$1$@&]^`$a$-DM
Y568:;<7S*CJ OJPJ
QJ@mH phsH H*>*KH EHfHq
OHeading 5 AE$$$d*$1$@&]^`$a$-DM
Y568:;<7S*CJOJPJ
QJ@mH phsH H*>*KHEHfHq
OHeading 6 AE$$$d*$1$@&]^`$a$-DM
Y568:;<7S*CJOJPJ
QJ@mH phsH H*>*KHEHfHq
O Caption AE$$$xxd*$1$@& ]^`$a$-DM
Y568:;<7S*CJOJPJ
QJ@mH phsH H*>*KHEHfHq
O Caption BE$$$xxd*$1$@& ]^`$a$-DM
Y568:;<7S*CJOJPJ
QJ@mH phsH H*>*KHEHfHq
J&@JFootnote ReferenceCJphEHObFootnote Text AE$$$d*$1$@& ]^`$a$-DM
Y568:;<7S*CJOJPJ
QJ@mH phsH H*>*KHEHfHq
O
Heading 2 A AE$$$d*$1$@&]^`$a$-DM
Y568:;<7S*CJOJPJ
QJ@mH phsH H*>*KHEHfHq
O
Heading 3 A AE$$$<d*$1$@&]^`$a$-DM
Y568:;<7S*CJOJPJ
QJ@mH phsH H*>*KHEHfHq
B@ Body TextE$$$d*$1$@& ]^`$a$-DM
Y568:;<7S*CJOJPJ
QJ@mH phsH H*>*KHEHfHq
6@6w
Footnote Text4@4PHeader
!4 @4PFooter
!ڀq=469
6666666666666666669
=
!z z z z z z z z z
z z z
z z z z z z z z z z z z z z z z z z*29PFP%Xbo62d.2W=
-D+
mk*^45G{ab6Lfq;<fg]^"#)hi!!!!%%((2,3,Y/Z/1122222P3Q31424}44499;;!?"?AAcDdDOFPF~F$IKJJKNPP9P#Q$Q%QcQTWXZZ[u]]K^^@___;abWdfffg}h~hiimknkmmoo,q-q?qTqdqeq8r9rttvvsyty}}}}?@>?@xy
&'3456S)*op>?ΩnE@}'(jkz{ö۶&2>?,Idwøָ̹ڹ(IJǻȻջ(HlmּԽս,Ibƾ 9Wȿܿ0YZv 23Lm|
5Mjk
#FUq@Agmn!"UeWop"#0Leuv';Ryz%&3P_|-.
*?Oh|'(5]r&:cd
<Tj67Ff9g&lGH&IWBC\6789:;<@yzDERd)*Ci*9m*Su=>bcm:xy
$%92 B
SH
I
8:;>0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0p0p0p0Ѐ0Ѐ0Ј0Ј0Ј0Ј0А0А0А0Ѐ0tЀ0tЀ0tЀ0tЀ0ptɀ0ptɀ0ptɀ0ptɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀH0pɀX0pGɀ0pmɀ0pmɀ0pmɀ0pɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ 0pO!ɀ 0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pO!ɀ0pɀ0pEɀ0pEɀ0pEɀ0pEɈ0EЀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɐ0pɐ0pɀ0pPɀ0pPɀ0pPɐ0pPɀ0pPɐ0pɐ0pZɐ0pZɐ 0pZɐ 0pZɐ0pZɐ 0pZɐ 0pZɐ0pZɐ0pZɐ0pZɐ0pZɐ0pZɀ0pɀ0p`fɈ0`fЈ0`fА0p`fɐ0p`fɐ0p`fɐ0p`fɐ0p`fɐ0p`fɐ0p`fɐ0p`fɐ0p`fɐ0p`fɐ0p`fɐ0p`fɐ0p`fɐ0p`fɐ0p`fɐ0p`fɐ0p`fɀ0p`fɀ0p`fɈ0`fЈ0`fЀ0p`fɀ0p`fɐ0p`fɐ0p`fɈ0`fЈ0`fЈ0`fЈ0`fЈ0`fЈ0p`fɀ0p`fɐ0p`fɐ0p`fɐ0p`fɀ0pɀ0p臀ɀ0p臀ɀ0p臀ɀ0p臀ɀ0p!ɀ0p!ɐ0p!ɐ0p!ɀ0p!ɀ0p!ɀ0p!ɀ0p!ɐ0p!ɐ0p!ɐ0p!ɀ0p!ɀ0p!ɀ0p!ɀ0p!ɀ0p!ɐ0p!ɐ0p!ɀ0p臀ɀ0p0ɀ0p0ɀ0p0ɀ0p0ɀ0p0ɀ0p0ɀ0p0ɀ0p0ɀ0p0ɐ0p0ɐ0p0ɐ 0p0ɐ 0p0ɐ 0p0ɐ0p0ɐ0p0ɐ0p0ɐ0p0ɐ0p0ɀ0p0ɐ0p0Ɉ00Ј00Ј00Ј00Ј00Ј00Ѐ0p臀ɀ0pɀ0pɀ(0pɀ0pkɀ 0pkɀ 0pkɀ 0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ0pkɀ(0pɀ0pÀɀ0pÀɀ0pÀɀ0pÀɀ0pÀɀ0pÀɀ0pÀɀ0pÀɀ0pÀɀ0pÀɀ0pÀɀ0pÀɀ0pÀɀ0pÀɀ0pÀɀ0pÀɀ0pÀɀ0pÀɐ0pÀɐ0pÀɀ0p臀ɀ0p̀ɀ(0p̀ɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ(0p̀ɀ0p܀ɀ0p܀ɀ0p܀ɀ0p܀ɀ0p܀ɀ0p܀ɀ0p܀ɀ0p臀ɀ0ptɀ0ptɀ(0ptɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ 0pEɀ 0pEɀ 0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ0pEɀ(0ptɀ0pɀ0pɀ0pɀ0pɀ0pɐ0pɐ(0ptɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0pɐ0p{ɐ0p{ɐH0p{ɀ0pɀ0p5ɀ0p5ɀ0p5ɐ0p5ɐ0p5ɐ0p5ɀ0pɐ0p2ɐ0p2ɐ0p2ɐ0p2ɐ0p2ɐ0p2ɐ0p2ɐ0p2ɐ0p2ɐ0p2ɐ0p2ɐ 0p2ɐ 0p2ɐ 0p2ɐ 0p2ɐ0p2Ɉ02А0p2ɐ0p2ɐ0p2ɐ0p2ɐ0p2ɐ0p2ɐ0p2ɐ0p2ɐ0p2ɐ0p2ɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɐ0pɀ0pɐ0pɐ0pɐ0pɐ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0pɀ0p@0@00`45G{ab6Lfq;<fg]^"#)hi!!!1424}44499;;!?AcDdDOFPF~FPP9P#Q$Q%QcQTWXZZ[__;abWdfff-q?qTqdqeq8r9rttvvsyty}}?@>?@x&'34'(*9m=>:xy
$92 B
8:>nwry>7
@
04
@V
07nwry>7p0p0p0p0p0p0lwry>7lwry>7@00olwry>7nwry>7nwry>7nwry>7
@>
@V
07nwry>7p0p0
@0
@00o
@0
@0
@0
@0
@0
@0
@0ppp
@0
@0
@0p
@0
@0
@0
@0pϿ2VpϿ2VpϿ2VpϿ2VpϿ2V
@0
@0
@0
@08
@08
@08p6p6p6
@0s?
@0s?
@0s?p6p6p6
@0
@0
@0M
@0M
@0
@0
@0
@0
@0
@0
@0OA0@$p0jZp0jZp0jZ
@0f
@0f
@0f0f0f0f0fp0jZp0jZp0jZp0jZpjZpjZpjZpjZpjZpjZ@80jZ@80jZ@80jZ
@0Р0@~Р0@~Р0@~Р0@~Р0@~@80jZ@80jZ@80jZ@80jZ
@at0iv
@0jZ
@0jZ
@0jZ@0t"њ@0t"њ@0t"њ00000
@0jZ
@0jZ0u
@0jZ
@0jZ
@0jZ
@0
@0
@h0
@0
@0
@0
@h0
@h0
@0Z
@0Z
@h0
@h0
@h0
@0jZ
@0jZ
@0jZ
@0jZ
@0jZ
@0jZ
@0jZ
@0jZ
@3jZ
@0jZ
@0jZ
@0"
@0"
@0"
@3jZ
@0jZ
@0jZ
@0jZ
@0jZ
@0jZ
@@0
@@0
@@0
@3jZ
@0jZ
@0jZ
@0jZ
@0jZ
@0jZ
@3jZ~1jZp0jZ
@w00o
@w00o0yCT~1yJ@rECTr30oCTr30o0X^wP@0@00
"&:f=SXDZfksq|o3j2,4D
$La
q^:TkAu^9222P4P7P6NQ=
`b$79DLb m64b$/ϧI/׆Hb$[%^C9רҽO$b$wV@N`V,^B$W}
GKaA
Vb$TxڧJ욕F[g,YZB$c]FRZNYB;B$p GEܜ@ @(
z
s*A5%C"?z
s*A5%C"?z
s*A5%C"?z
s*A5%C"?z
s*A5%C"?z
s*A5%C"?z
s*A5%C"?z
s*A5%C"?<
C ?25PO=`tk tmt3!"tt!t8 t Lt9D3;lvkv OY4
>
*5DMR]^h")mxr!|!%%3 3D3N324@4}44M5X5o5}56)6D6O67 7S9]99:;
;;;<<AAAAB#BVD`DpD~DDDDD%E3EF GqG|GGG H&HZH`HJJJJcMmMLNUNNNUO_OOOQ QQQQQbVoVVV5W?WWWbXpXYYYYYYZZ\\\\aabblbKdUddddddd/e2eeehhiiiijj!j+jjjjjakkkkkn nnnnnoopp.q4q;q=qAqDqFqJqPqRq^q`qkqoqxq{qWtet7wAwtyyyyozyzzz}}~
~epЄބ lv؎ ďȐWa
#}\f͙4>T^it'1Z[v.8'٣HOYeɥDR)4svŨթکuzNS<Ivìˬ(-FN,1DI%&12=Xc
&4AܸιԹ#źغ~ɻϻڻܻ"*-/CKXntֽܽ5=NVgsȾ˾;۾%->J#[ax{}4:NQS\"*:BNQlr%(*5^fv~U`")ou$*257GQ`izw}Xd'-58:KSYgtGY"UcMY'6B^dtwy(0;G?D
(+BOn{n{&+9?OR0R]WbLZkw,8&3DJ]`cw^c@G
$(-+?IR\
FLkz+1EHJXls=Knt/?Xaz*13=&0>H:H*8*-02EHy9? " ( T
Z
SZI
R
g
n
,9;>bw
mv#&&&g..2*233O6T699<<6?A???EEXRcRSSXUcUYYYY([3[&\4\t^{^|cc,f:f.q4qAqDqeqjq2dƈ\g!,̖P[{Ƥͤ1nsyΩԩnthk
&02NQkq}ɸѸܸιԹܹ
,4ɻϻڻ"*-KXntֽܽ!03NRgjȾ˾
%)>A\`˿ѿ59[ax{4:NQpv
:>NQlr%(IOY\vz$oury$*25MOiqw}"-6AMX^'-58SYce/2EJU[nw
69^dtw (,;>(+=@nu9?ORw}'R]GI+0
'*KRr{DJ]`!
1:[dFLTVgi+1EHlp-3=Knt/?Xazmn:=:E8Kb 1 2
Sq
s
t
7;>:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::sNtNuNvNwNxNyNhhh^h`hCJpho(EH^`CJOJ PJ
QJ pho(EHop^`pCJOJ
PJ
QJ
pho(EH@^`@CJpho(EH^`CJOJ PJ
QJ pho(EHo^`CJOJ
PJ
QJ
pho(EH^`CJpho(EH^`CJOJ PJ
QJ pho(EHoP^`PCJOJ
PJ
QJ
pho(EHhhh^h`hCJo(EH^`CJOJ PJ
QJ o(EHop^`pCJOJ
PJ
QJ
o(EH@^`@CJo(EH^`CJOJ PJ
QJ o(EHo^`CJOJ
PJ
QJ
o(EH^`CJo(EH^`CJOJ PJ
QJ o(EHoP^`PCJOJ
PJ
QJ
o(EHhhh^h`hCJo(EH^`CJOJ PJ
QJ o(EHop^`pCJOJ
PJ
QJ
o(EH@^`@CJo(EH^`CJOJ PJ
QJ o(EHo^`CJOJ
PJ
QJ
o(EH^`CJo(EH^`CJOJ PJ
QJ o(EHoP^`PCJOJ
PJ
QJ
o(EHhh^h`CJpho(EH^`CJOJ PJ
QJ pho(EHo^`CJOJ
PJ
QJ
pho(EH|^`|CJpho(EHL^`LCJOJ PJ
QJ pho(EHo^`CJOJ
PJ
QJ
pho(EH^`CJpho(EH^`CJOJ PJ
QJ pho(EHo^`CJOJ
PJ
QJ
pho(EHhh^h`CJpho(EH^`CJOJ PJ
QJ pho(EHo^`CJOJ
PJ
QJ
pho(EH|^`|CJpho(EHL^`LCJOJ PJ
QJ pho(EHo^`CJOJ
PJ
QJ
pho(EH^`CJpho(EH^`CJOJ PJ
QJ pho(EHo^`CJOJ
PJ
QJ
pho(EHhhh^h`hCJpho(EH^`CJOJ PJ
QJ pho(EHop^`pCJOJ
PJ
QJ
pho(EH@^`@CJpho(EH^`CJOJ PJ
QJ pho(EHo^`CJOJ
PJ
QJ
pho(EH^`CJpho(EH^`CJOJ PJ
QJ pho(EHoP^`PCJOJ
PJ
QJ
pho(EHhhh^h`hCJo(EH^`CJOJ PJ
QJ o(EHop^`pCJOJ
PJ
QJ
o(EH@^`@CJo(EH^`CJOJ PJ
QJ o(EHo^`CJOJ
PJ
QJ
o(EH^`CJo(EH^`CJOJ PJ
QJ o(EHoP^`PCJOJ
PJ
QJ
o(EH@01JKt^t_WqWr=@"$L@R@h@|@(@UnknownMichael GruningerGTimes New Roman5Symbol3ArialKMTimes-RomanTimesuTimes New Roman ItalicTimes New RomanCawKĠLucida GrandeqTimes New Roman BoldTimes New RomanuBrush Script MT ItalicBrush Script MT3Times? Courier NewCNaƴ0000҉0 Pro W3;HelveticaTimes New Roman Bold ItalicTimes New Roman;Wingdings#h]fFec҆7&Gq!d#q?wUses of PSLMichael GruningerMichael Gruninger(
Oh+'0
4@L
Xdlt|'Uses of PSL0Michael Gruninger0NormalMichael Gruninger200Microsoft Word 11.0@
@D8@Ì@l&G
՜.+,0`hpx
'qUses of PSLTitle
!"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~
!"#$%&'()*+,-./0123456789:;<=>?@ABCDEFHIJKLMNPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~Root Entry F]Data
G1TableOWordDocumentSummaryInformation(DocumentSummaryInformation8CompObjX FMicrosoft Word DocumentNB6WWord.Document.8__ |