摘要

阐述了 Agent的形式化描述应该采用含有正规和非正规模态算子的混合模态逻辑为逻辑工具的观点 .建立了 Agent- BDI逻辑的代表系统 A- BI,讨论了它的语法和语义 .特别是给出了非正规模态算子基于 Kripke标准可能世界的新的语义解释 ,证明了 A- BI逻辑系统不但是可靠的 ,而且是完备的 .A- BI逻辑系统恰当地刻画了信念与意图的本质与内在联系 ,可作为 Agent形式化研究的逻辑工具 .