A total AC-compatible ordering based on RPO

DOI10.1016/0304-3975(94)00276-2MaRDI QIDQ673623zbMATH OpenOpenAlexFDO

Authors Albert Rubio, Robert Nieuwenhuis

Publication date 28 February 1997

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(94)00276-2

zbMATH Keywords

AC-symbolsrewrite ryles

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• A precedence-based total AC-compatible ordering
• An AC-compatible Knuth-Bendix order.
• A fully syntactic AC-RPO.
• Publication:4938602
• A total, ground path ordering for proving termination of AC-rewrite systems

Cites work

• scientific article; zbMATH DE number 4047066 (Why is no real title available?)
• scientific article; zbMATH DE number 18651 (Why is no real title available?)
• scientific article; zbMATH DE number 176755 (Why is no real title available?)
• scientific article; zbMATH DE number 1348468 (Why is no real title available?)
• scientific article; zbMATH DE number 1348470 (Why is no real title available?)
• scientific article; zbMATH DE number 500953 (Why is no real title available?)
• A precedence-based total AC-compatible ordering
• AC-superposition with constraints: no AC-unifiers needed
• Any ground associative-commutative theory has a finite canonical system
• Associative-commutative reduction orderings
• Extension of the associative path ordering to a chain of associative commutative symbols
• On ground AC-completion
• SOLVING SYMBOLIC ORDERING CONSTRAINTS
• Termination of rewriting
• Termination of rewriting systems by polynomial interpretations and its implementation
• Termination orderings for associative-commutative rewriting systems

Cited in

(15)

• On the specification of visual languages: multisets as first-class citizens
• Theorem proving modulo associativity
• A fully syntactic AC-RPO.
• Theorem proving in cancellative abelian monoids (extended abstract)
• Canonized Rewriting and Ground AC Completion Modulo Shostak Theories
• An AC-compatible Knuth-Bendix order.
• AC-KBO revisited
• AC unification through order-sorted AC1 unification
• Unification of infinite sets of terms schematized by primal grammars
• Termination Modulo Combinations of Equational Theories
• AC-superposition with constraints: no AC-unifiers needed
• A note on division orderings on strings
• scientific article; zbMATH DE number 1405623 (Why is no real title available?)
• A precedence-based total AC-compatible ordering
• AC-KBO revisited

Describes a project that uses

Uses Software

• REVE

This page was built for publication: A total AC-compatible ordering based on RPO

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q673623)