Termination of order-sorted rewriting

Termination of order-sorted rewriting

Peter C. Ĝlveczky

In 6th NWPT, pages 286-299


We present a method for proving termination of order-sorted rewrite systems by transforming an order-sorted rewrite system into an unsorted one such that termination of the latter implies termination of the order-sorted system. The method is inspired by ideas of Gnaedig and Ganzinger and contains as special cases the method presented in [Gn92a] and the method that simply ignores sort information.

[Gn92a] Termination of order-sorted rewriting. Proc. Algebraic and Logic Programming. Third International Conference, Springer-Verlag, 1992.

Department of Informatics, University of Oslo, Norway. Email: peterol@ifi.uio.no.

Available as PostScript, DVI.

[BRICS symbol] BRICS WWW home page