Query Entailment Problem for S

Prelegent(ci)

Vincent Michielini

Afiliacja

University of Warsaw

Język referatu

angielski

Termin

5 marca 2025 14:15

Pokój

p. 5440

Tytuł w języku polskim

Query Entailment Problem for S

Seminarium

Seminarium „Teoria automatów”

---

In description logic, possibly infinite structures are described via an 
ABox A (i.e. a basic finite structure, to be completed), and an ontology 
T (or a TBox, a finite set of constraints aiming to complete the ABox). 
The query entailment problem asks the following: given an ABox A, a TBox 
T, and a conjunctive query q (= a subgraph), does any structure 
satisfying A and T necessarily also satisfy the request?

In ALC, the basic description logic (which is nothing more than modal 
logic in disguise), this problem is well understood, as it is known to 
be ExpTime-complete in combined complexity, and coNP-complete in data 
complexity (i.e. with TBox and query fixed) [Lutz '08].

However, the exact complexity for S, the extension of ALC where some 
roles (= binary relations) are specified to be transitive, was not known 
yet. The status being that the problem is coNExpTime-hard [Eiter et al. 
'09] and in 2ExpTime [Calvanese et al. '98]. Two articles in 2009 and 
2010 tried to close the gap by proving coNExpTime-completeness in 
special cases, but the general question remained open.

In this seminar, we finally answer this question by showing that the 
query entailment problem for S is actually 2-ExpTime complete. In fact, 
we show that the complexity gap is associated with the number of 
transitive roles: two distinct transitive roles are enough to get 
2-ExpTime-hardness, while the case with only one transitive role (and 
possibly many non-transitive ones) is in coNExpTime.

This latter case is proven by showing that whenever q is not entailed by 
(A,T), then there exists a counterexample with a representation of 
exponential size (while being most certainly infinite). In the talk, we 
will show how some variant of automata over infinite trees can be 
elegantly used in order to obtain such a representation. We will also 
highlight the crucial difficulties induced by two distinct transitive 
roles, that were overlooked so far.

---