Formal methods have been used in the past for the verification of the correctness of formalised versions of medical guidelines. In this paper a second possible application of the use of formal methods is proposed: checking whether a guideline conforms to global medical quality requirements. It is argued that this allows spotting design errors in medical guidelines, which is seen as a useful application for formal methods in medicine. However, this type of verification may require medical knowledge currently not available within the guidelines, i.e. medical background knowledge. In this paper, we propose a method for checking the quality of a treatment for a disorder, based on the theory of abductive diagnosis. We also examine the medical background knowledge required to be able to quality check a guideline. The method is illustrated by the formal analysis of an actual guideline for the management of diabetes mellitus type 2.


Diabetes Mellitus Type Diabetes Type Formal Method Temporal Logic Quality Check 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Console L, Theseider Dupré D, and Torasso P. On the relationship between abduction and deduction, Journal of Logic and Computation 1991; 1(5): 661–690.MathSciNetMATHCrossRefGoogle Scholar
  2. [2]
    Forbus KD. Qualitative process theory. Artificial Intelligence 1984; 24: 85–168.CrossRefGoogle Scholar
  3. [3]
    Fox J, Johns N, Lyons C, Rahmanzadeh A, Thomson R, and Wilson P. PROforma: a general technology for clinical decision support systems. Computer Methods and Programs in Biomedicine 1997; 54: 59–67.CrossRefGoogle Scholar
  4. [4]
    Fox J, and Das S. Safe and Sound: Artificial Intelligence in Hazardous Applications. Cambridge: MIT Press (jointly published with the American Association of Artificial Intelligence), 2000.Google Scholar
  5. [5]
    Kuipers BJ. Qualitative simulation. Artificial Intelligence 1986; 29: 289–388.MathSciNetMATHCrossRefGoogle Scholar
  6. [6]
    Kuipers BJ. Qualitative Reasoning. The MIT Press, Cambridge, Massachusetts, 1994.Google Scholar
  7. [7]
    Lucas PJF. Logic engineering in medicine. The Knowledge Engineering Review 1995; 10(2): 153–179.CrossRefGoogle Scholar
  8. [8]
    Lucas PJF. Symbolic diagnosis and its formalisation. The Knowledge Engineering Review 1997; 12(2): 109–146.MathSciNetCrossRefGoogle Scholar
  9. [9]
    Lucas PJF. Analysis of notions of diagnosis. Artificial Intelligence 1998; 105(1-2): 293–341.MathSciNetCrossRefGoogle Scholar
  10. [10]
    Marcos M, Balser M, Ten Teije A, and Van Harmelen F. From informal knowledge to formal logic: a realistic case study in medical protocols. Proceedings of the 12th EKAW-2002, 2002.Google Scholar
  11. [11]
    Ohno-Machado L, Gennari J, Murphy S, et al. Guideline Interchange Format: a model for representing guidelines. Journal of the American Medical Informatics Association 1998; 5(4): 357–372.CrossRefGoogle Scholar
  12. [12]
    Poole D. A methodology for using a default and abductive reasoning system. International Journal of Intelligent Systems 1990, 5(5), 521–548.MathSciNetMATHCrossRefGoogle Scholar
  13. [13]
    Reif W. The KIV Approach to Software Verification. In: M. Broy and S. Jähnichen (eds.), KORSO: Methods, Languages, and Tools for the Construction of Correct Software. Lecture Notes in Computer Science, Volume 1009, Springer–Verlag, Berlin, 1995.Google Scholar
  14. [14]
    Sackett DL, Richardson WS, Rosenberg W, and Brian R. Evidence Based Medicine-How to Practice and Teach EBM. Haynes Churchill Livingstone, 1996.Google Scholar
  15. [15]
    Shahar Y, Miksch S, and Johnson P. The Asgaard project: a task-specific framework for the application and critiquing of time-oriented clinical guidelines. Artificial Intelligence in Medicine 1998; 14: 29–51.CrossRefGoogle Scholar
  16. [16]
    Turner R. Logics for Artificial Intelligence. Ellis Horwood, Chichester, 1985.Google Scholar
  17. [17]
    Woolf SH. Evidence-based medicine and practice guidelines: an overview. Cancer Control 2000; 7(4): 362–367.Google Scholar

Copyright information

© Springer-Verlag London 2004

Authors and Affiliations

  • Peter Lucas
    • 1
  1. 1.Institute for Computing and Information SciencesUniversity of NijmegenNijmegenThe Netherlands

Personalised recommendations