An Enhanced Tableau Algorithm Based on Clause Reorganization
GU Hua-Mao1,2, GAO Ji1, WANG Xun2, WU Hai-Yan2
1.Institute of Artificial Intelligence, Zhejiang University, Hangzhou 310027 2.College of Computer Science and Information Engineering, Zhejiang Gongshang University, Hangzhou 310018
Abstract：Taking advantage of the expandability of acyclic concept definitions, an enhanced Tableau algorithm based on clause reorganization is presented. It substitutes the succinctest conjunctive clause of concepts for sub-concepts set in labeling nodes of complete tree/graph. To build a new complete tree/graph, a set of reasoning rules is designed, which avoids tremendous description redundancy caused by ∩-rules and ∪-rules of the traditional Tableau. Thus, the spatial performance of judging the satisfiabilities of acyclic concept definitions is improved greatly. In this papers only reasoning rules and proofs designated for SI language are provided. However, the idea of enhancement mode is suitable for various DL languages as well, which makes it much valuable.
[1] Baader F, Calvanese D, McGuinness D L, et al. The Description Logic Handbook: Theory, Implementation and Applications. Cambridge, UK: Cambridge University Press, 2003 [2] Baader F, Sattler U. An Overview of Tableau Algorithms for Description Logics. Studia Logica, 2001, 69(1): 5-40 [3] Horrocks I, Cough G. Description Logics with Transitive Roles // Proc of the 2nd ACM International Conference on Digital Libraries. Paris, France, 1997: 25-28 [4] Horrocks I, Sattler U. Ontology Reasoning in the SHOQ(D) Description Logic// Proc of the 17th International Joint Conference on Artificial Intelligence. Washington, USA, 2001: 199-204 [5] Horrocks I, Sattler U. A Tableau Decision Procedure for SHOIQ. Journal of Automated Reasoning, 2007, 39(3): 249-276 [6] Horrocks I, Sattler U. A Description Logic with Transitive and Inverse Roles and Role Hierarchies. Journal of Logic and Computation, 1999, 9(3): 385-410 [7] Lutz C, Milicˇic＇ M. A Tableau Algorithm for Description Logics with Concrete Domains and General TBoxes. Journal of Automated Reasoning, 2007, 38(1/2/3): 227-259 [8] Chang Liang, Shi Zhongzhi, Qiu Lirong, et al. A Tableau Decision Algorithm for Dynamic Description Logic. Chinese Journal of Computers, 2008, 31(6): 896-909 (in Chinese) (常 亮,史忠植,邱莉榕,等.动态描述逻辑的Tableau判定算法.计算机学报, 2008, 31(6): 896-909) [9] Straccia U. Reasoning within Fuzzy Description Logics. Journal of Artificial Intelligence Research, 2001, 14(1): 137-166 [10] Stoilos G, Stamou G, Tzouvaras V, et al. The Fuzzy Description Logic f-SHIN // Proc of the International Workshop on Uncertainty Reasoning for the Semantic Web. Galway, Ireland, 2005: 67-76 [11] Jiang Yuncheng, Shi Zhongzhi, Tang Yong, et al. Fuzzy Description Logic for Semantics Representation of the Semantic Web. Journal of Software, 2007, 18(6): 1257-1269 (in Chinese) (蒋运承,史忠植,汤 庸,等.面向语义Web 语义表示的模糊描述逻辑. 软件学报, 2007, 18(6): 1257-1269) [12] Horrocks I, Tobies S, Sattler U. A Pspace-Algorithm for Deciding ALCNIR Satisfiability. Technical Report, LTCS-98-08, Aachen, Germany: RWTH Aachen University, 1998
2009, Vol. 22 
