A FORMAL MODEL FOR VERIFICATION OF DYNAMIC CONSISTENCY OF KBSS

This paper proposes a translation of the main concepts involved in Kno wledge Based Systems Verification into a theoretical metalanguage base d on Halmos and Leblanc's ''Monadic and Polyadic Algebras.'' These alg ebras are expressed in terms of a few basic concepts of preorder-categ ory theory. Any Knowledge Base (KB) may be considered as a set of arro ws that gives rise to a preorder category C, called ''the N-category a ssociated to the KB.'' Two subsets are defined in C: E(q) = {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, E(p)); it is consistent if it is not the case that both a proposition and its negation are simultaneously in E(p), which is e quivalent to the inequality E(p) not equal C. In this context, the two main ideas in the paper are tile following, First, to characterize fo rward reasoning consistency of a KB with respect to a set of facts, in terms of consistency in (C, E(p)), where C is the N-category associat ed to the KB, and p is the conjunction of all the facts in the given s et. Second, to characterize the absence of conflict in backward reason ing in terms of some relations among sets of the form E(p) and E(q), f or appropriate p and q. The aim of the paper is to present ideas for f urther discussion leading to the construction of formal logico-algebra ic models for verification, rather than to propose a completed model. It presents just one possible approach which may suggest others.