Premium
A formal model for knowledge‐based systems verification
Author(s) -
Laita Luis M.,
Couto Julia,
De Ledesma Luis,
Margarit Alejandro Fernández
Publication year - 1994
Publication title -
international journal of intelligent systems
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 1.291
H-Index - 87
eISSN - 1098-111X
pISSN - 0884-8173
DOI - 10.1002/int.4550090902
Subject(s) - computer science , formal verification , formal methods , artificial intelligence , software engineering , theoretical computer science
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 P 0 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 P 0 . 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. © 1994 John Wiley & Sons, Inc.