Finite-Valued Lukasiewicz Modal Logic Is PSPACE-Complete

1 Introduction

Classical Modal Logics have been a matter of growing interest in the last decades due to their role in the formalization of several aspects of Computer Science. In particular, multimodal classical logics can be considered as a notational variant of basic Description Logic (DL) languages like ALC (see [Baader and et al., 2003] and [Schild, 1991]), and so they play an important role in the field of Knowledge Representation.

In recent years there have been efforts to generalize the formalism of DLs to the many-valued and fuzzy case (see [H´ajek, 2005; Straccia, 2006; Bobillo and Straccia, 2008; Cerami et al., 2010]), but no work has addressed, as long as the authors know, the analysis of the computational complexity of ALC Fuzzy Description Logics (FDLs) over a multiple valued logic (either finite or infinite). A first step towards an answer to the previous problem is the characterization of the computational complexity of Fuzzy Modal Logics, since Fuzzy Modal Logics correspond to ALC FDLs when there is no knowledge base (neither TBox nor ABox).

In this paper we prove that deciding satisfiability (and the same for validity and entailment) in a minimal finite-valued Łukasiewicz Modal Logic is a PSPACE-complete problem.

In Section 2 we remind what are minimal n-valued Łukasiewicz modal logics (for the sake of completeness we also introduce the non-modal Lukasiewicz propositional logic). Then, in Section 3 our main PSPACE completeness theorem is stated and proved. The proof is split in two diferent parts: one concerns being in PSPACE, and the other one takes care of being PSPACE-hard. Finally, in Section 4 we Marco Cerami and Francesc Esteva IIIA-CSIC

Bellaterra, Spain {cerami,esteva}@iiia.csic.es

explore some further consequences of our result and some future problems to be considered.

2 Preliminaries

In this Section we introduce the Łukasiewicz logics we are going to deal with in our main theorem.

2.1 Propositional Łukasiewicz Logic (with Delta Operator and Truth Constants )

Next we define what is the propositional non-modal logic we deal with, the n-valued Łukasiewicz logic Łn, using as a general framework the infinite-valued one Ł. The formulas of all these Łukasiewicz logics are built from a countable set of propositional variables V ar = {p, q, . . .} using the connectives & (conjunction), → (implication) and ⊥ (falsity truth constant).

In order to introduce the infinite-valued Łukasiewicz logic Ł we start by considering the Łukasiewicz standard algebra 〈[0, 1], ∗, ⇒, 0〉 defined by

• a binary operation ∗ called Łukasiewicz t-norm and defined as a ∗ b := max{0, a + b - 1}, for all a, b ∈ [0, 1],
• a binary operation ⇒ called the residuum (of the t-norm ∗) and defined as a ⇒ b := min{1, 1 - a + b}, for all a, b ∈ [0, 1].

A propositional evaluation is a homomorphism e from the algebra of formulas into the previous algebra, i.e., a mapping e from the set of formulas into [0, 1] such that

• e(ϕ&ψ) = e(ϕ) ∗ e(ψ),
• e(ϕ→ψ) = e(ϕ) ⇒ e(ψ),
• e(⊥) = 0.

A formula ϕ is said to be valid when it is evaluated to 1 in all propositional evaluations; it is said to be m-satisfiable when there is some propositional evaluation e such that e(ϕ) = m; and it is said to be satisfiable when it is 1-satisfiable. Then, the infinite-valued Łukasiewicz logic Ł is defined as the set of valid formulas; and analogously, Łn is defined as the set of formulas that are always evaluated to 1 in the subalgebra defined over the universe Ln := {0, 1 n-1 , 2 n-1 , . . . , n-2 n-1 , 1}.

In this framework it is common to introduce the connectives ∧, ∨, ↔, ¬, ⊕ and ⊤ at the syntactic level (the semantics counterpart will be denoted, respectively, by ∧, ∨,⇔,∼, ⊻ and 1) as the following abbreviations:

• ϕ ∧ ψ := ϕ&(ϕ → ψ) [semantically, min(a, b)]
• ϕ ∨ ψ := (ϕ → ψ) → ψ [semantically, max(a, b)]
• ϕ↔ψ := (ϕ→ψ)&(ψ →ϕ)
• ¬ϕ := ϕ → ⊥ [semantically, 1 - a]
• ϕ ⊕ ψ := ¬(¬ϕ&¬ψ) [semantically, min{1, a + b}]
• ⊤ := ¬⊥ [semantically, 1].

