版权所有:内蒙古大学图书馆 技术提供:维普资讯• 智图
内蒙古自治区呼和浩特市赛罕区大学西街235号 邮编: 010021
作者机构: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.