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 REALLIFE 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.