Decision procedures for BDI logics

The study of computational agents capable of rational behaviour has received increasing attention in recent years. A number of theoretical formalizations for such multi-agent systems have been proposed. However, most of these formalizations do not have a strong semantic basis nor a sound and complete axiomatization. Hence, it has not been clear as to how these formalizations could assist in building agents in practice. This paper explores a particular type of multi-agent system, in which each agent is viewed as having the three mental attitudes of belief (B), desire (D), and intention (I). It provides a family of multi-modal branching-time BDI logics with a possible-worlds semantics, categorizes them, provides sound and complete axiomatizations, and gives constructive tableau-based decision procedures for testing the satisfiability and validity of formulas. The computational complexity of these decision procedures is no greater than the complexity of their underlying temporal logic component.