Deciding expressive description logics in the framework of resolution.
We present a decision procedure for the description logic SHIQ based on the basic superposition calculus, and show that it runs in exponential time for unary coding of numbers. To derive our algorithm, we extend basic superposition with a decomposition inference rule, which transforms conclusions of...
| Main Authors: | , , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
Elsevier
2008
|