satisfiability checking of clinical practice guidelines using an analyzer

A clinical practice guideline consists of the best practices required for managing a particular disease. designing a consistent guideline is difficult and error-prone; hence, checking the consistency of guidelines is crucial. due to the complexity of guidelines, a formal language is an appropriate choice for modeling and analyzing a guideline. impnl has been introduced as a metric intervalbased temporal logic to model such guidelines. moreover, a sound and complete tableau-based algorithm has been designed for checking the satisfiability of an impnl formula. in this paper,we introduced a clinical practice guideline analyzer suitable for modeling and checking the consistency of a guideline. the analyzer can also determine points, in which inconsistencies occur, and help designers to quickly and easily fix a guideline. moreover, physicians can use the output of the analyzer (the calendar model) to check whether a patient is coherently treated with a specific guideline.