[1] Gu Huamao, , Shi Jinqin, et al. Clause-based enhancing mode for tableau algorithm for ALCN [J]. Journal of Southeast University (English Edition), 2008, 24 (3): 361-364. [doi:10.3969/j.issn.1003-7985.2008.03.027]

Copy

Clause-based enhancing mode for tableau algorithm for ALCN()

Share：

Journal of Southeast University (English Edition)[ISSN:1003-7985/CN:32-1325/N]

Volumn:

24

Issue:

2008 3

Page:

361-364

Research Field:

Computer Science and Engineering

Publishing date:

2008-09-30

Info

Title:

Clause-based enhancing mode for tableau algorithm for ALCN

Author(s):

Gu Huamao¹;  2;  3;  Shi Jinqin³;  Gao Ji¹

¹ Institute of Artificial Intelligence, Zhejiang University, Hangzhou 310027, China
² School of Computer and Information Engineering, Zhejiang Gongshang University, Hangzhou 310018, China
³ Food Sensory Science Laboratory, Zhejiang Gongshang University, Hangzhou 310018, China

Keywords:

tableau algorithm;  enhancing mode;  clause;  satisfiability

PACS:

TP301

DOI:

10.3969/j.issn.1003-7985.2008.03.027

Abstract:

As the tableau algorithm would produce a lot of description overlaps when judging the satisfiabilities of concepts(thus wasting much space), a clause-based enhancing mode designed for the language ALCN is proposed.This enhancing mode constructs a disjunctive normal form on concept expressions and keeps only one conjunctive clause, and then substitutes the obtained succinctest conjunctive clause for sub-concepts set in the labeling of nodes of a completion tree constructed by the tableau algorithm(such a process may be repeated as many times as needed).Due to the avoidance of tremendous descriptions redundancies caused by applying ∩- and ∪-rules of the ordinary tableau algorithm, this mode greatly improves the spatial performance as a result.An example is given to demonstrate the application of this enhancing mode and its reduction in the cost of space. Results show that the improvement is very outstanding.

References:

[1] Baader F, Calvanese D, McGuinness D, et al.The description logic handbook:theory, implementation, and applications[M].Cambridge:Cambridge University Press, 2003.
[2] Baader F, Sattler U.An overview of tableau algorithms for description logics[J].Studia Logica, 2001, 69(1):5-40.
[3] Horrocks I, Cough G.Description logics with transitive roles[C]//Proceedings of the International Workshop on Description Logics. Paris, France, 1997:25-28.
[4] Horrocks I, Sattler U.Ontology reasoning in the SHOQ(D)description logic[C]//Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence. Seattle, Washington, USA, 2001:199-204.
[5] Horrocks I, Sattler U.A tableau decision procedure for SHOIQ[J].Journal of Automated Reasoning, 2007, 39(3):249-276.
[6] Dong M K, Jiang Y C, Shi Z Z.A description logic with default reasoning[J].Chinese Journal of Computers, 2003, 26(6):729-736.(in Chinese)
[7] Kang Dazhou, Xu Baowen, Lu Jianjiang, et al.Description logics for fuzzy ontologies on semantic web[J].Journal of Southeast University:English Edition, 2006, 22(3):343-347.
[8] Stoilos G, Stamou G, Pan J Z, et al.Reasoning with very expressive fuzzy description logics[J].Journal of Artificial Intelligence Research, 2007, 30(8):273-320.
[9] Straccia U.Reasoning within fuzzy description logics[J].Journal of Artificial Intelligence Research, 2001, 14(1):137-166.
[10] Schmidt-Schau M, Smolka G.Attributive concept descriptions with complements[J].Artificial Intelligence, 1991, 48(1):1-26.

Memo

Memo:

Biographies: Gu Huamao(1975—), male, graduate;Gao Ji(corresponding author), male, professor, gaoji@mail.hz.zj.cn.
Foundation items: The National Natural Science Foundation of China(No.60775029), the Science and Technology Program of Zhejiang Province(No.2007C33072).
Citation: Gu Huamao, Shi Jinqin, Gao Ji.Clause-based enhancing mode for tableau algorithm for ALCN[J].Journal of Southeast University(English Edition), 2008, 24(3):361-364.

Common functions