Extending reduction orderings to ACU-compatible reduction orderings

DOI10.1016/S0020-0190(98)00084-2zbMath1339.68243MaRDI QIDQ293311

Uwe Waldmann

Publication date: 9 June 2016

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: http://www.sciencedirect.com/science/article/pii/S0020019098000842?np=y

zbMATH Keywords

terminationterm rewritingautomatic theorem provingabelian monoids

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

Cancellative Abelian monoids and related structures in refutational theorem proving. II

Cites Work

• Unnamed Item
• Unnamed Item
• Termination and completion modulo associativity, commutativity and identity
• Cancellative Abelian monoids and related structures in refutational theorem proving. II
• Normalized rewriting: An alternative to rewriting modulo a set of equations
• Complete Sets of Reductions for Some Equational Theories
• Transforming termination by self-labelling
• Theorem proving in cancellative abelian monoids (extended abstract)
• Complete sets of reductions modulo associativity, commutativity and identity
• Superposition theorem proving for abelian groups represented as integer modules