Efficient decision procedure for Belief modality - Birštunas, Adomas (Lietuvos matematikos rinkinys, 2005)
This paper defines decision algorithm for subclass of BKD45DKDIKD logic which is based on known algorithm for temporal BKD45DKDIKD logic [2]. BDI logics are widely used in agent based systems. Such usage of BDI logic can be found in [1]. The original decision algorithm uses loop-check technique for BEL and temporal operators. Applied loop-check technique is not optimized and therefore loop-check takes most of the time used in decision algorithm. Some examples of efficient loop-check applications for logic KT, S4 and some subclasses of intuitionistic logic can be found in [4]. Another efficient loop-check can be found in work [3]. We concentrate on our attitude on loop-check optimization for BEL operator. This paper defines decision algorithm modification, which uses efficient loop-check for BEL operator, but do not effect performance of other parts of algorithm. We define optimization only for BEL operator and therefore we omit temporal operators in this paper.
Keywords: BDI logic; loop-check; sequent calculus