Methods

• To estimate space bounds for propositional modal logics, we define decision procedures based on clausal tableau systems for them, in which saturating operations play an important role.

• For L being a propositional normal modal logic, to construct the least L-model for a positive propositional modal logic program P we build a L-model graph realizing P.

• Given a MDatalog program P in a first-order normal modal logic L, to construct the least L-model of P we can make the ground instantiation of P, treat it as a positive propositional modal logic program, and construct the least propositional L-model for it. (This method is for estimating computational complexity. In the thesis we also discuss a more efficient method.)