On the complexity of the decision problem in propositional nonmonotonic logic

Abstract

In McDermott and Doyle's nonmonotonic logic (NML) a sentence is defined to be derivable from a set of premises if the sentence belongs to every fixed point of a certain proof theoretical operator defined by the premises. A new characterization of derivability in NML is given without using fixed points. With the aid of this characterization the complexity of the decision problem in propositional NML is analysed. It is shown that the derivability problem together with the problem whether the premises have a fixed point containing a given sentence as well as the problem whether the premises have any fixed point are all NP-hard. Further it is shown that finding a fixed point of the premises containing a given sentence or a fixed point not containing a given sentence as well as determining whether a set of premises has a fixed point are all polynomial time nondeterministic Turing reducible to the satisfiability problem in classical propositional logic.