A FORMAL MODEL FOR KNOWLEDGE-BASED SYSTEMS VERIFICATION

A logico-algebraic model for verification of Knowledge Based Systems, based on Abraham Robinson's meta-algebra, is presented in this article . The set of rules of Knowledge Based System is considered to be the s et of axioms of a theory ''T''. The model consists of: (i) the collect ion ''P'' of all well formed formulas of the language of T, (ii) a sub set P0 of P that has as its elements the axioms of a given logic (biva lued, intuitionistic, or other), plus all the theorems that can be ded uced from this logic inside the language of T, (iii) some distinguishe d subsets of P, to be called m-ideals and m-filters, that depend on T and P0. Important concepts that are involved in the verification of Kn owledge Based Systems are considered, such as forward and backward rea soning consistencies. Appropriate characterizations are obtained by us ing properties of m-ideals and m-filters. (C) 1994 John Wiley & Sons, Inc.