The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #663

Title:Proof Planning and Maintainability of Ai Systems
Date:Nov 1993
Presented:Submitted to AI Applications
Abstract:Configuring large computer hardware systems is a complex task and efforts to automate it have spawned knowledge based systems which have proved difficult to maintain. We propose a new approach which breaks away from the traditional rule-based IKBS paradigm and have implemented a prototype system in Prolog in which to test out our ideas. In this paper we give a logical formalism for configuration and use a proofs as configurations approach; this approach is analogous to program synthesis via proofs as programs and equally rigorous. Meta-level control is achieved through proof plans, which embody common strategies for guiding inference. As well as ensuring soundness, in that only legal configurations can be synthesized, the system also facilitates maintenance because of its clean separation of object-level knowledge, heuristics, and control strategies. Using the hardware configuration domain by way of example, we have provided an important proof of concept in the quest for reliable, robust, and maintainable knowledge based systems.

[Search These Pages] [DAI Home Page] [Comment]