Proving Associative-Commutative Termination Using RPO-compatible Orderings
Proc. Automated Deduction in Classical and Non-Classical Logics
Springer LNAI 1761, Jan 2000
Deepak Kapur and G. Sivakumar

To view the entire paper click here