ing Temporal ABoxes in TDL-Lite (Extended Abstract)? ?? We propose an approach for abstracting temporal ABoxes over temporal DLLite knowledge bases (KBs) [2,3,1,4,12] to improve the reasoning performance when dealing with large ABoxes. We consider here the logic TDL-Lite(N), i.e., the fragment of the logic TF P X DL-LitebNool [3], combining DL-LitebNool with LTL, but with just future temporal operators and thus interpreted over the natural numbers. Let NC; NI; NG; NL be sets of concept, individual, global role, and local role names, respectively. The union NG [NL is the set NR of role names. TDL-Lite roles R, basic concepts B, and (temporal) concepts C are given by the following grammar where L 2 NL, G 2 NG, A 2 NC, and q 2 N: R ::= L j L j G j G ; C ::= B j :C j C1 u C2 j 3F C j #F C: A TBox, T , is a set of general concept inclusions (GCI) of the form C1 v C2, where C1; C2 2 NC. An ABox. A, is a set of concept assertions of the form #nA(a) or #n:A(a), or role assertions of the form n#+n1RA((aa;)b=) o#r ##n:R(a; b), where a; b 2 NI, and n 2 N (with, #0A(a) = A(a), # n A(a)). A TDL-Lite KB is a pair, K = (T ; A). The key idea is to map a TDL-Lite KB into an equisatis able LTL formula by applying the translation described in [3], and then abstracting large temporal ABoxes by adapting the technique presented in [9]. Given a TDL-Lite ABox we rst shift all role assertions associated to global roles to time point 0, and call the resulting ABox AG. We then map AG into AyG a rst-order temporal formula with unary predicates, QT L1(N): ? Extended version published as arXiv:2008.07463 ?? Copyright c 2021 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
B ::= ? j A j qR; AyG =
AG ^ ^
n(Eq R)(a); R2roleT ; nR(a;b)2AG (1) where roleT is the set of (global and local) role names occurring in T including their inverses, AG is the conjunction of all concept assertions in AG, and the unary predicates Eq R(x), Eq R (x), for R 2 NR, capture domain and range of role R, respectively, with q encoding the number of R-successors of a given individual. We abstract individuals according to their types. For each individual a 2 AyG, its type (a) = f#nP j #nP (a) 2 AyGg. With each type, , we associate a fresh new individual, v , the representative of all the individuals in AyG with type , and denote with y the set of all such representatives. Thus, by using
AG
(Sample) # Concept # Role
QT L1(N) ABox
Abs.
ABox ABox Abs. Abs. size Ind. ABox
just one representative for each type, we abstraction BG of AyG: nally generate the (equisatis able) BG = [
B ; with B = f#nP (v ) j = (a); #nP 2 g Experiments on Rva2ndAoGmly Generated ABoxes. To evaluate the gain in size of y the ABox after the abstraction, we randomly generate temporal ABoxes from a space of I individual names, N concept names, N global and N local role names, while the time point n is chosen within the time interval [0; T 1] in accordance with the uniform distribution over the space of N T I (1 + 2I) possible assertions. Table 1 reports abstraction results on sampled ABoxes with size varying from 70% up to 90% over the whole ABox space.
We observe a gain of more than 95% in the number of QT L1(N) ABoxes
assertions compared to the original TDL-Lite(N) ABoxes. This is due to the
translation of roles into pairs of unary predicates, together with the shifting of
global role assertions to the initial time point. Moreover, there is a clear gain
in the number of individuals, specially when the ABox size is close to the ABox
space, con rming experimental results obtained for non-temporal DLs [
LTL
BLACK
number Lt of GCIs in a TBox; and a xed value Lc of the length of concept. The
guessed TBox for Table 2 has the following parameters: N = 50, Lc = 5, Q = 3,
while the value of Lt is set close to 3 N so that all concept and role names are
considered in guessing the TBox (when Lc = 5 three names are at most chosen
from a space of 3 N and we have at most 2 3 = 6 names considering both
the right and left hand sides of each GCI). The resulting KB is translated into
LTL resulting in a formula with 110 150 propositional variables (this number
depends only on the size of the TBox and on the number of individuals). Table 2
reports reasoning results on such abstracted KBs using the tableaux based LTL
solver BLACK [
Conclusions. We proposed an approach for abstracting temporal ABoxes which
shows good results when increasing the number of ABox assertions in randomly
generated KB to values close to the ones observed in realistic (static) ontologies,
being able to process temporal KBs with millions of assertions. We con rmed the
results of this approach by comparing the runtimes of reasoning with ABoxes
vs abstracted ABoxes by showing signi cant savings. As a future work, one
can consider the feasibility of pairing the abstraction technique with parallelised
reasoning algorithms, splitting the parallel processes according to the abstracted
individuals, in the lines of what has already been experimented in [