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 set of axioms of a theory ''T''. The model consists of: (i) the collection ''P'' of all well formed formulas of the language of T, (ii) a subset P0 of P that has as its elements the axioms of a given logic (bivalued, intuitionistic, or other), plus all the theorems that can be deduced from this logic inside the language of T, (iii) some distinguished 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 Knowledge Based Systems are considered, such as forward and backward reasoning consistencies. Appropriate characterizations are obtained by using properties of m-ideals and m-filters. (C) 1994 John Wiley & Sons, Inc.