? Supported by the DFG under grant BA 1122/17-1 (FuzzyDL) and in the research training group 1763 (QuantLA) ?? Supported by the ESF project “Podpora vytváření excelentních výzkumných týmů u intersektorální mobility na Univerzitě Palackého v Olomouci II” No. CZ.1.07/2.3.00/30.0041. The project is co-financed by the European Social Fund and the state budget of the Czech Republic. ? ? ? Partially supported by DFG within the Cluster of Excellence 'Center for Advancing Electronics Dresden'
Fuzzy Description Logics (FDLs) have been introduced to reason about vague or
imprecise knowledge in application domains. In recent years, reasoning in many
FDLs based on infinitely many values has been proved to be undecidable [
The fact that a significant difference in computational complexity between
the crisp and the finite-valued case has not yet been found is mainly due to the
high expressivity of the languages studied so far. Indeed, these languages already
contain significant sources of nondeterminism in the crisp case. Our idea is that
the proof of a possible difference in the complexity between both formalisms has
to be searched in languages that allow for a lower expressivity. In such languages,
the sources of nondeterminism inherent in the classical framework have not yet
shown up, while the same languages may be already affected by the inherent
nondeterminism of the basic logical connectives in the finite-valued framework.
For this purpose, we want to take advantage of the “revival” that simple DL
languages have experienced in recent times. Due to practical reasons, in the
last years there have been different works on the complexity behavior of simple
languages such as those of the EL and DL-Lite families [
The question about the computational complexity of EL under a fuzzy
semantics has been already considered in [
In this work we are not facing the problem directly. Rather, we consider
propositional Horn clauses, which can be seen as a restricted form of
EL?axioms. Reasoning in both formalisms is polynomial under classical two-valued
semantics [
The consequences of our result are not restricted to the framework of Fuzzy
Description Logics, but they obviously go beyond that. Indeed, our result
contributes to achieving a deeper insight into the complexity of reasoning in
fragments of finite-valued propositional Łukasiewicz logic. To the best of our
knowledge, although there are numerous works on the computational complexity of
finite-valued propositional logics [16,19], this kind of problem has not yet been
dealt with in the literature. Perhaps the closest to our approach is the study of
fuzzy answer set programming. In this context, it has been shown that
satisfiability of a set of Horn clauses in restricted form can be decided in polynomial
time [
We now introduce the syntax and semantics of the logical formalism Łn-Horn. The former is given in terms of implications between conjunctions of literals. In contrast to classical propositional logic, we need to allow conjunctions also in the head of an implication due to our many-valued semantics.
This semantics is defined using the operators of finite fuzzy Łukasiewicz chains. For any natural number n 2, we consider the set of n truth values Łn := f0; n1 1 ; : : : ; nn 12 ; 1g together with the following operators: – The finite Łukasiewicz t-norm : Łn Łn
! Łn defined by x y := maxf0; x + y 1g: – The residuum of the finite Łukasiewicz t-norm ) : Łn as Łn
! Łn computed x ) y := minf1; 1 x + yg: As usual in fuzzy logic, these two operators satisfy the property that x y z iff y x ) z for all x; y; z 2 Łn. The algebra hŁn; ; ); 0; 1i is called the finite Łukasiewicz chain of length n.
Definition 1 (syntax). We consider a set V of propositional variables. A fuzzy Horn clause is of the form hx1 & : : : & xk ! y1 & : : : & ym pi or hx1 & : : : & xk ! 0 pi; (1) (2) where k 0, m 1, x1; : : : ; xk; y1; : : : ; ym 2 V, and p 2 Łn. A fuzzy Horn theory is a finite set of fuzzy Horn clauses.
Notice that the conjunction on the left-hand side of a Horn clause might be empty; that is, a Horn clause could have the form h ! y1 & : : : & ym pi.
The semantics of this logic is given in terms of valuations mapping each propositional variable to one of the possible truth degrees.
Definition 2 (semantics). A valuation of the propositional variables is a function v : V ! Łn. A fuzzy Horn clause of the form (1) or (2) is satisfied by v if v(x1) v(x1) v(xk) ) v(y1) v(xk) ) 0 p; respectively; v(ym) p or where the operation of the left-hand side of the implication is evaluated to 1 whenever k = 0. A fuzzy Horn theory H is satisfiable if there is a valuation that satisfies all fuzzy Horn clauses in H.
We show that satisfiability of fuzzy Horn theories in Łn-Horn is NP-complete, in contrast to the classical case, where it can be checked in linear time. The upper bound follows from the fact that one can simply guess a valuation in polynomial time (O(n jVj)) and then check satisfaction of all clauses.
In this section we reduce a variant of the satisfiability problem for (classical) propositional formulae to satisfiability of Horn theories in Łn-Horn, for any n 4. This shows that the problem is NP-hard already for Łukasiewicz chains of length 4; i.e., for chains containing four membership degrees.
Given a set V of variables, the set of literals is V [ f:x j x 2 Vg; that is, a literal is either a variable or a negated variable. For a natural number m, an m-clause is a disjuction of m literals Wim=1 `i. A propositional formula is in m-conjunctive normal form (m-CNF) if it is a conjunction of m-clauses; that is, if is of the form Vik=1 Ci for some k 0, where each Ci; 1 i k is an m-clause. It is well-known that deciding the satisfiability of m-CNF formulae is NP-hard, for any m 3 [17].
Let now n 4 and define m := n 1. Given an m-CNF formula , we construct a fuzzy Horn theory H such that is satisfiable in Łn-Horn if and only if H is satisfiable. For the rest of this section, let = Vik=1 Ci be an arbitrary but fixed formula in m-CNF, and var( ) V be the set of all propositional variables appearing in . For each x 2 var( ), we employ a fresh variable x0 2 V to simulate the literal :x in the fuzzy Horn theory H .
As a first step, we define the Horn theory
H` := fhx & x0 ! 0 fh ! x & x0 1 m i j x 2 var( )g [ m 1 m i j x 2 var( )g: It is easy to see that any valuation v : V ! Łn that satisfies the Horn clause h ! x & x0 mm 1 i must be such that v(x) mm 1 and v(x0) mm 1 , but maxfv(x); v(x0)g = 1. Moreover, if v also satisfies hx & x0 ! 0 m1 i, then it must be the case that minfv(x); v(x0)g = mm 1 . Overall, this means that for every x 2 var( ) and for all valuations v satisfying H`, exactly one of x; x0 is evaluated by v to 1, while the other is evaluated to m 1 m . The intuition of this construction is that we will read v(x) = 1 as evaluating the variable x to true, and v(x) 6= 1 (and hence v(x0) = 1) as evaluating x to false.
Consider now the translation that maps literals to variables, defined by We extend this mapping to m-clauses by setting (`) := (x
if ` = x 2 V x0 if ` = :x; x 2 V: i=1 m m _ `i := & i=1 (`i): Observe that a valuation satisfies the Horn clause h ! &im=1 (`i) m1 i if and only if at least one of the conjuncts (`i) is evaluated to 1; this will correspond to the literal satisfying the clause Wim=1 `i. We thus define the fuzzy Horn theory H := H` [ fh ! (Ci)
is satisfiable iff the fuzzy Horn theory H Proof. If is satisfiable, then there is a propositional valuation V satisfying . We use V to define a fuzzy valuation v : V ! Łn by setting for every x 2 var( ) (1 v(x) := m 1
m v(x0) := 2m 1 m if V (x) = true otherwise; v(x): By construction, this valuation satisfies all the Horn clauses in H`. Consider now the Horn clause h ! (C) m1 i for some m-clause C = Wim=1 `i of . Since V is a model of , there exists an i; 1 i m such that `i is evaluated to true by V . By construction, v( (`i)) = 1, and hence v satisfies the Horn clause.
Conversely, let v be a model of H , and consider the valuation V that maps every variable x to true if v(x) = 1 and to false if v(x) = m 1 m . For any m-clause in , we know that v( (C)) m1 . Thus, there is at least one literal ` appearing in C such that v( (`)) = 1. If ` is a propositional variable x, then v(x) = 1 and V evaluates x to true; hence V satisfies the clause C. Otherwise, we have that ` = :x for some propositional variable x. In this case, v(x) = mm 1 and V evaluates x to false; i.e., V evaluates :x to true, and hence satisfies C. tu Recall that satisfiability of m-CNF formulae is NP-hard for any m 3. Using our construction, since n = m + 1, we obtain that satisfiability of fuzzy Horn theories in Łn-Horn is also NP-hard for any n 4, as desired.
Corollary 4. Satisfiability of fuzzy Horn theories in Łn-Horn is NP-complete for any n 4.
For n = 4, we obtain the chain Ł4 = f0; 1=3; 2=3; 1g containing four membership degrees; thus, our results prove hardness for four-or-more-valued Horn logics. For two-valued Horn logics, which correspond to classical Horn logic, it is wellknown that satisfiability is decidable in linear time [18]. Unfortunately, the case of three-valued semantics is not covered by our result. 4
In this paper we have shown that increasing the set of membership degrees over which propositional variables are interpreted may have negative effects on the complexity of reasoning. Specifically, for Horn theories under finite-valued Łukasiewicz semantics, the complexity of deciding satisfiability increases from linear time—for the classical two-valued case—to NP-complete for the fourvalued (or higher) case. To the best of our knowledge, the precise complexity of satisfiability in three-valued Horn theories is still unknown, but we conjecture that it is NP-complete in this case as well.
The main motivation for our work is to understand the complexity of
reasoning in fuzzy extensions of tractable description logics, such as EL. Horn clauses
of the form (1) are expressible in (fuzzy) EL using fuzzy general concept
inclusions like hA1 u u Ak v B1 u u Bm pi, where Ai; Bj are concept names.
Unfortunately, to express the constant 0 in clauses of the form (2), we need the
additional constructor ?. Thus, while our hardness results do not transfer
directly to the case of Łn-EL, our result shows that reasoning in Łn-E L?, which
is also polynomial in the two-valued case [
As future work we plan to continue our task to determine the complexity of reasoning in fuzzy extensions of description logics. Our first goal is to find tight complexity bounds for extensions of EL with different fuzzy semantics. We are also interested in covering the missing case of Horn theories in Ł3-Horn. 13. Brandt, S.: Polynomial time reasoning in a description logic with existential restrictions, GCI axioms, and—what else? In: Proc. of the 16th Eur. Conf. on Artificial Intelligence (ECAI’04). pp. 298–302. IOS Press (2004) 14. Calvanese, D., De Giacomo, G., Lembo, D., Lenzerini, M., Rosati, R.: DL-Lite: Tractable description logics for ontologies. In: Proc. of the 20th Nat. Conf. on Artificial Intelligence (AAAI’05). pp. 602–607. AAAI Press (2005) 15. Cerami, M., Straccia, U.: On the (un)decidability of fuzzy description logics under Łukasiewicz t-norm. Information Sciences 227, 1–21 (2013) 16. Cintula, P., Hájek, P., Noguera, C. (eds.): Handbook of Mathematical Fuzzy Logic, 2 volumes. College Publications (2011) 17. Cook, S.A.: The complexity of theorem-proving procedures. In: Proc. of the 3rd
Annual ACM Symp. on Theory of Computing (STOC’71). pp. 151–158 (1971) 18. Dowling, W.F., Gallier, J.H.: Linear-time algorithms for testing the satisfiability of propositional Horn formulae. Journal of Logic Programming 1(3), 267–284 (1984) 19. Hähnle, R.: Tutorial: Complexity of many-valued logics. In: Proc. of the 31st Int.
Symp. on Multiple-Valued Logics (ISMVL’01). pp. 137–146. IEEE Press (May 2001), invited Tutorial 20. Mailis, T., Stoilos, G., Simou, N., Stamou, G.B., Kollias, S.: Tractable reasoning with vague knowledge using fuzzy EL++. Journal of Intelligent Information Systems 39(2), 399–440 (2012)