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 interval-based 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.