document.178

The DL ALCFI is chosen not simply because it was extensively studied in the past, but because this logic is the juncture point of several interesting research results established in the past as well.
For example, it is the logic where the finite model property is lost and the dynamic pair-wise blocking technique was proposed for; it is the logic where functional restrictions
can be eliminated; and it is also the logic where the complexity of its satisfiability problem goes up to NExpTime-hard when nominals are added. Each of the above mentioned results is an advancement and has impact on either practical or
theoretical research.
The encoding method for eliminating functional restrictions from an ALCFI knowledge base was presented14 in [Gia96, CGR98, GM00]. Our approach shares similarity with their work in introducing new concept names and encoding new constraints in the form of general concept inclusions. The difference is that we keep functional restrictions untouched but eliminate the effect of backward propagation of constraints on a tableaux structure.
[Tob00, Lut04] proved that the DL ALCFIO is NExpTime-hard. The conversion would be incorrect if there is a nominal. This limitation coincides with the as pointed out in the improved hardness proof in [Lut04]. If there are only nominals and inverse roles but no functional restrictions, the presented conversion is
satisfiability-preserving15. 
For DLs supporting inverse roles, the termination mechanism (a.k.a. cycle detection and blocking techniques) for tableau-based decision procedures is required to be dynamic to accommodate backward propagation of constraints [HS99]. To further support number restrictions, the more sophisticated dynamic pair-wise blocking technique [HS99] and its optimized variants [HS02] were introduced to guarantee soundness. A
study of the model properties of DLs with inverse roles shows that various dynamic termination mechanisms are sufficient. Generally speaking, the bidirectional traversal on a relational structure is a natural consequence of enforcing tableau expansion rules over inverse relations. However, there are some undesirable side effects from bidirectional propagation of constraints, e.g., one major problem is the unsoundness of the 14In one of those works, the connection between an in ALCFI and its corresponding
in ALCF was briefly pointed out. There exist further extensions for number restrictions, interested readers are referred to [CGLN01].
15Recently in [Lut07], it was proved that the conjunctive query entailment problem is NexpTimehard in ALCI but remains ExpTime-complete in SHQ.
74
tableau caching technique [BCM+03], and the second problem is the save and restore problem (as mentioned before in Section 4.1.1 and Section 4.1.2), the third problem is the lack of efficient propagation of unsatisfiability, and the final problem is that
the size of the tableaux structure could become unnecessarily large. Further, though the book-keeping cost for a sequence of establishing, breaking and re-establishing of blockings is minor for small knowledge bases, the cost could be amplified for larger
knowledge bases, and it also entails complicated design and implementation issues.
This chapter presented a way to adapt a static termination mechanism to tableaubased decision procedures for the concept satisfiability test w.r.t. general axioms in ALCFI. The static termination mechanism is intuitively simple and easily implementable. The major run-time performance advantage for static blocking and one-way traversal is that it requires a small footprint algorithm, thus it is well suited to resource
limited computer systems16. The independence of sibling nodes of a tableaux structure also implies implementations that explore the multi-threading mechanism and multi-core computer systems more efficiently.
In the beginning of this chapter, a transformation is introduced to convert a source problem to a target problem and to preserve equisatisfiability in ALCFI. The search of a model in the converted problem can safely use the static equality termination
mechanism (a.k.a. the equality blocking technique [BCM+03]) globally. Based on the static blocking mechanism and (a very weak form of) the inconsistency propagation capability, one is then able to show that the decision procedure runs in exponential
time in the worst case for the concept satisfiability problem in ALCFI. 
16The virtual memory might be huge but is often much slower than physical memory, and frequent page swapping can cause low-level performance thrashing. Small footprint algorithms can be
significantly faster than memory intensive algorithms.
75 
The decision procedure relies on two functionalities: the static equality blocking which is globally applicable but transient, and the unsatisfiability caching which is globally applicable and persistent. [DM00] is credited for this idea. As shown in [GN07], the data structure Witness here can possibly be persistent as well under certain conditions.
We demonstrated a decision procedure using the restart strategy. Whenever one new unsatisfiable set (of labels) is obtained and it is not the given problem itself, the decision procedure restarts. In other cases, the procedure terminates and is able to decide the satisfiability of the problem. Though the use of the restart strategy here is for an easy analysis of the complexity, it is also of potential advantage to the runtime performance for realistic problems. For example, it is possible to assert artificial elements in Nogood (as a penalty) to bypass the searching of certain branches which were timed out before. Possibly this might help in practice because the reasoning
system can somehow choose to explore branches first.
An ExpTime decision procedure for a DL with both inverse roles and functional restrictions would not be ready but for a polynomial-time conversion. This is because the decision procedure is correct only for problems with a special property (which is called t-careanywhere dynamic pairwise were carried out. It is observed that, as expected, fresh concept names and new general concept inclusions have a modest size expansion by a factor of 5, and a runtime performance penalty of a factor of around 3 to 4. But for a set of hard problems, this penalty is well offset by the global tableaux caching functionality, and magnitudes of performance gain have been achieved for half of the test cases. As already discussed in the background section (at the end of Section 4.1.2), the tableaux caching technique
can serve not only as a static blocking technique, it can also prune away of the search space. By contrast with running problems in DLs with inverse roles, running the converted problems in DLs without inverse roles likely demands less memory (for there is no need to make an extra copy of the tableaux structure before
branching so that an undoing will be possible). It is quite promising that the global (sub)tableaux caching technique can be used in tableau-based DL systems to try some realistic problems yet unsolved because of inverse roles. 
In Chapter 6, we will deal with SHIQ and present a more general, but less powerful18, global tableaux caching technique.