Reasoning with stratified default theories

Default logic is one of the principal formalisms for nonmonotonic reasoning. In this paper; we study algorithms for computing extensions for a class of general propositional default theories. We focus on the problem of partitioning a given set of defaults into a family of its subsets. Then we investigate how the results obtained for these subsets can be put together to achieve the extensions of the original theory. The method we propose is designed to prune the search space and reduce the number of calls to propositional provability procedure. It also constitutes a simple and uniform framework for the design of parallel algorithms for computing extensions.