Stratification and knowledge base management

We address the problem of interactively constructing models of a knowledge base expressed in logic. User inputs in the form of assertions are added to the initial knowledge base and some specific logical consequences of the assertions are used to provide guidance for further interaction. We show that the concept of stratification applied to disjunctive knowledge bases provides a framework for maintaining the computational complexity of the interaction to a manageable level. We discuss the dynamics of the stratification and the related complexity issues. Several algorithms that form the core of an interactive knowledge base maintainance system are presented including a linear time stratification algorithm based on a graph theoretic characterization of the concept of stratifiability