On Modularity in Term Rewriting and Narrowing

We introduce a modular property of equational proofs, called modularity of normalization, for the union of term rewrite systems with shared symbols. The idea is, that every normalization with R = R1 + R2 may be obtained by rst normalizing with R1 followed by an R2 normalization. We develop criteria for this that cover non-convergent TRS R, where, as the main restriction, R1 is required to be left-linear and convergent. As interesting applications we consider solving equations modulo a theory given by a TRS. Here we present a modular narrowing strategy that can be combined with nearly all common narrowing strategies. Furthermore, we also prove some modularity results for decidability of uni cation and matching (via termination of narrowing).

• Type: Conference
• Year: 1994
• Where: CCL
• Authors: Christian Prehofer
• Keywords: Automated Reasoning, CCL 1994, Cover Non-convergent Trs, Modular Narrowing Strategy, R2 Normalization