Semantic Matching for Left-Linear Convergent Rewrite Systems
Bernd Bütow, Robert Giegerich, Enno Ohlebusch, Stephan Thesing · 1999
In this paper, a calculus for solving the semantic matching problem w.r.t. left-linear or variable-preserving convergent term rewriting systems is presented. Narrowing calculi usually use advanced selection rules to reduce the search space. Our approach to design a special calculus for special goals is 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, i.e. from right to left. For these reasons, the calculus is called Reverse Restructuring. We show soundness and completeness of Reverse Restructuring and demonstrate its efficiency for an important class of problems. This work was supported by the DFG-project "Abstrakte Inferenzmaschine" under Az. Gi 178/1-2. A preliminary version of the paper (which didn't contain a proof of the completeness...