Skip to Main content Skip to Navigation
Conference papers

Termination of Order-sorted Rewriting

Abstract : In this paper, the problem of termination of rewriting in order-sorted algebras is addressed for the first time. Our goal is to perform termination proofs of programs for executable specification languages like OBJ3. An extension of Lexicographic Path Ordering is proposed, that gives a termination proof for order-sorted rewrite systems, that would not terminate in the unsorted case. We mention also, that this extension provides a termination tool for unsorted terminating systems, that usual orderings cannot handle.
Complete list of metadata

Cited literature [15 references]  Display  Hide  Download

https://hal.inria.fr/hal-01893012
Contributor : Isabelle Gnaedig <>
Submitted on : Thursday, October 11, 2018 - 12:24:18 AM
Last modification on : Friday, October 26, 2018 - 12:28:33 PM
Long-term archiving on: : Saturday, January 12, 2019 - 12:40:27 PM

File

termin-os-conf-preprint.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Isabelle Gnaedig. Termination of Order-sorted Rewriting. ALP 1992 - 3rd International Conference on Algebraic and Logic Programming, Sep 1992, Volterra, Italy. pp.37 - 52, ⟨10.1007/bfb0013818⟩. ⟨hal-01893012⟩

Share

Metrics

Record views

89

Files downloads

283