Automated Reasoning in Temporal DL-Lite
This work addresses a domain-specific problem for researchers in knowledge representation and temporal logic, but it is incremental as it applies existing methods to a new data context.
This paper tackles the problem of automated reasoning over temporal DL-Lite knowledge bases by testing off-the-shelf LTL reasoners for satisfiability, resulting in experiments that measure running time and translation sizes to assess robustness and scalability.
This paper investigates the feasibility of automated reasoning over temporal DL-Lite (TDL-Lite) knowledge bases (KBs). We test the usage of off-the-shelf LTL reasoners to check satisfiability of TDL-Lite KBs. In particular, we test the robustness and the scalability of reasoners when dealing with TDL-Lite TBoxes paired with a temporal ABox. We conduct various experiments to analyse the performance of different reasoners by randomly generating TDL-Lite KBs and then measuring the running time and the size of the translations. Furthermore, in an effort to make the usage of TDL-Lite KBs a reality, we present a fully fledged tool with a graphical interface to design them. Our interface is based on conceptual modelling principles and it is integrated with our translation tool and a temporal reasoner.