Decision procedures for BDI logics
Anand S. Rao, Michael P. Georgeff
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.
@article{bdilogic-jlc8,
Author = {Rao, Anand S. and Georgeff, Michael P.},
Doi = {10.1093/logcom/8.3.293},
Issn = {0955-792X},
Journal = {Journal of Logic and Computation},
Keywords = {Rational agents,belief-desire-intention (BDI) model,branching time temporal logic,modal logic,multi-modal logic,tableaux methods,temporal logic,theorem proving},
Month = jun,
Number = 3,
Pages = {293--342},
Title = {Decision procedures for {BDI} logics},
Url = {http://logcom.oxfordjournals.org/cgi/content/long/8/3/293},
Volume = 8,
Year = 1998}