I DATA & KNOWLEDGE ENGINEERING b • • Um verstn' Modal Change Logic (MCL) Specifying the reasoning of knowledge-based systems

We investigate the fl)rmal specification of the reasoning process of knowledge-based systems in this paper. We analyze the corresponding parts of the KADS specification languages KARL and (ML) e and deduce some general requirements. 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 unil~cing semantical framework that integrates the core of the different solutions and overcomes their problems. We define a semantics and axiomatization with the Modal Change Logic (MCL). The main contribution of the paper is not to introduce yet another specification language. Instead we aim at four goals: (1) defining a framework for describing the dynamic reasoning behavior of knowledge-based systems which integrates existing approaches: (2) defining a semantics for the specification of the dynamic reasoning behavior of a knowledge-based system within the.Ylatex o. ~ alq, ehras setting that overcomes everal shortcomings and ad hoc solutions of existing approaches; and (3) providing an axionmtization that enables the development of mechanized proof support. (4) Through conceptual and semantical clarity, we investigate the relationships to simila