Layered clausal resolution in the multi-modal logic of beliefs and goals

Abstract

In this paper a proof technique for reasoning about the multi-modal logic of beliefs and goals is defined based on resolution at different levels of a tree of clauses. We have considered belief and goal as normal modal logic operators. The technique is inspired by that in [6,7] and allows for a locality property to be satisfied. The main motivation for this work arises not as much from theorem-proving as from the notion of belief and goal revision under an assumption of consistency of the beliefs and goals of an agent. We also present proofs of soundness and completeness of the logic. © Springer-Verlag Berlin Heidelberg 2005.