Modular Design and Verification of Logical Knowledge Bases

Grigoris Antoniou

In this paper I describe a framework for the design of modular knowledge based systems which is motivated by work in algebraic specification and software engineering. The main characteristic of the framework is that verification work can be done in a local setting. We present two concrete module concepts within this framework, and give formal semantics and correctness notions for them. Finally, we show a method for proving correctness of modules using an assertional proof system for logic programs.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.