Automated Reasoning in Temporal DL-Lite

<p><strong>Automated Reasoning in Temporal DL-Lite*</strong></p> <p>We investigate the feasibility of automated reasoning over temporal DL-Lite (TDL-Lite) knowledge bases (KBs). We translate TDL-Lite KBs into a fragment of First Order temporal logic and then into LTL, and apply off-the-shelf LTL and FO-based reasoners for checking the satisfiability. We conduct various experiments to analyse the size of the LTL&nbsp;translation as well as the runtime performance of different reasoners on&nbsp;toy scenarios and on randomly generated TDL-Lite KBs. To improve&nbsp;the reasoning performance when dealing with large ABoxes, our work&nbsp;also proposes an approach for abstracting temporal assertions in KBs.&nbsp;We run several experiments with this approach to assess the effectiveness of the technique by measuring the gain in terms of the size of the&nbsp;translation, and the number of both ABox assertions and individuals.&nbsp;We also measure the runtime of the solvers on such abstracted KBs.&nbsp;Lastly, in an effort to make the usage of TDL-Lite KBs a reality, we&nbsp;present a fully-fledged tool with a graphical interface to design and reason over them. Our interface is based on conceptual modeling principles and it is integrated with our translation tool and a temporal reasoner.</p> <p>(*)&nbsp;This work has been submitted to the Journal of Automated Reasoning</p>