Search

In this paper, we present sequent calculus for branching-time temporal logic with until operator. This sequent calculus uses efficient loop-checktechinque. We prove that we can use not all but only several special sequents from the derivation tree for the loop-check. We use indexes to discover these special sequents in the sequent calculus. These restrictions let us to get efficient decision procedure based on introduced sequent calculus.

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.