Formally Verifying Dynamic Properties of Knowledge Based Systems

Abstract. In this paper we study dynamic properties of knowledge-based systems. We argue the importance of such dynamic properties for the construction and analysis of knowledge-based systems. We present a case-study of a simple classification method for which we formulate and verify two dynamic properties which are concerned with the anytime behaviour and the computation trace of the classification method. We show how Dynamic Logic can be used to formally express these dynamic properties. We have used the KIV interactive theorem prover to obtain machine-assisted proofs for all the properties and theorems in this paper.

• Type: Conference
• Year: 1999
• Where: EKAW
• Authors: Perry Groot, Annette ten Teije, Frank van Harmelen
• Keywords: Classification Method, Dynamic Properties, EKAW 1999, Information Management, Knowledge-based Systems