Complexity of Modal Logics [PhD Thesis] by Edith Spaan

Show description

We look at the following three languages: • C\2 = £({1, 2}, V) • C\ — C{{ 1},V U {[2]0|(f>an C formula}) • C2 = C{{2}, V U {[1]0|(j) an C formula}) We’ll use this approach, because it leads to more elegant formulations of the construction. C onstruction To determine whether a formula is T\ 0 T 2 satisfiable, define a recursive predicate T\ 0 ^-W O R L D as follows, for T and £ sets of formulas, and a € {1,2}: T x 0 J*2-WORLD(a, T, £) iff £ = 0 or there exist a model M = (W ,R a, 7r), and a world wq GW such that: CHAPTER 3.

First suppose that 0! consists of two elements, say a and 6. 6, © aGn T a satisfiability is polynomial time reducible to T a ® satisfiability. By the previous section, T a ® T\> satisfiability is in NP, and thus © a€n T a satisfiability is in NP as well. Finally, suppose that 0! contains at least three elements. Since we are not in case N, it follows that for all a £ fi, is not a skeleton subframe of T a. Furthermore, since we are not in case A, we know that / \ is not a skeleton subframe of T a.

The satisfiability problem for this class of frames is in NP. e. pO(^ )w }| \). We start by describing the form of the frames in T \ and T 2. 3 Let T \ and T 2 be two classes of uni-modal frames closed under disjoint union. If we are not in case I and A through F, then for some a £ {1,2}, we are in one of the following three cases: not skeleton subframe of T a not skeleton subframe of Ta • CY ct G •A • ; •— •> \• ; •— • • H • \ , * ** \ ) • • CY^^ ^_^0—^0 ^ 00 ^0 ^ ^ ^CY , CY } 9 ^CY J In the proof of the first requirement, we have seen that / \ m , and 9 + 2 „ are not skeleton subframes of T \ nor of T 2.