@INPROCEEDINGS{Hustadt+Motik+Sattler@LPAR2004,
 AUTHOR        = {Hustadt, U. and Motik, B. and Sattler, U.},
 TITLE         = {A Decomposition Rule for Decision Procedures by Resolution-Based Calculi},
 BOOKTITLE     = {Proceedings of the 11th International Conference on 
 Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2004)
 [Montevideo, Uruguay, 14-18 March 2005)},
 EDITOR        = {Baader, F. and Voronkov, A.},
 PUBLISHER     = {Springer},
 CMONTH        = mar # {~14--18},
 CYEAR         = {2005},
 YEAR          = {2005},
 PAGES         = {21-35},
 URL           = {http://dx.doi.org/10.1007/978-3-540-32275-7_2},
 ABSTRACT      = {Resolution-based calculi are among the most widely used calculi 
 for theorem proving in first-order logic. Numerous refinements 
 of resolution are nowadays available, such as e.g. basic superposition, 
 a calculus highly optimized for theorem proving with equality. However, 
 even such an advanced calculus does not restrict inferences enough to 
 obtain decision procedures for complex logics, such as SHIQ. 
 In this paper, we present a new decomposition inference rule, 
 which can be combined with any resolution-based calculus compatible 
 with the standard notion of redundancy. We combine decomposition with 
 basic superposition to obtain three new decision procedures: 
 (i) for the description logic SHIQ, (ii) for the description logic ALCHIQb, 
 and (iii) for answering conjunctive queries over SHIQ knowledge bases. 
 The first two procedures are worst-case optimal and, based on the 
 vast experience in building efficient theorem provers, we expect them 
 to be suitable for practical usage.}
}