A Conceptual And Formal Model Of A Diagnostic Reasoner

The knowledge acquisition process can be supported by distinguishing different models in the development process of knowledge-based systems, where each model is dedicated to a specific phase. Two of these models are the conceptual model and the formal model. Conceptual models of knowledge-based systems facilitate initial system specification because they are easy to understand and construct. However, such models are often ambiguous and inconsistent, and contain hidden assumptions. The use of formal methods is a way to overcome these problems, and formalization becomes essential when we have to guarantee that system specifications are met, such as in safety critical systems. This paper presents a conceptual model and a formal model of a diagnostic reasoner, and includes a proof which shows that the high-level specification of our reasoner is ensured by the formal model presented.