Modular and incremental automated termination proofs
We propose a modular approach of term rewriting systems, making the best of their hierarchical structure. We define rewriting modules and then provide a new method to prove termination incrementally. We obtain new and powerful termination criteria for standard rewriting, thanks to the combination of dependency pairs and C-epsilon-termination. Taking benefit of the generality of the module approach while restraining the notion of termination itself (thus relaxing constraints over hierarchies components), we can easily express previous results and methods the premises of which either include restrictions over unions or make a particular reduction strategy compulsory. We describe our implementation of the modular approach. Proofs are fully automated and performed incrementally. Since convenient orderings are simpler, we observe a dramatic speedup in the finding of the proof.
termination term rewriting systems