Confluence and Completion of Membership Conditional TRS
Junnosuke Yamada · Institutional Repositories DataBase (IRDB) · 1990
We propose a sufficient condition for the confluence of noetherian quasi-closed membership conditional term rewriting systems (MCTRS).The condition is the critical pair lemma for MCTRS.For that purpose, we introduce contextual rewriting which modifies contexts attached to terms, and we extend the notion of critical pair to the rules of such rewriting.By allowing modification of contexts, we can treat wider class of MCTRS than the previous work.As an application of the condition, we propose a completion algorithm for such systems.Additionally we use the comple- tion algorithm for an inductionless induction like proof of a property of a recursively defined function.