A decision method for nonmonotonic reasoning based on autoepistemic reasoning (Q1891263)

Autoepistemic logic is a modal logic with an operator \(L\), which is interpreted as ``is believed''. Autoepistemic logic models the beliefs of an ideally rational fully introspective agent. The main object of interest in autoepistemic logic is the set of beliefs of the agent given a set of sentences as the initial premises of the agent. The agent's ideal rationality implies that the agent believes exactly every logical consequence of the initial assumptions of her/his beliefs. Full introspection entails that the agent is capable of using both positive introspection (if he believes \(p\) then he believes that he believes \(p\)) and negative introspection (if he has no evidence for \(p\) then he does not believe \(p\)). Due to negative introspection, the logic is non- monotonic. If the agent gets evidence for \(p\) he must retract his disbelief in \(p\). It turned out that many versions of nonmonotonic and default reasoning, for example Reiter's default logic, can be mapped to autoepistemic reasoning. Decision procedures for autoepistemic logic can therefore also be applied to these other versions of nonmonotonic reasoning. In the paper a new decision procedure for a particular, but still quite general class of autoepistemic logics is introduced. The logic is composed of an arbitrary monotonic, possibly first-order logic and the belief operator. The only restriction is to forbid quantifications into belief contexts. The logic is \(L\)-hierarchic. This means that a sentence \(p\) can appear in an introspective sequence of conclusions only after all \(q\) such that \(Lq\) is a subformula of \(p\) have appeared in the sequence. It is claimed that only slight modifications of the algorithm are necessary for logics which are not \(L\)-hierarchic. The decision procedure itself needs a theorem prover of the basic monotonic logic as a subroutine, and this is the only requirement for the basic logic. The method is a bottom-up approach. It decomposes the problem into a classical reasoning problem that is submitted to the given theorem prover for the basic logic, and a conflict resolution task. Conflict resolution triggers a simple backtracking scheme in the algorithm. As compared to other decision procedures which need exponential space in many cases, the proposed one needs polynomial space. The method is proved sound and complete. A few applications to other systems, in particular to Reiter's default logic are discussed. Some optimizations developed for the autoepistemic case could be transferred to the default logic case, thus reducing the search space in the decision procedure for default logic.