Standard and Non-Standard Inferences in the Description Logic FL0 Using Tree Automata (Abstract)?

Franz Baader

Oliver Fernández Gil

Maximilian Pensel

0 0 Chair for Automata Theory , Theoretical Computer Science, TU Dresden , Germany

In the early days of Description Logic (DL) research, the inexpressive DL FL0, which has only conjunction, value restriction and the top concept as concept constructors, was considered to be the smallest possible DL. It came as a surprise when it was shown that subsumption reasoning w.r.t. acyclic FL0 terminologies (TBoxes) is coNP-hard. The complexity increases when more expressive forms of TBoxes are used: for cyclic TBoxes to PSpace and for general TBoxes consisting of general concept inclusions (GCIs) even to ExpTime. Thus, w.r.t. general TBoxes, subsumption reasoning in FL0 is as hard as in ALC, its closure under negation. In addition to standard inferences such as the subsumption and the instance problem, also various non-standard inferences, such as unification or computing the least common subsumer, were investigated for various DLs. For FL0, there are, however, very few results that consider general TBoxes. In the ExpTime-completeness result for subsumption in FL0 w.r.t. general TBoxes, the ExpTime upper bound is actually inherited from the more expressive DL ALC. Dedicated subsumption algorithms and nonstandard inferences have been considered mostly for the case without TBoxes or w.r.t. a restricted form of (acyclic and cyclic) TBoxes in FL0 and its extension by number restrictions. Here, we use automata working on infinite trees to solve both standard and non-standard inferences in FL0 w.r.t. general TBoxes.1 On the one hand, we give an alternative proof of the ExpTime upper bound for subsumption in FL0 w.r.t. general TBoxes based on the use of looping tree automata. On the other hand, we employ parity tree automata to tackle the non-standard inference problems of computing the least common subsumer and the difference of FL0 concepts w.r.t. general TBoxes. To show our results, we basically proceed as follows: 1. We introduce the so-called least functional model of an FL0 concept w.r.t. an FL0 TBox, and prove that subsumption corresponds to inclusion of least functional models. Basically, a functional model is an infinite tree where every node has exactly one successor for every role. Such trees can be ordered by inclusion, i.e., by pairwise comparing the sets of concept names to which the nodes reached by the same role chain belong.

2. Then we show that such least functional models can be represented using socalled looping tree automata (LTAs): given an FL0 concept C and a general TBox T , we can construct an LTA AbC;T whose size is at most exponential in the size of C and T such that AbC;T accepts exactly the least functional model of C w .r.t. T . Using the product construction for LTAs, inclusion of least functional models can then be reduced to the emptiness problem for LTAs. Since the emptiness problem for LTAs is in P and the automata have at most exponential size, this yields the desired ExpTime upper bound for subsumption in FL0 w .r.t. general TBoxes. Note that, in contrast to the case of acyclic or cyclic TBoxes, where automata on finite or infinite words can be employed to decide subsumption, GCIs require the use of automata working on trees .

3. To deal also with non-standard inferences such as computing the least common subsumer (lcs) or the difference of two FL0 concepts w .r.t. a general FL0 TBox, the automata constructions need to be extended considerably. Instead of constructing an automaton that represents the least functional model of a fixed FL0 concept C, we now need to build an automaton accepting all trees representing least functional models of some FL0 concept w .r.t. T . For this task, simple LTAs (which do not have an acceptance condition) are not sufficient; instead we use parity tree automata (PTAs), which use a set of so-called priorities in their acceptance condition. The construction of a PTA AbT that accepts exactly the trees that are least functional models of some FL0 concept C w .r.t. a given general TBox T is quite involved. It makes use of the closure of PTAs under intersection, complement, and projection. The PTA AbT constructed this way has double-exponentially many states and exponentially many priorities in the size of T .

4. Given FL0 concepts C; D, their least common subsumer (lcs) w .r.t. a general TBox T is the the most specific concept that subsumes C and D w .r.t. T . In general, the lcs need not exist if the TBox contains cyclic dependencies between concepts. We can show that it exists iff the intersection of the least functional models of C and D w .r.t. T is a least functional model of some FL0 concept w .r.t. T . To decide whether the lcs exists, we can thus proceed as follows. We construct the automata AbC;T and AbD;T , and use the product construction to obtain an automaton for the intersection of the least functional models of C and D. Using an additional product construction and the emptiness test for PTAs, one can then decide whether this intersection is accepted by AbT . The complexity of this decision procedure is in 2NExpTime \ co-2NExpTime.

5. The difference of FL0 concepts can be treated similarly, by using difference rather than intersection of least functional models.

Baader , F. , Fernández Gil , O. , Pensel , M. : Standard and non-standard inferences in the description logic FL0 using tree automata . In: GCAI 2018 , 4th Global Conference on Artificial Intelligence. EPiC Series in Computing 55 , pages 1 - 14 , EasyChair ( 2018 ).