Checking the quality of clinical guidelines using automated reasoning tools

作     者：Hommersom, Arjen Lucas, Peter J. F. Van Bommel, Patrick 

作者机构：Radboud Univ Nijmegen Inst Comp & Informat Sci Sect Model Based Syst Dev NL-6500 GL Nijmegen Netherlands 

出 版 物：《THEORY AND PRACTICE OF LOGIC PROGRAMMING》 (逻辑程序设计理论与实践)

年 卷 期：2008年第8卷第5-6期

页      面：611-641页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 0701[理学-数学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：European Commission's IST [IST-FP6-508794] 

主　　题：automated reasoning clinical guideline temporal logic abduction 

摘      要：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-2. It is shown that the reasoning required for checking the quality of a guideline can be mapped to such a fully automated theorem-proving facilities. The medical quality of an actual guideline concerning diabetes mellitus 2 is investigated in this way.