An NP-complete fragment of fibring logic

The fibring method provides a semantic way to take various modal logics as arguments to produce an integrated one, and the benefit of this method is clear: a stronger expressive power. In this article, we prove the computational complexity of a class of fibring logics. Especially for a fibring logic composed of two S5 systems, we present a novel reduction method, Fibring Structure Mapping, to settle its complexity. Then, we found a special NP -complete fragment for the fibred S5 system. The significance of these results is that, on the one hand, the reduction method presented in this article can be generalized to settle the computational complexity problem of other fibring logics, and on the other hand, they help us to achieve a balance between the expressive power and the difficulty of computation.