Conceptual and formal specifications of problem-solving methods

Reusable problem-solving methods as provided by the PROTEGE-II improve knowledge engineering by allowing developers to design reasoners quickly from pre-existing components. The PROTEGE-II approach allows developers to select methods from a library, and to map the methods to a domain ontology. Still, these methods lack a clear conceptual and formal description that would enable their reuse through matching their competence and assumptions with the available domain knowledge and the given task. KARL is a conceptual and formal knowledge-specification language that provides modeling primitives for specifying problem-solving methods. In this paper, we show how the code and informal descriptions of problem-solving methods in PROTEGE-II can be complemented with the conceptual and formal method definitions in KARL. For our case study we choose two methods from the PROTEGE-II framework: chronological backtracking and a task-specific refinement, the board-game method. In addition to the conceptual and formal specification of these methods, we provide insights in the refinement of general-purpose methods to task-specific (i.e., strong) problem-solving methods. We further show how a task-specific method can be adapted to a given domain and application. In the case of both methods, we achieve this adaptation by introducing ontological commitments over the terminological structure of the entities used to describe the states of the reasoning process, and by using these terminological structure to define state transitions of Larger grainsize.