MODAL CHANGE LOGIC (MCL) - SPECIFYING THE REASONING OF KNOWLEDGE-BASED SYSTEMS

We investigate the formal specification of the reasoning process of kn owledge-based systems in this paper. We analyze the corresponding part s of the KADS specification languages KARL and (ML)(2) and deduce some general requirements. The essence of these languages is that they int egrate a declarative specification of inferences with control informat ion. The languages differ in the way they achieve this integration and each of them has shortcomings. We propose a unifying semantical frame work that integrates the core of the different solutions and overcomes their problems. We define a semantics and axiomatization with the Mod al Change Logic (MCL). The main contribution of the paper is not to in troduce yet another specification language. Instead we aim at four goa ls: (1) defining a framework for describing the dynamic reasoning beha vior of knowledge-based systems which integrates existing approaches; (2) defining a semantics for the specification of the dynamic reasonin g behavior of a knowledge-based system within the stares as algebras s etting that overcomes several shortcomings and ad hoc solutions of exi sting approaches; and (3) providing an axiomatization that enables the development of mechanized proof support. (4) Through conceptual and s emantical clarity, we investigate the relationships to similar work in software engineering and database engineering opening possibilities f or further cross-fertilization of these fields. (C) 1998 Elsevier Scie nce B.V.