A Total, Ground path Ordering for Proving Termination of AC-Rewrite Systems.

Deepak Kapur G. Sivakumar

Published in: RTA (1997)

Keyphrases

rewrite systems
knuth bendix
term rewriting
quantifier free
active rules
shortest path
operational semantics
theorem proving
theorem prover