AC Completion with Termination Tools

DOI10.1007/978-3-642-22438-6_37zbMath1341.68198OpenAlexW65907803MaRDI QIDQ5200044

Sarah Winkler, Aart Middeldorp

Publication date: 29 July 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-22438-6_37

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

Multi-completion with termination tools

Uses Software

• Tyrolean
• AProVE
• mkbTT
• Slothrop
• REVE

Cites Work

• Unnamed Item
• Unnamed Item
• Termination of rewriting systems by polynomial interpretations and its implementation
• Matrix interpretations for proving termination of term rewriting
• An algebraic approach to unification under associativity and commutativity
• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• Adventures in associative-commutative unification
• Completion for multiple reduction orderings
• Modular and incremental proofs of AC-termination
• Proving Termination Properties with mu-term
• Slothrop: Knuth-Bendix Completion with a Modern Termination Checker
• Multi-completion with Termination Tools (System Description)
• Complete Sets of Reductions for Some Equational Theories
• A Dependency Pair Framework for A ∨ C-Termination