“A practical ordering for AC rewrite systems”

Stephen J. Garland and Deepak Kapur

MIT Laboratory for Computer Science, 1996. Unpublished.

The AC-DSMPOS ordering orients a large class of associative-commutative (AC) equational systems automatically and efficiently into terminating rewrite systems. This ordering enhances DSMPOS, the “dynamically suggested monotonic path ordering with status” based on RPOS and used since 1985 in LP (the Larch Prover) with features developed by Kapur, Sivakumar and Zhang in 1990 to handle AC functions. The new ordering, which has been implemented in LP, automatically generates and uses precedence suggestions to orient AC equational systems incrementally into terminating rewrite systems. Experimental evidence indicates that AC-DSMPOS adequately and efficiently handles many examples arising in practical applications involving distributed algorithms, hardware and software descriptions and specifications, and equational axiomatizations of well-known algebraic structures and abstract data types that involve AC functions. (It also orients the distributivity axiom in the right direction.)

Back to Publications of Stephen J. Garland