Asbru in KIV, a tutorial

Guidelines are health care instruments to standardise and improve the quality of medical treatments. Guidelines may contain errors. With the growing importance of guidelines, also the potential impact of errors therein grows. We propose to apply formal methods to those health care instruments to rigourus quality test them and reduce the amount of errors. We translate the guidelines in the formal planing language Asbru, which can be verified with the interactive theorem prover KIV. This paper is meant as a tutorial how to use the different techniques developed during the Protocure project to handle small and large plan hierarchies.