Inconsistency checking: an approach based on satisfiability

In this paper we construct a propositional formula for each hypothesis in a knowledge base. This is done by traversing the knowledge network constructed from a given knowledge base. The basis for this work is the fact that, for any hypothesis f, both f and NOT f can not be proved simultaneously in a consistent knowledge base. Thus the presence of a satisfiable formula of the form (f and NOT f) indicates an inconsistency in the knowledge base. Since consistency checking in a knowledge base is proved to be an NP-complete problem, distributing the task will be advantageous. Unlike the earlier attempts to check inconsistency of knowledge bases, our approach gives flexibility to distribute the consistency checking, in a distributed environment.