In the last few years, the complexity of reasoning in fuzzy description logics has been studied in depth. Surprisingly, despite being arguably the simplest form of fuzzy semantics, not much is known about the complexity of reasoning in fuzzy description logics using the Gdel t-norm. It was recently shown that in the logic G-IALC under witnessed model semantics, all standard reasoning problems can be solved in exponential time, matching the complexity of reasoning in classical ALC. We show that this also holds under general model semantics.
Introduction Fuzzy Description Logics (DLs) have been studied as a means of representing vague or imprecise knowledge in a formal and well-understood manner. In contrast to classical DLs, the semantics of fuzzy DLs are based on fuzzy sets. Fuzzy sets associate every element of the domain with a number from the interval [0; 1], which represents the degree to which the element belongs to the fuzzy set.
When dening a fuzzy DL, one must decide how to interpret the logical constructors to handle the truth degrees. The simplest approach is to use the minimum operator for conjunctions to generalize intersection to fuzzy sets. Thus, the degree of membership of a conjunction is interpreted as the minimum of the membership degrees of the conjuncts. This operation, called the Gdel t-norm , can be used to interpret all other logical constructors in a formally justied manner [19,22]. The quantiers 8 and 9 are interpreted as inma and suprema of truth values, respectively. To avoid problems with innitely many truth values, reasoning in fuzzy DLs is often restricted to so-called witnessed models [21].
The study of fuzzy DLs underwent a large change in recent years, after some
relatively inexpressive fuzzy DLs were shown to be undecidable when reasoning
w.r.t. general ontologies [
Despite being widely regarded as the simplest t-norm, surprisingly little is
known about fuzzy DLs based on Gdel semantics. It was generally believed
that these logics are decidable, but no proof existed to support this claim. The
only results for similar logics restrict reasoning a priori to a nite subset of
[0; 1]; in this case, a reduction to classical reasoning yields decidability [
In this paper, we extend the analysis of reasoning in G-IALC to the case of
general models, adapt the automata-based algorithm from [
Preliminaries
We briey introduce the basic notions of G-IALC and order structures. The
two basic operators of Gdel fuzzy logic are conjunction and implication,
interpreted by the Gdel t-norm and its residuum. The Gdel t-norm is the binary
function min(x; y) on [
y otherwise.
For a deeper introduction to t-norm-based fuzzy logics, see [
A total preorder over a set S is a transitive and total binary relation . on S. For x; y 2 S, we write x y if x . y and y . x. Notice that is an equivalence relation on S. Similarly, we write x < y if x . y, but not y . x. We write ./ for an arbitrary element of f=; ; >; ; <g, and ./ for the corresponding relation induced by . , i.e. , & , > , . , or < . Subscripts are used to distinguish these relations for dierent total preorders.
An order structure S is a nite set containing the numbers 0, 0:5, and 1, together with an involutive unary operation inv : S ! S such that inv(x) = 1 x for all x 2 S \ [0; 1]. For an order structure S, order(S) denotes the set of all total preorders . over S that have 0 and 1 as least and greatest element, respectively, preserve the order of real numbers on S \ [0; 1], and satisfy x . y i inv(y) . inv(x) for all x; y 2 S. Given . 2 order(S), the following functions on S are well-dened since . is total: min (x; y) := (x if x . y y otherwise res (x; y) := (1 if x . y y otherwise It is easy to see that these operators agree with min and ) on the set S \ [0; 1].
Let NI, NR, and NC be sets of individual, role, and concept names, respectively. G-IALC concepts are built as follows, where A 2 NC and r 2 NR:
C ::= A j > j :C j C u C j C ! C j 9r:C j 8r:C: We call concepts of the form 9r:C or 8r:C quantied concepts . An interpretation is a pair I = ( I ; I ), where I is a non-empty domain, and I maps every a 2 NI to an element aI 2 I , every A 2 NC to a fuzzy set AI : I ! [0; 1], and every r 2 NR to a fuzzy binary relation rI : I I ! [0; 1]. The interpretation of complex concepts is shown in Table 1. In G-IALC, one can simulate the additional constructors bottom, residual negation, and disjunction, by using >, :, u, and !. The knowledge of a domain is represented using axioms that restrict the class of interpretations that are relevant for the dierent reasoning tasks. Denition 1 (axioms). A crisp assertion is either a concept assertion a : C or a role assertion (a; b) : r for a concept C, r 2 NR, and a; b 2 NI. An (order) assertion is of the form h ./ i, where is a crisp assertion and is either a crisp assertion or a value from [0; 1]. An interpretation I satises an order assertion h ./ i if I ./ I , where (a : C)I := CI (aI ), ((a; b) : r)I := rI (aI ; bI ), and qI := q for all q 2 [0; 1]. An ordered ABox A is a nite set of order assertions. An interpretation is a model of A if it satises all order assertions in A.
A general concept inclusion (GCI) is an expression of the form hC v D qi for concepts C; D, and q 2 [0; 1]. An interpretation I satises this GCI if CI (x) ) DI (x) q holds for all x 2 I . A TBox is a nite set of GCIs. An ontology is a pair O = (A; T ), where A is an ordered ABox and T is a TBox. An interpretation is a model of a TBox T if it satises all GCIs in T , and it is a model of an ontology O = (A; T ) if it is a model of both A and T . Ordered ABoxes are more expressive than ABoxes usually considered in fuzzy DLs [27] since they allow to state order relations between concepts and roles. This more general kind of ABox is better suited for our algorithms.
We denote by sub(O) the closure under negation of the set of all subconcepts appearing in an ontology O. The concepts ::C and C are equivalent, and we regard them here as equal; thus, sub(O) is nite. By VO we denote the closure under the operator x 7! 1 x of the set of all truth degrees appearing in O, together with 0, 0:5, and 1. Since this operator is involutive, VO is also nite. We denote the elements of VO [0; 1] as 0 = q0 < q1 < < qk = 1.
As with classical DLs, the most basic reasoning task in G-IALC is to decide ontology consistency. One may also be interested in computing the degree to which an entailment holds.
Denition 2 (reasoning). An ontology O is consistent if it has a model. Given p 2 [0; 1], a concept C is p-satisable w.r.t. O if there is a model I of O and an x 2 I with CI (x) p. The best satisability degree of C w.r.t. O is the supremum over all p such that C is p-satisable w.r.t. O. C is p-subsumed by a concept D w.r.t. O if all models of O satisfy the GCI hC v D pi. The best subsumption degree of C and D w.r.t. O is the supremum over all p such that C is p-subsumed by D w.r.t. O.
In this paper, we consider only the consistency problem for ontologies O = (A; T )
where A is a local ordered ABox, i.e. it contains no role assertions and uses only
a single individual name a. For all other reasoning problems, one can use exactly
the same reductions to local consistency as in [
Deciding Local Consistency Let O = (A; T ) be an ontology with a local ordered ABox using the individual name a. Our algorithm is based on the observation that the axioms and the semantics of the constructors only introduce restrictions on the order of the values that models can assign to concepts, not on the values themselves. For example, an interpretation I satises ha : (A ! B) = pi with p < 1 i AI (aI ) > BI (aI ) and BI (aI ) = p. Thus, rather than building a model directly, we rst create an abstract representation of a model that encodes only the order between concepts. This will be achieved through an order structure on VO [ sub(O).
As in classical ALC, it suces to consider tree-shaped models. Since the values of concepts in a node of this tree are also restricted by the values of concepts at the parent node, we additionally introduce expressions of the form C" to refer to the value of C at the parent node. We additionally use a new element to represent the degree of the role connection from the parent node. Denition 3 (order structure U ). We dene sub"(O) := fC" j C 2 sub(O)g and the order structure U := VO [ sub(O) [ sub"(O) [ f ; : g with inv( ) := : , inv(C) := :C, and inv(C") := (:C)" for all C 2 sub(O).
For convenience, we extend the notation of sub"(O) by setting q" := q for q 2 VO.
Using total preorders from order(U ), we can describe the relationships between all the subconcepts from O and the truth degrees from VO at given domain elements. Such a preorder can be seen as the type of a domain element, from which a tree-shaped interpretation, represented by a Hintikka tree, can be built.
In the following, let n be the number of quantied concepts in sub(O) and a xed bijection between the set of all quantied concepts in sub(O) and f1; : : : ; ng that species which quantied concept is satised by which successor in the Hintikka tree. For a given role r 2 NR, we denote by r the set of all indices (E) where E 2 sub(O) is a quantied concept of the form 9r:C or 8r:C. Denition 4 (Hintikka ordering). A Hintikka ordering is a total preorder .H 2 order(U ) that satises the following conditions for every C 2 sub(O): C = > implies C H 1, if C = D1 u D2, then C if C = D1 ! D2, then C
H minH (D1; D2),
H resH (D1; D2).
This preorder is compatible with the TBox T if for every GCI hC v D qi 2 T we have resH (C; D) &H q. It is compatible with A if for every order assertion ha : C ./ qi or ha : C ./ a : Di in A, we have C ./H q or C ./H D, respectively. These conditions ensure that the semantics of all propositional constructors is preserved (the order structure U already takes care of the involutive negation). The following denition deals with the quantied concepts.
Denition 5 (Hintikka condition). A tuple (.0; .1; : : : ; .n) of Hintikka orderings satises the Hintikka condition if: for every 1 i n and all ; 2 VO [ sub(O), we have .0 i " .i "; for every 9r:C 2 sub(O), we have (9r:C)" &i mini( ; C) for all i 2 r, and for i = (9r:C) and every 2 VO [ sub(O) with (9r:C)" >i " we have mini( ; C) >i "; and for every 8r:C 2 sub(O), we have (8r:C)" .i resi( ; C) for all i 2 r, and for i = (8r:C) and every 2 VO [ sub(O) with (8r:C)" <i ", we have resi( ; C) <i ".
Here lies the main dierence to [
A Hintikka tree for O is an innite n-ary tree,3 where every node u is associated with a Hintikka ordering .u compatible with T , such that: every tuple (.u; .u1; : : : ; .un) satises the Hintikka condition, and ." is compatible with A.
Proposition 6. If there is a Hintikka tree for O, then O has a model. Proof. Given a Hintikka tree, we construct a model in two steps. In the rst step, we recursively dene a function v : U (f1; : : : ; ng N) ! [0; 1]. For a word u = (i0; m0) : : : (i`; m`) 2 (f1; : : : ; ng N) , let 1(u) := i0 : : : i` 2 f1; : : : ; ng denote its projection to the rst component. The mapping v will satisfy the following conditions for all ; 2 U and all u 2 (f1; : : : ; ng N) : (P1) for all values q 2 VO we have v(q; u) = q, (P2) v( ; u) v( ; u) i . 1(u) , (P3) v(inv( ); u) = 1 v( ; u), (P4) for all 9r:C 2 sub(O), we have v(9r:C; u) = sup sup min(v( ; u (i; m)); v(C; u (i; m)));
i2 r m2N (P5) for all 8r:C 2 sub(O), we have v(8r:C; u) = inf inf v( ; u (i; m)) ) v(C; u (i; m)):
i2 r m2N
In the second step, we construct, with the help of this function v, an
interpretation Iv = ((f1; : : : ; ng N) ; Iv ) satisfying CIv (u) = v(C; u) for all concepts C
and all u 2 (f1; : : : ; ng N) , and show that Iv is indeed a model of O.
Step 1. The function v is dened recursively, starting from the root node ". Let
U = " be the set of all equivalence classes of ". Then ." yields a total order
on U = ". In particular, [0]" <" [q1]" <" [q2]" <" <" [qk 1]" <" [
We rst dene an auxiliary function v~" : U = " ! [0; 1]. For all q 2 VO we set
v~"([q]") := q. It remains to dene a value for all equivalence classes that do not
contain a value from VO. Notice that due to the minimality of [0]" and maximality
of [
For the recursion step, assume that we have already dened v for a node u 2 (f1; : : : ; ng N) such that (P1)(P3) are satised at u, let u1 := 1(u), and consider the next pair (i; m) 2 f1; : : : ; ng N. We initialize the auxiliary function v~u;i : U = u1i ! [0; 1] by setting v~u;i([q]u1i) := q for all q 2 VO and v~u;i([C"]u1i) := v(C; u) for all C 2 sub(O). To see that this is well-dened, consider the case that [C"]u1i = [D"]u1i, i.e. C" u1i D". From the Hintikka condition, we get C 1(u) D, and from (P2) at u we obtain v(C; u) = v(D; u). Similarly, one can show that [q]u1i = [C"]u1i implies v(q; u) = v(C; u). For the remaining equivalence classes, we use a construction similar to (1) by considering all neighboring equivalence classes that contain an element of VO [ sub"(O) (whose values are already xed) and evenly distributing the values between them.
To ensure that the semantics of the role restrictions are respected at the node u, we consider rst the case that i = (9r:C) for 9r:C 2 sub(O) and dene v( ; u (i; m)) for 2 U as follows: <>8 22mm22mm 11 ff ((((9:r9:rC: C))) +)+21m21mf (f () ) if (:9r:C) <u1i " if minu1i( ; C) .u1i " "
<u1i (9r:C)", .u1i inv(minu1i( ; C)), otherwise, >:f ( ) where f ( ) := v~u;i([ ]u1i). That is, we let min(v( ; u (i; m)); v(C; u (i; m))) approach v(9r:C; u) with increasing m, and do the same for all values in between. This is well-dened since, if lies in both intervals, then the Hintikka condition yields minu1i( ; C) u1i inv(minu1i( ; C)) <u1i (9r:C)". But this is impossible since U is an order structure, and thus minu1i( ; C) u1i 0:5 <u1i (9r:C)", which contradicts the Hintikka condition. If i corresponds to a value restriction, we use a similar denition where (9r:C)" is replaced by (8r:C)", minu1i( ; C) is replaced by resu1i( ; C), and the order is inverted.
We now verify that (P1)(P5) hold for this v at all u (i; m). (P1) is satised by the denition of v~u;i and the Hintikka condition. For (P2), observe that the Hintikka ordering .u1i is preserved by the denition of v~u;i and the denition of v at u (i; m) only compresses the distances between neighboring equivalence classes, but does not aect their ordering. (P3) also holds because it is valid at u (i; 0) and all shifts towards (9r:C) for increasing m are mirrored for (:9r:C)", and similarly for value restrictions. W"e now verify (P4); (P5) follows from dual arguments. For this, consider any 9r:C 2 sub(O) and i := (9r:C). From the construction and the Hintikka condition, we know that
msu2pN min(v( ; u (i; m)); v(C; u (i; m))) = v((9r:C)" ; u (i; m)) = v(9r:C; u):
min(v( ; u (j; m)); v(C; u (j; m))) v((9r:C)" ; u (j; m)) = v(9r:C; u) from the Hintikka condition and (P2).
Step 2. We dene the interpretation Iv over the domain I := (f1; : : : ; ng N) as follows. For every concept name A 2 NC and all domain elements u, we set AIv (u) := (v(A; u) if A 2 sub(O),
0 otherwise.
For every role name r 2 NR and all domain elements u, we likewise dene rIv (u; w) := (v( ; w) if w = u (i; m) with i 2 0 otherwise.
r,
Finally, we dene aIv := " for the individual name a. It can be shown by
induction on the structure of C, using similar arguments as in [
It remains to show that Iv is indeed a model of O. For every ha : C ./ qi 2 A, the Hintikka tree satises C ./" q, and thus we obtain from (2), (P1), and (P2):
CIv (aIv ) = v(C; ") ./ v(q; ") = q; and similarly for assertions of the form ha : C ./ a : Di.
Consider now u 2 I and hC v D qi 2 T . Since q 2 VO and . 1(u) is compatible with T , it must hold that q . 1(u) res 1(u)(C; D) = 1 if C . 1(u) D D if D < 1(u) C = 1 if v(C; u) v(D; u) D if v(D; u) < v(C; u); where the second equality is due to (P2). Thus, we obtain v(1; u) if v(C; u) v(D; u) v(D; u) if v(D; u) < v(C; u) = CIv (u) ) DIv (u): q = v(q; u) from (2), (P1), and (P2).
Conversely, every model can be unraveled into an innite tree, and then we can abstract from the specic values by just considering the ordering between the elements of U , which yields a Hintikka tree.
Proposition 7. If O has a model, then there is a Hintikka tree for O. tu Proof. Let I be a model of O. We use this model to construct a Hintikka tree for O and recursively generate a mapping g : f1; : : : ; ng ! I specifying which domain elements correspond to the nodes in the tree. This mapping satises the following condition for all ; 2 VO [ sub(O) and all u 2 f1; : : : ; ng : (P6) .u i
I (g(u))
I (g(u)), where we dene qI (x) := q for all q 2 VO and x 2 I .
We rst consider the root node " of the tree. Recall that the ontology contains a local ordered ABox that uses only the individual name a. We dene g(") := aI and the Hintikka ordering ." as follows for all ; 2 VO [ sub(O): ." i
I (aI )
I (aI ):
We extend this order to the elements in sub"(O) [ f ; : g arbitrarily, such that
for all ; 2 U we have ." i inv( ) ." inv( ). It is easy to show that ." is
an element of order(U ) satisfying (P6) at ", and that ." is a Hintikka ordering
that is compatible with T (cf. [
Assume now that we have already dened g(u) and .u for u 2 f1; : : : ; ng such that (P6) is satised. For all i 2 f1; : : : ; ng, we construct .ui such that (.u; .u1; : : : ; .un) satises the Hintikka condition. For brevity, we consider only the case i = (9r:C); value restrictions can be handled using similar arguments.
If there is a yi 2 I such that (9r:C)I (g(u)) = min(rI (g(u); yi); CI (yi)), then we dene g(ui) := yi, and .ui for all ; 2 U by .ui i
I (g(ui))
I (g(ui)); (3) where we abbreviate I (g(ui)) := rI (g(u); g(ui)) and (D")I (g(ui)) := DI (g(u)) for all concepts D 2 sub(O). It is clear that .ui behaves on VO [ sub"(O) exactly as .u does on VO [ sub(O). As for the root node, it is easy to show that .ui is actually a Hintikka ordering compatible with T .
If there is no such element yi, then the set fmin(rI (g(u); y); CI (y)) j y 2 I g must contain an innite increasing chain whose supremum is (9r:C)I (g(u)). Let (yj)j2N be the domain elements corresponding to these increasing values, and dene .yj for each j 2 N as follows for all ; 2 U : .yj i
I (yj)
I (yj): (4) As before, this denes Hintikka orderings compatible with T that behave on VO [ sub"(O) exactly as .u on VO [ sub(O). Since there are only nitely many such orderings, we can nd a Hintikka ordering .ui and an innite subsequence (yj` )`2N such that .yj` = .ui for all ` 2 N. We now dene g(ui) := yj0 and .ui as above, which obviously satises (P6).
We show the Hintikka condition for (.u; .u1; : : : ; .un), again considering only the existential restrictions 9r:C 2 sub(O). For all i 2 r, we have (9r:C)I (g(u)) = sup min rI (g(u); y); CI (y) y2 I min rI (g(u); g(ui)); CI (g(ui)) ; which shows that (9r:C)" &ui minui( ; C). For i = (9r:C), assume that there is an 2 VO [ sub(O) with (9r:C)" >ui ", and thus we have 9r:C >u . By (P6), we obtain (9r:C)I (g(u)) > I (g(u)). If we have dened .ui directly via (3), then min( I (g(ui)); CI (g(ui))) = (9r:C)I (g(u)) > I (g(u)), and thus minui( ; C) >ui ", as required. If we have chosen .ui as one of the Hintikka orderings dened by (4), assume that minui( ; C) .ui ". Then, for all ` 2 N, min(rI (g(u); yj` ); CI (yj` )) I (g(u)) < (9r:C)I (g(u)); thus the supremum of these values is not equal to (9r:C)I (g(u)), contradicting our construction.
Finally, for every ha : C ./ qi 2 A, we have CI (aI ) ./ q, and thus C ./" q by the denition of .", and similarly for assertions of the form ha : C ./ a : Di. Hence, the tree dened by .u, for u 2 f1; : : : ; ng , is a Hintikka tree for O. tu These propositions show that Hintikka trees characterize consistency of ontologies with a local ordered ABox. That is, deciding the existence of a Hintikka tree for O suces for deciding consistency of O. We now show that the former problem can be solved in exponential time in the size of O. For this, we construct a looping tree automaton whose runs correspond exactly to such Hintikka trees. This automaton accepts a non-empty language i the ontology O is consistent.
A looping automaton over n-ary (innite) trees is a tuple A = (Q; I; ), consisting of a non-empty set Q of states, a subset I Q of initial states, and a transition relation Qn+1. A run of this automaton is a mapping : f1; : : : ; ng ! Q such that (i) (") 2 I, and (ii) for all u 2 f1; : : : ; ng , we have (u); (u1); : : : ; (un) 2 . A is non-empty i it has a run. Denition 8. The Hintikka automaton for an ontology O is the looping tree automaton AO := (QO; IO; O), where
IO := f.H 2 QO j .H is compatible with Ag, and
O contains all tuples from Qn+1 that satisfy the Hintikka condition.
O It is easy to see that the runs of AO are exactly the Hintikka trees for O. The cardinality of U = VO [ sub(O) [ sub"(O) [ f ; : g is linear in the size of O and the number of Hintikka orderings for O is bounded by 2jUj2 . Likewise, the arity n of AO is bounded by jsub(O)j, which is linear in the size of O. Thus, the size of the Hintikka automaton AO is exponential in the size of O. Since emptiness of looping tree automata can be decided in polynomial time [30], we obtain an ExpTime-decision procedure for consistency of ontologies with local ordered ABoxes in G-IALC. The complexity of classical ALC [25] yields a matching lower bound. Theorem 9. Consistency in G-IALC w.r.t. local ordered ABoxes and general models is ExpTime-complete.
It is easy to adapt the decision procedures for ontology consistency where the
ABox need not be local, and for concept satisability and subsumption from [
The algorithm for concept satisability is based on the observation that the ABox is irrelevant for this inference since G-IALC does not include nominals and we can check consistency of the ontology beforehand. Thus, C is p-satisable w.r.t. O = (;; T ) i (fha : C pig; T ) is (locally) consistent, where a is an arbitrary individual name. To obtain the best satisability degree, only polynomially many local consistency tests of the above kind, one for each value in VO, are needed. The reason for this is that, given p; p0 2 (qi; qi+1) for two consecutive values qi; qi+1 2 VO, the Hintikka trees for (fha : C pig; T ) stand in a natural bijection to those for (fha : C p0ig; T ), and thus C is p-satisable i it is p0-satisable. Similar arguments hold for deciding subsumption and computing best subsumption degrees between concepts. 4
Conclusions We have studied the standard reasoning problems for the fuzzy DL G-IALC w.r.t. general model semantics. We showed that all standard reasoning problems can be solved in exponential time. To achieve this, we developed an automaton that decides the existence of a Hintikka tree, which is an abstract representation of a model of a given ontology. The main insight needed for this approach is that we can abstract from the precise truth degrees assigned by an interpretation, and focus only on their ordering.
Our results complement those recently developed in [
As an added benet, in our formalism we can express order assertions like hana : Tall > bob : Talli, intuitively stating that Ana is taller than Bob, without needing to specify the precise degrees to which ana and bob belong to the concept Tall. Such assertions provide useful expressivity for the representation of domain knowledge. This is similar to [23,24], where values can even be compared at unnamed domain elements.
As we have developed an automata-based algorithm, it is natural to ask
whether previous automata-based approaches [
Acknowledgements. The authors would like to thank F. Baader for fruitful discussions that led to the development of this paper. 18. Guller, D.: On the satisability and validity problems in the propositional Gdel logic. Computational Intelligence 399, 211227 (2012) 19. HÆjek, P.: Metamathematics of Fuzzy Logic (Trends in Logic). Springer-Verlag (2001) 20. HÆjek, P.: Making fuzzy description logic more general. Fuzzy Sets and Systems 154(1), 115 (2005) 21. HÆjek, P.: On witnessed models in fuzzy logic. Mathematical Logic Quarterly 53(1), 6677 (2007) 22. Klement, E.P., Mesiar, R., Pap, E.: Triangular Norms. Trends in Logic, Studia
Logica Library, Springer-Verlag (2000) 23. Lu, J., Kang, D., Zhang, Y., Li, Y., Zhou, B.: A family of fuzzy description logics with comparison expressions. In: Proc. of the 3rd Int. Conf. on Rough Sets and Knowledge Technology (RSKT’08). Lecture Notes in Computer Science, vol. 5009, pp. 395402. Springer-Verlag (2008) 24. Lutz, C.: Description logics with concrete domains - a survey. In: Advances in Modal Logic 4 (AiML’02). pp. 265296. King’s College Publications (2003), http: //www.aiml.net/volumes/volume4/Lutz.ps 25. Schild, K.: A correspondence theory for terminological logics: Preliminary report. In: Proc. of the 12th Int. Joint Conf. on Articial Intelligence (IJCAI’91). pp. 466471. Morgan Kaufmann (1991), http://ijcai.org/Past%20Proceedings/ IJCAI-91-VOL1/PDF/072.pdf 26. Stoilos, G., Stamou, G.B., Pan, J.Z., Tzouvaras, V., Horrocks, I.: Reasoning with very expressive fuzzy description logics. Journal of Articial Intelligence Research 30, 273320 (2007) 27. Straccia, U.: Reasoning within fuzzy description logics. Journal of Articial Intelligence Research 14, 137166 (2001) 28. Straccia, U.: Description logics over lattices. International Journal of Uncertainty,
Fuzziness and Knowledge-Based Systems 14(1), 116 (2006) 29. Straccia, U., Bobillo, F.: Mixed integer programming, general concept inclusions and fuzzy description logics. Mathware & Soft Computing 14(3), 247259 (2007), http://ic.ugr.es/Mathware/index.php/Mathware/article/view/21 30. Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logics of programs. Journal of Computer and System Sciences 32(2), 183221 (1986)