| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 406586 | Neurocomputing | 2014 | 15 Pages |
Abstract
We give the first ExpTime (complexity-optimal) tableau decision procedure for checking satisfiability of a knowledge base in the description logic SHIOSHIO, which extends the basic description logic ALCALC with transitive roles, hierarchies of roles, inverse roles and nominals. Our procedure exploits global state caching and does not use blind (analytic) cuts.
Related Topics
Physical Sciences and Engineering
Computer Science
Artificial Intelligence
Authors
Linh Anh Nguyen,