{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,6]],"date-time":"2024-08-06T02:41:37Z","timestamp":1722912097373},"reference-count":61,"publisher":"Cambridge University Press (CUP)","issue":"5-6","license":[{"start":{"date-parts":[[2008,11,1]],"date-time":"2008-11-01T00:00:00Z","timestamp":1225497600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2008,11]]},"abstract":"Abstract<\/jats:title>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<\/jats:sc>and a complementary program that searches for finite models of first-order statements,mace<\/jats:sc>-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.<\/jats:p>","DOI":"10.1017\/s1471068408003451","type":"journal-article","created":{"date-parts":[[2008,11,20]],"date-time":"2008-11-20T04:35:46Z","timestamp":1227155746000},"page":"611-641","source":"Crossref","is-referenced-by-count":11,"title":["Checking the quality of clinical guidelines using automated reasoning tools"],"prefix":"10.1017","volume":"8","author":[{"given":"ARJEN","family":"HOMMERSOM","sequence":"first","affiliation":[]},{"given":"PETER J. F.","family":"LUCAS","sequence":"additional","affiliation":[]},{"given":"PATRICK","family":"VAN BOMMEL","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2008,11,1]]},"reference":[{"key":"S1471068408003451_ref1","doi-asserted-by":"publisher","DOI":"10.1145\/182.358434"},{"key":"S1471068408003451_ref10","doi-asserted-by":"publisher","DOI":"10.1080\/01449298808901868"},{"key":"S1471068408003451_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/BF00881715"},{"key":"S1471068408003451_ref50","doi-asserted-by":"publisher","DOI":"10.1177\/0272989X9401400306"},{"key":"S1471068408003451_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/s10994-006-5833-1"},{"key":"S1471068408003451_ref7","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"S1471068408003451_ref5","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/1.5.661"},{"key":"S1471068408003451_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-3384-5_11"},{"key":"S1471068408003451_ref19","first-page":"138","volume-title":"Proc. of the Work-in-Progress Track at the 10th International Conference on Inductive Logic Programming","author":"Kersting","year":"2000"},{"key":"S1471068408003451_ref6","doi-asserted-by":"publisher","DOI":"10.1111\/j.1467-8640.1991.tb00388.x"},{"key":"S1471068408003451_ref20","first-page":"263","volume-title":"Computational Algebra","author":"Knuth","year":"1970"},{"key":"S1471068408003451_ref61","doi-asserted-by":"publisher","DOI":"10.1145\/321296.321302"},{"key":"S1471068408003451_ref11","volume-title":"Safe and Sound: Artificial Intelligence in Hazardous Applications","author":"Fox","year":"2000"},{"key":"S1471068408003451_ref47","doi-asserted-by":"publisher","DOI":"10.1111\/0824-7935.00114"},{"key":"S1471068408003451_ref16","volume-title":"Textbook of Medical Physiology","author":"Guyton","year":"2000"},{"key":"S1471068408003451_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"S1471068408003451_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/S0933-3657(02)00011-8"},{"key":"S1471068408003451_ref23","doi-asserted-by":"publisher","DOI":"10.1016\/0933-3657(93)90033-Y"},{"key":"S1471068408003451_ref3","first-page":"219","volume-title":"Proc. of 13th International SPIN Workshop on Model Checking of Software","author":"B\u00e4umler","year":"2006"},{"key":"S1471068408003451_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-51803-7_36"},{"key":"S1471068408003451_ref58","volume-title":"Handbook of Medical Informatics","author":"van Bemmel","year":"2002"},{"key":"S1471068408003451_ref59","doi-asserted-by":"publisher","DOI":"10.1177\/107327480000700411"},{"key":"S1471068408003451_ref56","unstructured":"Terenziani P. , Montani S. , Torchio M. , Molino G. and Anselma L. 2003. Temporal consistency checking in clinical guidelines acquisition and execution. In Proc. of AMIA Annual Symposium. Washington, DC, USA, 659\u2013663."},{"key":"S1471068408003451_ref36","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0012852"},{"key":"S1471068408003451_ref14","volume-title":"Review of Medical Physiology","author":"Ganong","year":"2005"},{"key":"S1471068408003451_ref15","first-page":"411","volume-title":"Proc. of AIME-2007","author":"Groot","year":"2007"},{"key":"S1471068408003451_ref25","doi-asserted-by":"publisher","DOI":"10.1017\/S0269888997002026"},{"key":"S1471068408003451_ref17","doi-asserted-by":"publisher","DOI":"10.1109\/TKDE.2007.190611"},{"key":"S1471068408003451_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/S0169-2607(98)00025-X"},{"key":"S1471068408003451_ref24","doi-asserted-by":"publisher","DOI":"10.1017\/S0269888900008134"},{"key":"S1471068408003451_ref37","unstructured":"Patil R. 1981. Causal representation of patient illness for ELECTROLYTE and ACID-BASE diagnosis. Tech. Rep. MIT\/LCS\/TR-267, MIT."},{"key":"S1471068408003451_ref26","first-page":"309","volume-title":"Proc. of AI-2003 (Research and Developments in Intelligent Systems XX)","author":"Lucas","year":"2003"},{"key":"S1471068408003451_ref40","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2005.02.003"},{"key":"S1471068408003451_ref27","volume-title":"Principles of Intelligent Systems","author":"Lucas","year":"1991"},{"key":"S1471068408003451_ref28","doi-asserted-by":"publisher","DOI":"10.1114\/1.1289459"},{"key":"S1471068408003451_ref31","doi-asserted-by":"crossref","unstructured":"McCune W. June, 2001. MACE 2.0 Reference Manual and Guide. Tech. Memo ANL\/MCS-TM-249, Argonne National Laboratory, Argonne, IL.","DOI":"10.2172\/797949"},{"key":"S1471068408003451_ref44","first-page":"23","article-title":"Automated deduction with hyperresolution","volume":"1","author":"Robinson","year":"1965","journal-title":"International Journal of Computatational Mathematics"},{"key":"S1471068408003451_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/S0933-3657(00)00103-2"},{"key":"S1471068408003451_ref29","volume-title":"Proc. of the 12th EKAW-2002","author":"Marcos","year":"2002"},{"key":"S1471068408003451_ref30","first-page":"122","article-title":"Temporal logic with past is exponentially more succinct","volume":"79","author":"Markey","year":"2003","journal-title":"EATCS Bulletin"},{"key":"S1471068408003451_ref2","unstructured":"Areces C. , Gennari R. , Heguiabehere J. and De Rijke M. 2000. Tree-based heuristics in modal theorem proving. In Proc. of the ECAI'2000. Berlin, Germany."},{"key":"S1471068408003451_ref32","unstructured":"McCune W. August 2003. Otter 3.3 Reference Manual. Tech. Memo ANL\/MCS-TM-263, Argonne National Laboratory, Argonne, IL."},{"key":"S1471068408003451_ref33","volume-title":"A Critiquing Approach to Expert Computer Advice: ATTENDING","author":"Miller","year":"1984"},{"key":"S1471068408003451_ref34","unstructured":"Moore R. C. 1979. Reasoning about Knowledge and Action. Ph.D. Thesis, MIT."},{"key":"S1471068408003451_ref35","first-page":"10","volume-title":"IEEE Computer","author":"Moszkowski","year":"1985"},{"key":"S1471068408003451_ref38","first-page":"645","volume-title":"Proc. of AMIA Annual Symposium","author":"Peleg","year":"2000"},{"key":"S1471068408003451_ref57","volume-title":"Logics for Artificial Intelligence","author":"Turner","year":"1985"},{"key":"S1471068408003451_ref39","first-page":"79","article-title":"The development of CASC","volume":"15","author":"Pelletier","year":"2002","journal-title":"AI Communications"},{"key":"S1471068408003451_ref41","doi-asserted-by":"publisher","DOI":"10.1002\/int.4550050506"},{"key":"S1471068408003451_ref42","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0015471"},{"key":"S1471068408003451_ref45","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24615-2_3"},{"key":"S1471068408003451_ref12","first-page":"49","article-title":"Decision support for health care: The proforma evidence base","volume":"14","author":"Fox","year":"2006","journal-title":"Informatics in Primary Care"},{"key":"S1471068408003451_ref46","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(96)00025-2"},{"key":"S1471068408003451_ref49","first-page":"19","volume-title":"Deductive Databases and Logic Programming","author":"Shepherdson","year":"1987"},{"key":"S1471068408003451_ref51","doi-asserted-by":"crossref","unstructured":"Shortliffe E. 1974. Mycin: A rule-based computer program for advising physicians regarding antimicrobial therapy selection. Ph.D. Thesis, Stanford University.","DOI":"10.1145\/1408800.1408906"},{"key":"S1471068408003451_ref52","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/4.3.249"},{"key":"S1471068408003451_ref53","doi-asserted-by":"publisher","DOI":"10.1016\/j.artmed.2005.10.006"},{"key":"S1471068408003451_ref54","doi-asserted-by":"publisher","DOI":"10.1111\/0824-7935.00112"},{"key":"S1471068408003451_ref48","doi-asserted-by":"publisher","DOI":"10.1016\/S0933-3657(98)00015-3"},{"key":"S1471068408003451_ref55","doi-asserted-by":"publisher","DOI":"10.1016\/S0933-3657(01)00087-2"},{"key":"S1471068408003451_ref60","volume-title":"Automated Reasoning: Introduction and Applications","author":"Wos","year":"1984"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068408003451","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T11:46:41Z","timestamp":1557920801000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068408003451\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,11]]},"references-count":61,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2008,11]]}},"alternative-id":["S1471068408003451"],"URL":"https:\/\/doi.org\/10.1017\/s1471068408003451","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,11]]}}}