  Requirements about the quality of clinical guidelines can be represented by
schemata borrowed from the theory of abductive diagnosis, using temporal logic
to model the time-oriented aspects expressed in a guideline. Previously, we
have shown that these requirements can be verified using interactive theorem
proving techniques. In this paper, we investigate how this approach can be
mapped to the facilities of a resolution-based theorem prover, Otter, and a
complementary program that searches for finite models of first-order
statements, Mace. It is shown that the reasoning required for checking the
quality of a guideline can be mapped to such fully automated theorem-proving
facilities. The medical quality of an actual guideline concerning diabetes
mellitus 2 is investigated in this way.
