On constructing fibred tableau calculus for BDI logics

Abstract. In [12, 16] we showed how to combine propositional BDI logics us-ing Gabbay’s fibring methodology. In this paper we extend the above mentioned works by providing a tableau-based decision procedure for the combined/fibred logics. To achieve this end we first outline with an example two types of tableau systems, (graph & path), and discuss why both are inadequate in the case of fib-ring. Having done that we show how to uniformly construct a tableau calculus for the combined logic using Governatori’s labelled tableau system KEM