A formal model for verification of dynamic consistency of KBSs

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 are defined in C: Eq = {x : x → q is an arrow in C}, and Ep = {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 Ep, which is equivalent to the inequality Ep ≠ C. In this context, the two main ideas in the paper are 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 Ep 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.