Publisher Summary This chapter discusses completion algorithms for conditional rewriting
systems. It provides an overview on a completion algorithm for hierarchical conditional term
rewriting systems (CTRS). The algorithm starts by trying to orient as many equations as it
can, using information given by the user about the precedence on the operators. When it has
too little information, it asks the user for more. Moreover, it checks the rules against hierarchy
hypotheses. The preconditions have to be primitive and the left-hand sides have to contain …