A formal model for verification of dynamic consistency of KBSs

✍ Scribed by L.M. Laita; B. Ramírez; L.De Ledesma; A. Riscos

• Publisher: Elsevier Science
• Year: 1995
• Tongue: English
• Weight: 1018 KB
• Volume: 29
• Category: Article
• ISSN: 0898-1221
• DOI: 10.1016/0898-1221(94)00250-o

✦ Synopsis

This paper proposes a translation of the main concepts involved in Knowledge Based Systems Verification into a theoretical metalanguage based on Halmos and Leblanc's "Monadic and Polyadic Algebras." These algebras are expressed in terms of a few basic concepts of preorder-category theory.

Any Knowledge Base (KB) may be considered as a set of arrows that gives rise to a preorder category C, called "the N-category associated to the KB." Two subsets axe defined in C: Eq = {x :

x --* q is an arrow in C}, and E p = {x : p --* x is an arrow in C}, where q and p, respectively, are a goal and a conjunction of facts.

A logic is a pair (C, EP); it is consistent if it is not the case that both a proposition and its negation are simultaneously in E p, which is equivalent to the inequality E p ¢ C. In this context, the two main ideas in the paper axe the following. First, to characterize forward reasoning consistency of a KB with respect to a set of facts, in terms of consistency in (C, EP), where C is the N-category associated to the KB, and p is the conjunction of all the facts in the given set. Second, to characterize the absence of conflict in backward reasoning in terms of some relations among sets of the form E p and Eq, for appropriate p and q.

The aim of the paper is to present ideas for further discussion leading to the construction of formal logico-algebraic models for verification, rather than to propose a completed model. It presents just one possible approach which may suggest others.