From informal knowledge to formal logic: A realistic case study in medical protocols

We report our experience in a case study with constructing fully formalised knowledge models of realistic, specialised medical knowledge. We have taken a medical protocol in daily use by medical specialists, modelled this knowledge in a specific-purpose knowledge representation language, and finally formalised this knowledge representation in terms of temporal logic and parallel programs. The value of this formalisation process is that each successive formalisation step has contributed to improving the quality of the original medical protocol, and that the final formalisation allows us to provide machine-assisted proofs of properties that are satisfied by the original medical protocol (or, alternatively, precise arguments why the original protocol fails to satisfy certain desirable properties). We believe that this the first time that a significant body of medical knowledge (in our case: a protocol for the management of jaundice in newborns) has been formalised to the extent that it becomes amenable to automated theorem proving, and that this has actually lead to improvement of the original body of medical knowledge.