Optimised ExpTime Tableaux for 𝒮ℋℐ𝒩 over Finite Residuated Lattices

• Main Authors: Jian Huang, Xinye Zhao, Jianxing Gong
• Format: Article
• Language: English
• Published: Hindawi Limited 2014-01-01
• Series: Journal of Applied Mathematics
• Online Access: http://dx.doi.org/10.1155/2014/702326

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.