Since a Clinical Practice Guideline describes the diagnosis and treatment process of a disease, designers of such guidelines should ensure their logical consistency. A formal approach for modeling them provides a basis for some useful reasoning (e.g., satisfiability checking). In this paper, we describe a metric interval-based temporal description logic, which is suitable for modeling the dynamic aspect of a domain and the the medical ontologies. We also propose a tableau-based algorithm for checking the satisfiability of such guidelines, to assure their logical consistency. We explain the process of encoding a real- life guideline, the “Treatment of Tuberculosis”, and present a situation where designers can use our logic and associated satisfiability algorithm to detect an inconsistency in the guideline for patients with Cirrhosis disease
