Optimised ExpTime Tableaux for ?ℋℐ? over Finite Residuated Lattices
Joint Authors
Gong, Jianxing
Huang, Jian
Zhao, Xinye
Source
Journal of Applied Mathematics
Issue
Vol. 2014, Issue 2014 (31 Dec. 2014), pp.1-15, 15 p.
Publisher
Hindawi Publishing Corporation
Publication Date
2014-04-07
Country of Publication
Egypt
No. of Pages
15
Main Subjects
Abstract EN
This study proposes to adopt a novel tableau reasoning algorithm for the description logic ?ℋℐ? with semantics based on a finite residuated De Morgan lattice.
The syntax, semantics, and logical properties of this logic are given, and a sound, complete, and terminating tableaux algorithm for deciding fuzzy ABox consistency and concept satisfiability problem with respect to TBox is presented.
Moreover, based on extended and/or completion-forest with a series of sound optimization technique for checking satisfiability with respect to a TBox in the logic, a new optimized ExpTime (complexity-optimal) tableau decision procedure is presented here.
The experimental evaluation indicates that the optimization techniques we considered result in improved efficiency significantly.
American Psychological Association (APA)
Huang, Jian& Zhao, Xinye& Gong, Jianxing. 2014. Optimised ExpTime Tableaux for ?ℋℐ? over Finite Residuated Lattices. Journal of Applied Mathematics،Vol. 2014, no. 2014, pp.1-15.
https://search.emarefa.net/detail/BIM-491715
Modern Language Association (MLA)
Huang, Jian…[et al.]. Optimised ExpTime Tableaux for ?ℋℐ? over Finite Residuated Lattices. Journal of Applied Mathematics No. 2014 (2014), pp.1-15.
https://search.emarefa.net/detail/BIM-491715
American Medical Association (AMA)
Huang, Jian& Zhao, Xinye& Gong, Jianxing. Optimised ExpTime Tableaux for ?ℋℐ? over Finite Residuated Lattices. Journal of Applied Mathematics. 2014. Vol. 2014, no. 2014, pp.1-15.
https://search.emarefa.net/detail/BIM-491715
Data Type
Journal Articles
Language
English
Notes
Includes bibliographical references
Record ID
BIM-491715