Optimised Exptime tableaux for S H I N over finite residuated lattices

This study proposes to adopt a novel tableau reasoning algorithm for the description logic s h i n 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. © 2014 jian huang et al.