Abstract
Developing path orderings for associative-commutative (AC) rewrite systems has been quite a challenge at least for a decade. Compatibility with the recursive path ordering (RPO) schemes is desirable, and this property helps in orienting the commonly encountered distributivity axiom as desired. For applications in theorem proving and constraint solving, a total ordering on ground terms involving AC operators is often required. It is shown how the main solutions proposed so far ([7],[13]) with the desired properties can be viewed as arising from a common framework. A general scheme that works for non-ground (general) terms also is proposed. The proposed definition allows flexibility (using different abstractions) in the way the candidates of a term with respect to an associative-commutative function symbol are compared, thus leading to at least two distinct orderings on terms (from the same precedence relation on function symbols).
This paper is a revised version of an earlier draft entitled A recursive path ordering for proving associative-commutative termination [8] by the authors which was published as a technical report of the Department of Computer Science, State University of New York, Albany, NY 12222, May 1998. This research has been partially supported by the National Science Foundation Grant nos. CCR-9712366, CCR-9712396, and CDA-9503064.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bachmair, L., and Plaisted, D.A. (1985): Termination orderings for associative-commutative rewriting systems. J. Symbolic Computation, 1, 329–349
Ben Cherifa, A., and Lescanne, P. (1987): Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming, 9,2, 137–160.
Delor, C., Puel, L. (1993): Extension of the associative path ordering to a chain of associative commutative symbols. Proc. of 5th Intl. Conf. on Rewrite Techniques and Applications (RTA-93), LNCS, Springer-Verlag, 389–404.
Dershowitz, N. (1987): Termination of rewriting. J. Symbolic Computation, 3, 69–116.
Gnaeding, I., and Lescanne, P. (1986): Proving termination of associative-commutative rewriting systems by rewriting. Proc. of 8th Intl. Conf. on Automated Deduction (CADE-8), Oxford, LNCS 230 (ed. Siekmann), Springer Verlag, 52–60.
Kapur, D., and Sivakumar, G. (1995): Maximal extensions of simplification orderings. Proc. of 15th Conf. on Foundations of Software Technology and Theoretical Computer Science (ed. Thiagarajan), Bangalore, India, Springer Verlag LNCS 1026, 225–239, Dec. 1995.
Kapur, D., and Sivakumar, G. (1997): A total ground path ordering for proving termination of AC-Rewrite systems. Proc. Rewriting Techniques and Applications, 8th Intl. Conf., RTA-97, Sitges, Spain, June 1997, Springer LNCS 1231 (ed. H. Comon), 142–156.
Kapur, D., and Sivakumar, G.: A recurive path ordering for proving associative-commutative termination Technical Report, Department of Computer Science, State University of New York, Albany, NY, May 1998.
Kapur, D., Sivakumar, G. and Zhang, H. (1995): A new ordering for proving termination of AC-rewrite systems. J. Automated Reasoning, 1995.
Kapur, D., and Zhang, H. (1995): An overview of Rewrite Rule Laboratory (RRL). J. Computer and Mathematics with Applications, 29,2, 91–114.
Lankford, D.S. (1979): On proving term rewriting systems are Noetherian. Memo MTP-3, Lousiana State University.
Narendran, P., and Rusinowitch, M. (1991): Any ground associative commutative theory has a finite canonical system. In Book, R. (ed.) Proc. of 4th Intl. Conf. on Rewrite Techniques and Applications (RTA-91), LNCS 488, 423–434.
Rubio, A. (1997): A total AC-compatible ordering with RPO scheme. Technical Report, Technical Univ. of Catalonia, Barcelona, Spain.
Rubio, A., Nieuwenhuis, R. (1993): A precedence-based total AC-compatible ordering. In Kirchner, C. (ed.) Proc. of 5th Intl. Conf. on Rewrite Techniques and Applications (RTA-93), LNCS Springer-Verlag, 374–388.
Steinbach, J. (1989): Path and decomposition orderings for proving AC-termination. Seki-Report, SR-89-18, University of Kaiserslautern. See also “Improving associative path orderings,” in: Proc. of 10th Intl. Conf. on Automated Deduction (CADE-10), Kaiserslautern, LNCS 449 (ed. Stickel), 411–425.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kapur, D., Sivakumar, G. (2000). Proving Associative-Commutative Termination Using RPO-Compatible Orderings. In: Caferra, R., Salzer, G. (eds) Automated Deduction in Classical and Non-Classical Logics. FTP 1998. Lecture Notes in Computer Science(), vol 1761. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46508-1_3
Download citation
DOI: https://doi.org/10.1007/3-540-46508-1_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67190-9
Online ISBN: 978-3-540-46508-9
eBook Packages: Springer Book Archive