Abstract:
|
We present the first fully syntactic (i.e., non-interpretation-based)
AC-compatible recursive path ordering (RPO). It is very 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 non-ground terms, as well as for partial precedences.
More importantly, 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 like Knuth-Bendix
completion. |