In this paper a calculus for solving the semantic matching problemwith respect to left-linear or variable-preserving convergent term-rewritingsystems is presented. Narrowing calculi usually use advancedselection rules to reduce the search space. Our approach to designing a special calculus for special goalsis another way of reducing the efficiency defects of narrowing.Our calculus constructs derivations in the reverse direction by guessing terms from which an already known term might be derived. To this end, the rules of the underlying term-rewriting system are also applied in the reverse direction, that is, from right to left. For these reasons, the calculus is called reverse restructuring.We show soundness and completeness of reverse restructuringand demonstrate its efficiency for an important class of problems.
展开▼
