Optimising Tableaux Decision Procedures For Description Logics
Optimising Tableaux Decision Procedures For Description Logics
复制标题
优化描述逻辑的 Tableaux 决策过程
DOI：
--
复制
发表时间：
1997
期刊：
影响因子：
--
通讯作者：
Ian Horrocks
中科院分区：
文献类型：
--
作者：
Ian Horrocks
描述逻辑是一种与语义网络密切相关的形式形式，但其显著的特点是概念描述语言的语义是形式化的，从而可以通过合适的算法计算两个概念描述之间的包含关系。描述逻辑已被证明在一系列应用中是有用的，但它们的广泛接受受到其有限的表达能力和其包含算法的棘手性的阻碍。本文探讨了用表达性概念描述语言为描述逻辑提供健全、完整和经验上可处理的包容推理的可行性。这表明，虽然已知在最坏的情况下，这些语言中的包容推理是难以处理的，但适当优化的算法可以在现实知识库中提供可接受的性能。这种说法得到了FaCT系统的实现和测试的支持。FaCT是用于表达性概念描述语言的描述逻辑类，它包括对传递角色和角色层次的支持。提出了一种表演算式的包含推理算法，并证明了该算法的正确性和完备性。本文还描述了FaCT所采用的各种新颖和适应性优化技术，并通过使用大型现实知识库（来自Galen项目）和随机生成的满意度问题进行广泛的实证测试来评估其有效性。这些测试表明，优化技术将FaCT的性能提高了至少三个数量级，因此，当与Galen知识库一起使用时，FaCT提供了可接受的性能。本文中提出的工作对描述逻辑的用户和描述逻辑系统的实现者都有价值，他们将能够在他们的算法中合并部分或全部优化技术。优化技术也可能对更广泛的自动推理和人工智能研究人员感兴趣。本论文中提及的任何部分工作都没有被提交用于支持本大学或任何其他大学或其他学习机构的另一个学位或资格的申请。(1)本论文文本的版权归作者所有。副本（以任何方式），无论是全文还是摘录，都只能按照作者的指示制作，并提交给曼彻斯特约翰·莱兰兹大学图书馆。详情可向图书馆馆长索取。本页必须成为任何副本的一部分。未经作者（书面）许可，不得按照上述指示（以任何方式）制作副本的进一步副本。(2)本论文中可能描述的任何知识产权的所有权归曼彻斯特大学所有，但须遵守任何事先相反的协议，未经大学书面许可，第三方不得使用，该大学将规定任何此类协议的条款和条件。关于披露和利用可能发生的条件的进一步信息，可以从计算机科学系的负责人处获得。我感谢我的导师，无论是过去的还是现在的，Alan Rector, Graham Gough， Richard Banach和Carole Goble的帮助和支持。没有他们的帮助，本论文的工作是不可能完成的。还要感谢医学信息学和人工智能小组的成员，特别是Sean Bechhofer， Ian Pratt和Dominik schop。最后，我要感谢广大Description Logic社区的所有成员，他们提供了启发、建议和鼓励。作者Ian Horrocks于1981年获得曼彻斯特大学计算机科学学士学位。毕业后，他在计算机科学系担任研究助理，先是在巴克莱微处理器实验室，后来在数据流并行架构组工作。1983年，他加入Scientex Limited担任技术总监，负责开发一系列文字处理和桌面出版产品。1994年，他回到曼彻斯特大学，成为医学信息学组的一名研究生。1995年以论文《两种术语知识表示系统的比较》获得硕士学位。他的研究兴趣是知识表示，自动推理，特别是描述逻辑。他有许多出版物值得称赞，并且是1997年描述逻辑国际研讨会组织委员会的成员
Description Logics form a family of formalisms closely related to semantic networks but with the distinguishing characteristic that the semantics of the concept description language is formally de ned, so that the subsumption relationship between two concept descriptions can be computed by a suitable algorithm. Description Logics have proved useful in a range of applications but their wider acceptance has been hindered by their limited expressiveness and the intractability of their subsumption algorithms. This thesis investigates the practicability of providing sound, complete and empirically tractable subsumption reasoning for a Description Logic with an expressive concept description language. It suggests that, while subsumption reasoning in such languages is known to be intractable in the worst case, a suitably optimised algorithm can provide acceptable performance with a realistic knowledge base. This claim is supported by the implementation and testing of the FaCT system. FaCT is a Description Logic classi er for an expressive concept description language which includes support for both transitive roles and a role hierarchy. A tableaux calculus style algorithm for subsumption reasoning in this language is presented along with a proof of its soundness and completeness. The wide range of novel and adapted optimisation techniques employed by FaCT is also described and their e ectiveness is evaluated by extensive empirical testing using both a large realistic knowledge base (from the Galen project) and randomly generated satis ability problems. These tests demonstrate that the optimisation techniques improve FaCT's performance by at least three orders of magnitude, and that as a result, FaCT provides acceptable performance when used with the Galen knowledge base. The work presented in this thesis should be of value to both users of Description Logics, to whom the FaCT system has been made available, and to implementors of Description Logic systems, who will be able to incorporate some or all of the optimisation techniques in their algorithms. The optimisation techniques may also be of interest to a wider audience of Automated Deduction and Arti cial Intelligence researchers. 12 Declaration No portion of the work referred to in this thesis has been submitted in support of an application for another degree or quali cation of this or any other university or other institution of learning. (1) Copyright in the text of this thesis rests with the Author. Copies (by any process) either in full, or of extracts, may be made only in accordance with instructions given by the Author and lodged in the John Rylands University Library of Manchester. Details may be obtained from the Librarian. This page must form part of any such copies made. Further copies (by any process) of copies made in accordance with such instructions may not be made without the permission (in writing) of the Author. (2) The ownership of any intellectual property rights which may be described in this thesis is vested in the University of Manchester, subject to any prior agreement to the contrary, and may not be made available for use by third parties without the written permission of the University, which will prescribe the terms and conditions of any such agreement. Further information on the conditions under which disclosures and exploitation may take place is available from the Head of the Department of Computer Science. 13 Acknowledgements I gratefully acknowledge the help and support of my advisors, both past and present, Alan Rector, Graham Gough, Richard Banach and Carole Goble. Without their assistance the work embodied in this thesis would not have been possible. Thanks are also due to the members of the Medical Informatics and Arti cial Intelligence groups, in particular Sean Bechhofer, Ian Pratt and Dominik Schoop. Finally, I would like to thank all the members of the wider Description Logic community who have provided inspiration, advice and encouragement. This work was supported by a grant from the Engineering and Physical Sciences Research Council. 14 The Author Ian Horrocks obtained a B.Sc. in Computer Science from Manchester University in 1981. After graduation he worked as a Research Assistant in the Computer Science Department, rst in the Barclays microprocessor laboratory and later with the data ow parallel architecture group. In 1983 he joined Scientex Limited as Technical Director and was responsible for the development of a range of word processing and desk-top publishing products. In 1994 he returned to Manchester University as a research student in the Medical Informatics Group. He obtained an M.Sc. in 1995 with a thesis entitled A Comparison of Two Terminological Knowledge Representation Systems. His research interests are knowledge representation, automated reasoning and, in particular, description logics. He has a number of publications to his credit and is a member of the organising committee for the 1997 International Workshop on Description Logics. 15 Chapter