Correction of dynamic knowledge

The work concerns a framework for the formal specification and verification of the dynamic knowledge of knowledge-based systems. At a conceptual level, a system is specified in terms of problems, problem-solving processes, knowledge. An important question is to determine if a process is applicable to solve a problem. In this paper we present how problems and problem-solving processes are specified by abstract data types and we introduce a formalization of the relationships between them. We show how it can be formally proved that a process is correct with respect to a given problem.