A Fully Syntactic AC-RPO

We present the first fully syntactic (i.e., non-interpretation-based) AC-compatible recursive path ordering (RPO). It is simple, and hence easy to implement, and its behaviour is intuitive as in the standard RPO. The ordering is AC-total and defined uniformly for both ground and nonground terms, as well as for partial precedences. More important, it is the first one that can deal incrementally with partial precedences, an aspect that is essential, together with its intuitive behaviour, for interactive applications such as Knuth–Bendix completion.