Name
Abstract | ||
|---|---|---|
This study proposes to adopt a novel tableau reasoning algorithm for the description logic SHIN 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. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1155/2014/702326 | JOURNAL OF APPLIED MATHEMATICS |
Field | DocType | Volume |
Discrete mathematics,Lattice (order),EXPTIME,Mathematical analysis,Mathematics | Journal | 2014 |
ISSN | Citations | PageRank |
1110-757X | 0 | 0.34 |
References | Authors | |
18 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| J. Huang | 1 | 44 | 12.63 |
| Xinye Zhao | 2 | 0 | 0.34 |
| Jianxing Gong | 3 | 3 | 1.82 |