Another abbreviation we will use is

In the literature, there are several ways to expand all these logics Ł and Łn. One way of expanding them is by adding a unary operator Δ semantically interpreted as

Another expansion of Łn considered in this paper is the one obtained by adding n canonical truth constants, one truth constant a for each a ∈ Ln; the truth constant a is semantically interpreted as its canonical value a. We will use the three names Łn,Δ, Łcn and Łcn,Δ to denote, respectively, each one of these expansions (here c refers to the use of canonical constants). It is worth saying that the decision problem for all these propositional logics (i.e., the tautologicity problem) is known to be coNP-complete, while its satisfiability problem is NP-complete (see [H´ajek, 1998]).

We point out that in the proof we will use the well known fact that

are valid formulas in propositional Łukasiewicz logic.

2.2 n-valued Łukasiewicz Modal Logic

Following the same pattern as in [Bou et al., ] next we introduce the many-valued modal logics Λ(Fr, Łn), Λ(Fr, Łn,Δ), Λ(Fr, Łcn ) and Λ(Fr, Łcn,Δ) over all Łukasiewicz frames.

Each one of these modal logics is defined by expanding its propositional language with two unary modal operators ✷ and ✸. As usual the nesting degree deg(ϕ) of a modal formula ϕ is defined as the maximum number of nested occurrences of ✷ and ✸. And the nesting degree deg(Σ) of a finite set Σ is the maximum of {deg(σ) : σ ∈ Σ}.

A (many-valued) Kripke Łn-model (or simply, Kripke model, when there is no ambiguity) is a triple M = 〈W, R, V 〉, where:

• the domain W is a set of elements (called possible worlds),
• R : W ×W → Ln is an n-graded binary relation on W (called the accessibility relation),
• V : V ar ×W → Ln is a function, called evaluation, which maps every propositional variable p ∈ V ar and possible world w ∈ W to the set of truth values Ln.

The mapping V can be uniquely extended to one defined over all pairs of formulas and possible worlds such that

• the function V (·,w) from formulas into Ln is a propositional evaluation,
• V (✸ϕ,w) =max{R(w,w′ ) ∗ V (ϕ,w′ ) : w′ ∈W},
• V (✷ϕ,w) =min{R(w,w′ ) ⇒ V (ϕ,w′ ) : w′ ∈W},

for every formula ϕ and every w ∈ W.

A modal formula ϕ is said to be modally valid when it is evaluated to 1 in all Kripke models; it is said to be modally msatisfiable when there is some Kripke model and some world w such that V (ϕ,w) = m; and it is said to be modally satisfiable when it is 1-satisfiable. The logic Λ(Fr, Łn) is defined as the set of its modal formulas that are modally valid; and analogously we can define Λ(Fr, Łn,Δ), Λ(Fr, Łcn ) and Λ(Fr, Łcn,Δ) over all Łukasiewicz frames. Besides these sets of valid formulas, we will consider, for each m ∈ Ln, the sets Satm(Fr, Łn), Satm(Fr, Łn,Δ), etc. of modally msatisfiable formulas.

It is worth pointing out that for these modal logics (unlike the general many-valued case, see [Bou et al., ]), the modal operators are interdefinable by means of the modally valid formulas

Throughout the paper we will use both of them to ease the reading, but will prove the inductive result just for ✸, because the same results will straightforwardly work for ✷ by means of the above equivalences.

When the range of R is a subset of {0, 1} we will say that the Kripke model is crisp. And the restriction of validity to crisp Kripke models allows us to define the logics Λ(CFr, Łn), Λ(CFr, Łn,Δ), and so on; and the same for the sets Satm(CFr, Łn), Satm(CFr, Łn,Δ), etc. In the case of crisp Kripke models, it holds that the normality axiom ✷(ϕ → ψ) → (✷ϕ → ✷ψ) is modally valid; the same does not hold for arbitrary Kripke models.

We remind that in [Bou et al., ] all these modal logics (not just the ones based on crisp Kripke models) are explicitly finitely axiomatized.

A fact that will be used later in the proof of Theorem 14 is that by the definition of ✸ as a maximum, it is obvious that

• if V (✸p,w) = 1, then there is some w′ with R(w, w′ ) = 1 such that V (p, w′ ) = 1.

This tells us that if a diamond is modally satisfiable, then we can justify it without appealing to any intermediate value in Ln \ {0, 1}.

