Meta-level verification of the quality of medical guidelines using interactive theorem proving

Requirements about the quality of medical guidelines can be represented using schemata borrowed from the theory of abductive diagnosis, using temporal logic to model the time-oriented aspects expressed in a guideline. In this paper, we investigate how this approach can be mapped to the facilities offered by a theorem proving system for program verification, KIV. It is shown that the reasoning that is required for checking the quality of a guideline can be mapped to such theoremproving facilities. The medical quality of an actual guideline concerning diabetes mellitus 2 is investigated in this way, and some problems discovered are discussed.