A Metric Interval-based Temporal Description Logic

Abstract

Because of the importance of undecidability and the concern with the high complexity of automated reasoning, a few interval-based temporal description logics (ITDLs) have been designed. Moreover, most existing ITDLs are not able to specify the lengths of intervals. In other words, they are not metric. On the other hand, some domains (e.g., medicine) are inherently interval-based, and require a metric logic in order to formalize defined processes and to check process consistency. Hence, a metric interval-based temporal description logic is required. In this thesis, we introduce such a logic (MITDL) along with two algorithms for the satisfiability checking of its formulas. We first introduce an interval-based temporal logic, called IMPNL, inspired by Metric Propositional Neighbourhood Logic. We also present a sound, com- plete and terminating tableau-based algorithm for checking the satisfiability of IMPNL formulas. Afterwards, we combine a restricted version of IMPNL (IMPNL without a negation operator) with the ALC description logic to form a MITDL. We propose two tableau-based algorithms for checking the satisfia- bility of MITDL formulas. We show and prove they are sound, complete and terminate. These algorithms have PSpace and 2NExp-Time complexities. As a proof of concept, we use IMPNL and MITDL to model some clinical practice guidelines (CPG) and check their consistency. We compare MITDL with several languages commonly used for modeling CPGs.