Modular and incremental proofs of AC-termination

摘要

Termination is a non-modular property of rewriting systems, thus it is a difficult task to discover termination proofs for rewriting systems of a large number of rules. Recently, new modular and incremental termination criteria, suitable for automation, were proposed, using an approach based on notions of termination under non-deterministic collapse and dependency pairs, which apply to hierarchical combinations of rewriting systems. We extend this approach and corresponding results to the important case of rewriting modulo associativity and commutativity.