KJ3 - a tool assisting formal validation of knowledge-based systems

摘要

This paper presents the design and implementation of KJ3 (Knowledge Judgment, version 3) which is an assisting tool for formal validation of knowledge-based systems (KBSs). The KJ3 project is motivated by two main obstacles to knowledge validation, the lack of a uniform representation and a comprehensive validation procedure. KJ3 combines Petri Nets and theorem proving techniques to solve these difficulties. In KJ3, the Enhanced High-Level Petri Net (EHLPN) is employed as a meta representation scheme to describe different KBS formalisms in a uniform format. With EHLPN, there is only one type of problems, the reachability problems, to be solved for all validation tasks. The kernel of KJ3 is a hyper-linking-based theorem prover which serves as the inference engine for checking the correctness of the transformed reachability problems. Because of the versatility of EHLPN and the soundness and completeness of the hyper-linking proof procedure, KJ3 is a reliable and robust platform for formal validation. Users can apply KJ3 to validate different types of KBSs without concerning the inference process involved in the validation procedure. Other main features of KJ3 include a friendly user interface for describing and transforming KBSs and defining the validation tasks, a mechanism for explaining the validation results, and facilities for analysing the behaviour of KBSs and defining new types of KBSs and validation tasks. (C) 2002 Elsevier Science Ltd. All rights reserved. [References: 66]