エージェントの相互信念を扱う拡張BDI logicの演繹体系  [in Japanese] A Deduction System of Extended BDI Logic to Handle Mutual Belief  [in Japanese]

BDI logicは、合理的エージェントの記述に用いられる時相論理体系で、CTLにエージェントの心的状態を記述する様相オペレータを導入し、述語論理に拡張したものである。我々は、CTLベースの命題論理に限定したBDI logicに対し、seauent calculus による完全な演鐸体系を与えた。しかし、もともとのBDI logic は、単独のエージェントの心的状態に対応する様相オペレータしか持たず持たず、マルチエージェント環境でのエージェントの相互心的環境の記述はできない。本論文では、我々の演鐸体系に対し、マルテエージェント環境におけるエージェント毎の心的状態様相オペレータ、および相互心的状態の記述を許すように拡張したものを与え、またその体系によるいくつかの証明の例を示す。

BDI logics are extensions of the predicate variant of CTL to represent the behavior of rational agents by introducing mental state operators. We previously presented deduction systems for CTL-based prepositional BDI logics using sequent calculus.However,since the original BDI logics have only operators to represent the mental states of individual agents, they cannot handle mutual mental states for multiple agents.In this paper,we extend our deduction systems so that we can handle individual and mutual mental states for multiple agents in multi-agent environments.We also show some examples of proof in our system.