|
Abstract : |
The tableau algorithm implemented in the FaCT knowledge representation system decides satisability and subsumption in SHIQ, a very expressive description logic providing, e.g., inverse and transitive roles, number restrictions, and general axioms. Intuitively, the algorithm searches for a tree-shaped abstraction of a model. To ensure termination of this algorithm without compromising correctness, it stops expanding paths in the search tree using a so-called \double-blocking " condition. This condition was clearly more exacting than was strictly necessary, but it was assumed that more precisely dened blocking conditions would, on the one hand, make the proof of the algorithm's correctness far more dicult and, on the other hand (and more importantly), be so costly to check as to outweigh any benet that might be derived. However, FaCT's failure to solve UML derived knowledge bases led us to reconsider this conjecture and to formulate more precisely de-, |
