Journal: Data and Knowledge Engineering
We investigate the formal specification of the reasoning process of knowledge-based systems. We analyse the corresponding parts of the KADS specification languages KARL and (ML)2 and deduce some general requirements for such specifications. The essence of these languages is that they integrate a declarative specification of inferences with control information. The languages differ in the way they achieve this integration and each of them has shortcomings. We propose a unifying semantical framework that integrates the core of the different solutions and overcomes their problems. We define a semantics and axiomatization with the logic MLCM (Modal Logic of Creation and Modification). MLCM was developed to reason about dynamic properties of the specification language COLD. MCL (Modal Change Logic) is a generalization of MLCM based on experience in applying MLCM to knowledge-based systems and specifications with evolving algebras. The main contribution of the paper is not to introduce yet another specification language. Instead we aim on four goals: (1) defining a framework for describing the dynamic reasoning behaviour of knowledge-based systems which integrates existing approaches; (2) defining a semantics for the specification of the dynamic reasoning behaviour of a knowledge-based system within the states as algebras setting of MLCM that overcomes several shortcomings and ad-hoc solutions of existing approaches; and (3) providing an axiomatization that enables the development of mechanised proof support. (4) Through conceptual and semantical clarity, we investigate the relationships to similar work in software engineering and database engineering opening possibilities for further cross-fertilization of these fields.