3 Complexity of n-valued Łukasiewicz Modal Logic

The aim of the present section is to study the computational complexity of the modal logics introduced above.

Theorem 1. For every n ∈ N and every m ∈ Ln,

• the set of modally m-satisfiable formulas over Kripke Łn-models is PSPACE-complete,
• the set of modally valid formulas over Kripke Łn-models is PSPACE-complete.

The same complexity result is attained when we add the Delta operator and/or the canonical truth constants. And also we get the same complexity when we only deal with crisp Kripke models.

In the rest of this section we prove this last theorem. Since

• ϕ is modally valid iff ϕ ∨ a is not modally asatisfiable (where a is the penultimate element of Łn, i.e., a = n-2 n-1 ), and
• ϕ is modally m-satisfiable iff m ↔ ϕ is modally satisfiable,

it will be enough to prove PSPACE-completeness of the modal satisfiability problems. It may seem that this trick needs the use of canonical constants in the language, but by McNaughton theorem (see [Cignoli et al., 2000, Corollary 3.2.8], we can also reduce m-satisfiability to satisfiability without the help of canonical constants; for example, we notice that

• ϕ is modally 0.75-satisfiable, iff
• ϕ2 ↔ ¬(ϕ2 ) is modally satisfiable,

Thus, by the inclusion relationships among the sets of modally satisfiable formulas it will be enough to prove that

• Sat1(Fr, Łcn,Δ) and Sat1(CFr, Łcn,Δ) are in PSPACE,
• Sat1(Fr, Łn) and Sat1(CFr, Łn) are PSPACE-hard.

Hence, we get that all sets introduced above in Section 2.2 are PSPACE-complete.

3.1 Satisfiability is in PSPACE

We start giving a PSPACE algorithm for solving Sat1(Fr, Łcn,Δ), and later we will see that this algorithm can be slightly modified to compute Sat1(CFr, Łcn,Δ). Our algorithm follows a similar approach to the one given in [Blackburn et al., 2001, p. 383-388]. We stress the fact that all formulas considered in this section may contain the Delta operator and truth constants.

Definition 2. Let Σ be a set of modal formulas, and Sub(Σ) be the set of its subformulas. We define the closure of Σ, in symbols Cl(Σ), as the set

where the superscript + refers to the process of deleting all occurrences of two consecutive negation symbols (i.e., ¬¬). When Cl(Σ) = Σ we will say that Σ is closed.

Note that if Σ is finite, then so is Cl(Σ).

Definition 3. Let Σ be a closed set of modal formulas. We define the sequence (Σ0, Σ1, . . . , Σdeg(Σ)) by the recurrence

• Σ0 := Σ,
• Σr+1 := {ψ : ✸ψ ∈ Σr} ∪ {ψ : ✷ψ ∈ Σr}.

The family of modal levels of Σ is the set Σ◦ := {Σ0, Σ1, . . . , Σdeg(Σ)}.

Note that, for every r, deg(Σr) ≤ deg(Σ)-r. In particular deg(Σdeg(Σ)) = 0.

Definition 4. Let Σ be a closed set of formulas. A Hintikka function over some Σr ∈ Σ◦ is a mapping H : Σr → Ln such that

1. H is a homomorphism of non modal connectives (which includes the Delta operator and truth constants),
2. H(✸ψ) =∼ H(✷¬ψ), for each ✸ψ ∈ Σr,
3. H(✷ψ) =∼ H(✸¬ψ), for each ✷ψ ∈ Σr.

It is said that H is an atom if there exists a Kripke model M = 〈W,R, V 〉 and a world w ∈ W such that, for each formula ψ ∈ Σ, it holds that H(ψ) = V (ψ, w).

Lemma 5. Let H : Σr → Ln and H′ : Σr+1 → Ln be two Hintikka functions, then:

Proof. For every formula ✸ψ ∈ Σr it is obvious that

Then, using that ✸ψ ∈ Σr iff ✷¬ψ ∈ Σr (by Definition 2), we get that min{H′ (ψ) ⇒ H(✸ψ) : ✸ψ ∈ Σr} = min{H(✷¬ψ) ⇒ H′ (¬ψ) : ✷¬ψ ∈ Σr}. From this fact, it easily follows that min{H′ (ψ) ⇒ H(✸ψ) : ✸ψ ∈ Σr} = min{H(✷ϑ) ⇒ H′ (ϑ) : ✷ϑ ∈ Σr}.

Definition 6. Let H : Σr → Ln be a Hintikka function, k ∈ Ln and ✸ψ ∈ Σr. We say that a Hintikka function H′ : Σr+1 → Ln is induced by ✸ψ and k-related to H (in symbols, H′ ∈ H✸ψ,k) if the following conditions hold:

• H(✸ψ) = k ∗ H′ (ψ),
• for each ✷ϑ ∈ Σr, H(✷ϑ) ≤ k ⇒H′ (ϑ).

Lemma 7. Let Σ be a closed set of formulas, Σr ∈ Σ◦ and H a Hintikka function over Σr. If H is an atom, then for every ✸ψ ∈ Σr, there is some k ∈ Ln and some H′ ∈ H✸ψ,k such that H′ is an atom.

Proof. Let H be an atom over Σr and ✸ψ ∈ Σr. Then, by Definition 4, there exist a Kripke model M = 〈W, R, V 〉 and w ∈ W such that V (✸ψ,w) = H(✸ψ). Hence there exists w′ ∈ W such that V (✸ψ,w) = R(w,w′ ) ∗ V (ψ,w′ ). Let H′ : Σr+1 → Ln be the Hintikka function defined by H′ (ϕ) = V (ϕ,w′ ), for every formula ϕ ∈ Σr+1. It is obvious that H′ is an atom. Take k = R(w,w′ ), then H(✸ψ) = V (✸ψ, w) = R(w, w′ ) ∗ V (ψ, w′ ) = k ∗ H′ (ψ) i.e., H and H′ satisfy the first condition of Definition 6. On the other hand, for each ✷ϑ ∈ Σr, we have that V (✷ϑ, w) = min{R(w,w′′ ) ⇒ V (ϑ,w′′ ) : w′′ ∈ W}, and hence H(✷ϑ) = V (✷ϑ,w) ≤ R(w,w′ ) ⇒ V (ϑ,w′ ) = k ⇒ H′ (ϑ). So, there is k ∈ Ln such that H′ ∈ H✸ψ,k.

Definition 8. Let Σ be a finite closed set of formulas, H be a Hintikka function over Σ0, and H be a family of Hintikka functions with domains (denoted by dom) belonging to Σ◦ . We say that H is a witness set generated by H on Σ when

1. H ∈ H,

1. if I ∈ H and ✸ψ ∈ dom(I), then there is some k ∈ Ln and some J ∈ I✸ψ,k such that J ∈ H,
2. if J ∈ H and J ̸= H, then there are I 0 , . . . , I r ∈ H satisfying I 0 = H, I r = J, and for each 0 ≤ i < r, there are a formula ✸ψ ∈ dom(I i ) and an element k ∈ Ln such that I i+1 ∈ I i✸ψ,k .

Lemma 9. Let Σ be a finite closed set of formulas, and H be a Hintikka function over Σ0 (i.e., Σ). Then, H is an atom iff there is a witness set generated by H on Σ.

Proof. Let Σ be a finite closed set of formulas, and H a Hintikka function over Σ0.

• (⇒) We proceed by induction on the nesting degree of the set dom(H).
• If deg(Σr) = 0 and H is an atom, then H = {H} is a witness set generated by H on Σ0.
• (d) Let deg(Σr) = d and H be an atom over Σr. Suppose, by inductive hypothesis, that, for each Σs ∈ Σ◦ such that deg(Σs) < d and each Hintikka function H′ over Σs, it holds that, if H′ is an atom, then there is a witness set generated by H′ on Σs. Since H is an atom over Σr, then, by Lemma 7, for each ✸ψ ∈ Σr there exist k ∈ Ln and an atom I ψ ∈ H✸ψ,k over Σr+1. Since the degree of Σr+1 < d, then, by inductive hypothesis, each atom I ψ generates a witness set I ψ on Σr+1. So, the set

is a witness set generated by H on Σ.

• (⇐) Suppose now that there is a witness set H generated by H on Σ, then we have to show that there exists a model which satisfies H. So, define the model M = 〈W, R, V 〉, where:

• for each variable p ∈ V ar and I ∈ H, let V (p, I) = I(p).

On the one hand, since for each I ∈ H, dom(I) contains a finite number of formulas of the form ✸ψ, then, by Definition 8, each element of the model has a finite number of R-successors. On the other hand, whenever I ′ ∈ I✸ψ,k, then deg(dom(I ′ )) < deg(dom(I)) and, therefore, the depth of the model is finite as well (it is indeed equal to deg(Σ)).

To end the proof, we have to show that, for every formula ϕ ∈ Σ, it holds that V (ϕ,H) = H(ϕ). In order to achieve this result we will prove by induction that for each I ∈ W, it holds that V (ϕ, I) = I(ϕ). So, let I ∈ W and ϕ ∈ dom(I), then:

• If ϕ = p is a propositional variable, then, by definition of V , we have that V (p, I) = I(p).
• If ϕ is a propositional combination of variables or modal formulas, since H is a Hintikka function, by Definition 4 it holds that V (ϕ, H) = H(ϕ).
• Let ϕ = ✸ψ and suppose, by inductive hypothesis, that for each J ∈ W such that deg(dom(J)) < deg(dom(I)) and for each formula χ, it holds that V (χ, J) = J(χ). By Definitions 6 and 8, we have that there exists J ∈ I✸ψ,k, for a k ∈ Ln, such that, for each ✷ϑ ∈ dom(I), we have that I(✷ϑ) ≤ k ⇒ J(ϑ), then, by residuation, k ≤ I(✷ϑ) ⇒ J(ϑ), for each ✷ϑ ∈ dom(I) and, therefore, by Lemma 5 and the construction of M, k ≤ min{I(✷ϑ) ⇒ J(ϑ) : ✷ϑ ∈ dom(I)} = min{J(χ) ⇒ I(✸χ) : ✸χ ∈ dom(I)} = R(I, J). So, by Definition 6 and the inductive hypothesis, I(✸ψ) = k ∗ J(ψ) ≤ R(I, J) ∗ J(ψ) = R(I, J) ∗ V (ψ, J) ≤ max{R(I, I ′ ) ∗ V (ψ, I ′ ) : I ′ ∈ W} = V (✸ψ, I). On the other hand, let I ′ ∈ W be such that I ′ ∈ I✸χ,k′ for a ✸χ ∈ dom(I) and k′ ∈ Ln, then, by the construction of M and inductive hypothesis, I(✸ψ) ≥ I(✸ψ) ∧ I ′ (ψ) = (I ′ (ψ) ⇒ I(✸ψ)) ∗ I ′ (ψ) ≥ min{I ′ (ϑ) ⇒ I(✸ϑ) : ✸ϑ ∈ dom(I)} ∗ I ′ (ψ) = R(I, I ′ ) ∗ V (ψ, I ′ ). Hence I(✸ψ) ≥ max{R(I, I ′ ) ∗ V (ψ, I ′ ) : I ′ ∈ W} = V (✸ψ, I). So, V (✸ψ, I) = I(ψ).

So, for each formula ϕ, V (ϕ,H) = H(ϕ) and, then, H is an atom over Σ.

Next we consider the algorithm Witness(H,Σ) given in Figure 1. This algorithm returns a boolean, and is very close to the one given in [Blackburn et al., 2001] for the minimal classical modal logic.

if H is a Hintikka function and Σ = dom(H) and for each subformula ✸ψ ∈ dom(H) there are k ∈ Ln and a Hintikka function I ∈ H✸ψ,k such that W itness(I , dom(I )) then return true else return false end if

Lemma 10. Let Σ be a finite closed set of formulas, and H : Σ → Ln. Then, Witness(H,Σ) returns true if and only if H is a Hintikka function over Σ that generates a witness set in Σ.

Proof. Let Σ be a finite closed set of formulas, and H : Σ → Ln.

• (⇒) Suppose that Witness(H,Σ) returns true, we proceed by induction on the degree of Σ.
• If deg(Σ) = 0 and Witness(H,Σ) returns true then, H is a Hintikka function over Σ, and hence H = {H} is a witness set generated by H on Σ.

• (d) Let deg(Σ) = d and suppose, by inductive hypothesis, that for each set Σ′ of formulas such that Σ′ ⊆ Σ and deg(Σ′ ) < d and each function H′ : Σ′ →Ln, it holds that, ifWitness(H′ ,Σ′ ) returns true, then H′ is a Hintikka function over Σ′ that generates a witness set in Σ′ . If Witness(H,Σ) returns true then, on the one hand, H is a Hintikka function over Σ. On the other hand, for each formula ✸ψ ∈ Σ, there are k ∈ Ln and I ∈ H✸ψ,k such that Witness(I,Σ′ ), where Σ′ ∈ Σ◦ is such that deg(Σ′ ) = d - 1. Since deg(Σ′ ) < d, and Witness(I,Σ′ ) returns true, then, by inductive hypothesis, I is a Hintikka function over Σ′ that generates a witness set I ψ in Σ′ . So, the set

is a witness set generated by H on Σ.

• (⇐) Suppose that H is a Hintikka function over Σ that generates a witness set in Σ, we proceed by induction on the degree of Σ.
• If deg(Σ) = 0 then it is enough that H is aHintikka function over Σ for Witness(H, Σ) to return true.
• (d) Let deg(Σ) = d and suppose, by inductive hypothesis, that for each set Σ′ of formulas such that Σ′ ⊂ Σ and deg(Σ′ ) < d and each function H′ : Σ′ → Ln, it holds that, if H′ is a Hintikka function over Σ′ that generates a witness set in Σ′ , then Witness(H′ ,Σ′ ) returns true. So, if H is a Hintikka function over Σ that generates a witness set H in Σ, then, by Definition 8, we have that, for each formula ✸ψ ∈ Σ there are k ∈ Ln and I ∈ H✸ψ,k ∩ H. Then we have that I is a Hintikka function over Σ′ that generates a witness set in Σ′ , where Σ′ ∈ Σ◦ is such that deg(Σ′ ) = d - 1. Hence, since deg(Σ′ ) < d, then, by inductive hypothesis, Witness(I,Σ′ ) returns true. So, Witness(H,Σ) returns true.

Theorem 11. Sat1(Fr, Łcn,Δ) is in PSPACE.

Proof. Let ϕ be a modal formula. By Lemmas 9 and 10, we have that ϕ is m-satisfiable iff there is a Hintikka function H : Cl(ϕ) → Ln such that H(ϕ) = m and Witness(H,Cl(ϕ)) returns true. Thus we need to prove that Witness can be given a PSPACE implementation. Consider a non-deterministic Turing machine that guesses a Hintikka function H over Cl(ϕ) and runs Witness(H, Cl(ϕ)), then we need to prove that this machine runs in NPSPACE and, by an appeal to Savitch's Theorem we will achieve the desired result. The key points of the implementation are the following:

1. As pointed out in [Blackburn et al., 2001], encoding a subset Σ of Cl(ϕ) requires space O(|ϕ|) (here |ϕ| refers to the length of the encoding of ϕ). On the one hand, each element of a function H : Σ → Ln can be represented as an ordered pair 〈ψ, i〉 ∈ Σ × Ln and, on the other hand, |H| = |Σ|. Hence, if j = max{|r| : r ∈
2. Ln}, then encoding a Hintikka function requires space bounded above by |ϕ| + j · |ϕ|, that is space O(|ϕ|).
3. For each subformula ✸ψ ∈ dom(H), whether there are k ∈ Ln and a Hintikka function I ∈ H✸ψ,k, can be checked separately. Given a subformula ✸ψ ∈ dom(H), the value k ∈ Ln and the Hintikka function I ∈ H✸ψ,k to be checked can be selected by nondeterministic choice. Note that, although the size of the set H✸ψ,k can be in O(n|✸ψ| ), for a given function I, we do not need to check every element of H✸ψ,k to see whether I ∈ H✸ψ,k, since we only need to test if I satisfies the conditions of Definition 6 and this can be done within space linear on the size of I.

Hence, by the previous points, every time algorithm Witness is applied to a function H and its domain Cl(ϕ), a subformula ✸ψ ∈ dom(H) is selected and a k ∈ Ln and I ∈ H✸ψ,k are non-deterministically chosen, the space needed is in O(|ϕ|). So, since deg(ϕ) recursive calls are needed until we meet a Hintikka function I whose domain contains no modal formula and deg(ϕ) ≤ |ϕ|, the amount of space required to run the algorithm is O(|ϕ|2 ). Moreover, to keep track of the subformulas that have been checked by the algorithm, it is enough to implement two kinds of pointers to the modal operators occurring in the representation of ϕ: one pointer to indicate that, for a given subformula ✸ψ ∈ dom(H) it has been fully checked whether there is k ∈ Ln and a Hintikka function I ∈ H✸ψ,k such that Witness(I, dom(I)) and the other pointer when the same has not yet been fully checked.

Theorem 12. Sat1(CFr, Łcn,Δ) is in PSPACE.

Proof. It is easy to see that the same algorithm given in Figure 1, but replacing k ∈ Ln with k ∈ {0, 1}, computes Sat1(CFr, Łcn,Δ).

3.2 Satisfiability is PSPACE-hard

Here we will prove that the four problems pointed out at the end of Section 3 are PSPACE-hard.

The PSPACE-hardness of the set Sat1(CFr, Łn) is proved by using a polynomial reduction into the problem of satisifiability for classical Kripke models.

Proof. Let us consider the mapping tr from classical modal formulas into our modal formulas defined by

• tr(p) = p& (n-1) . . . &p, if p is a propositional variable,
• tr(⊥) = ⊥,
• tr(ϕ1 ∧ϕ2) = tr(ϕ1) ∧ tr(ϕ2),
• tr(ϕ1 →ϕ2) = tr(ϕ1) → tr(ϕ2),
• tr(✸ϕ) = ✸ tr(ϕ).

This translation is clearly polynomial (because essentially we are only replacing variables), and by induction on formulas it is easy to check that for all modal formulas ϕ, it holds that

• ϕ is modally satisfiable in a classical Kripke model, iff
• tr(ϕ) is modally satisfiable in a crisp Kripke model.

By the PSPACE-hardness of classical modal logic ([Ladner, 1977]) the proof finishes.

Unfortunately, for the case of the set Sat1(Fr, Łn), the authors do not know how to get the PSPACE-hardness by a reduction from the classical case. Such a reduction can be obtained by the mapping tr′ defined like tr except for the condition

but this reduction is not polynomial. Thus, in order to prove our next theorem we need to go into the details of codifying quantified Boolean formulas QBF (it is well known that validity of QBF is PSPACE-complete). Since we essentially use the same ideas that are used in the classical modal case (see the proof given in [Blackburn et al., 2001, Theorem 6.50]), we will not go into all the details of the proof.

Theorem 14. Sat1(Fr, Łn) is PSPACE-hard.

Proof. Let us consider β a QBF formula. By the proof given in [Blackburn et al., 2001, Theorem 6.50], it is well known how to define (see [Blackburn et al., 2001, p. 390] a classical modal formula f(β) such that

• β is valid, iff
• f(β) is modally satisfiable in a classical Kripke model.

The formula f(β) can also be seen as one of our modal formulas, and it is quite straightforward to check that for the formulas of the form f(β) it happens that

• f(β) is modally satisfiable in a classical Kripke model, iff
• f(β) is modally satisfiable in a Kripke Łn-model.

This fact is based on the properties stated at the end of Section 2.2.

To finish this section let us point that when our language has the Delta operator, this last proof can be simplified quite a lot just by realizing that the reduction tr′ can be somehow converted into one that is polynomial; this is so because

is a valid formula.

4 Conclusions and Open Problems

We have seen in Theorem 1 that the minimal n-valued Łukasiewicz modal logics are PSPACE-complete. An easy consequence of this statement is the fact that the same complexity is obtained when dealing with the entailment problem. In other words, for each one of the modal languages considered in this paper, the set

is PSPACE-complete. This is so because, as a consequence of the definability of Δ in Łn, it holds that ϕ entails ψ iff ϕn-1 → ψ (which coincides with Δϕ → ψ) is modally valid.

On the other hand, there is a close connection between the expressive powers of the minimal n-valued Łukasiewicz modal logic and the one of the description logic Łn-ALC

without knowledge base. Thus, the research in this paper can be understood as a first step towards understanding the complexity of the description logic Łn-ALC when there is a knowledge base.

Finally, it is worth pointing out that the infinite-valued Łukasiewicz modal logic (without Delta and truth constants) has been shown to be decidable in [H´ajek, 2005], but characterizing its computational complexity is still an open problem. This logic is defined like in Section 2.2, but replacing Ln with the Łukasiewicz standard algebra (over [0, 1]), maximum with supremum, and minimum with infimum.

Funding

The authors thank Eurocores (LOMOREVI Eurocores Project FP006/FFI2008-03126-E/FILO), Spanish Ministry of Education and Science (project TASSAT TIN2010-20967C04-01, project ARINF TIN2009-14704-C03-03, project Agreement Techologies CONSOLIDER CSD 2007- 0022), and Catalan Government (2009SGR-1433/34). Marco Cerami has been supported by grant JAEPredoc, n.074 of CSIC.