Verication of medical guidelines using task execution with background knowledge

Abstract. The use of a medical guideline can be seen as the exe-cution of computational tasks, sequentially or in parallel, in the face of patient data. It has been shown that many of such guidelines can be represented as a `network of tasks', i.e., as a number of steps that have a specic function or goal. To investigate the quality of such guidelines we propose a formalization of criteria for good practice medicine a guideline should comply to. We use this theory in con-junction with medical background knowledge to verify the quality of a guideline dealing with diabetes mellitus type 2 using the in-teractive theorem prover KIV. Verication using task execution and background knowledge is a novel approach to quality checking of medical guidelines.