Reasoning about Minimal Belief and Negation as Failure

TL;DR

This paper analyzes the complexity of reasoning in propositional MBNF, a unifying nonmonotonic logic framework, showing it is computationally harder than related formalisms and establishing a correspondence with autoepistemic logic.

Contribution

It characterizes the complexity of propositional MBNF reasoning, provides algorithms, and links negation as failure to negative introspection in autoepistemic logic.

Findings

Entailment in propositional MBNF is at the third level of the polynomial hierarchy.

Algorithms for reasoning in propositional MBNF are developed.

Negation as failure in MBNF corresponds to negative introspection in autoepistemic logic.

Abstract

We investigate the problem of reasoning in the propositional fragment of MBNF, the logic of minimal belief and negation as failure introduced by Lifschitz, which can be considered as a unifying framework for several nonmonotonic formalisms, including default logic, autoepistemic logic, circumscription, epistemic queries, and logic programming. We characterize the complexity and provide algorithms for reasoning in propositional MBNF. In particular, we show that entailment in propositional MBNF lies at the third level of the polynomial hierarchy, hence it is harder than reasoning in all the above mentioned propositional formalisms for nonmonotonic reasoning. We also prove the exact correspondence between negation as failure in MBNF and negative introspection in Moore's autoepistemic logic.