Specifying and verifying knowledge-based systems with KIV
Dieter Fensel, Schoenegge, Arno · 1997
. We discuss the use of the Karlsruhe Interactive Verifier (KIV) for the verification of conceptual and formal specifications of knowledge-based systems. KIV was originally developed for the verification of procedural programs but it fits well for verifying knowledge-based systems. Its specification language is based on algebraic specification means for the functional specification of components and dynamic logic for the algorithmic specification. It provides an interactive theorem prover integrated into a sophisticated tool environment supporting aspects like the automatic generation of proof obligations, generation of counter examples, proof management, proof reuse etc. Only through this support, verification of complex specifications becomes possible. We provide some examples on how to specify and verify tasks, problem-solving methods, and their relationships. Keywords. Knowledge-based systems, knowledge-level modelling, formal specification, verification, interactive th...