We consider the operation of sum on Kripke frames, where a family of frames-summands is indexed by elements of another frame. In many cases, the modal logic of sums inherits the finite model property and decidability from the modal logic of summands. In this paper we show that, under a general condition, the satisfiability problem on sums is polynomial space Turing reducible to the satisfiability problem on summands. In particular, for many modal logics decidability in PSPACE is an immediate corollary from the semantic characterization of the logic.
تحميل البحث