Left-linear completion with AC axioms

DOI10.46298/LMCS-21(2:10)2025MaRDI QIDQ6987756zbMATH OpenFDO

Authors Nao Hirokawa, Aart Middeldorp

Publication date 6 May 2025

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.46298/LMCS-21(2:10)2025

zbMATH Keywords

AC axiomscompletionterm rewriting

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Cites work

• A note on simplification orderings
• About the rewriting systems produced by the Knuth-Bendix completion algorithm
• Abstract completion, formalized
• AC completion with termination tools
• Complete Sets of Reductions for Some Equational Theories
• Completion and reduction orders (invited talk)
• Completion of a Set of Rules Modulo a Set of Equations
• Confluence by decreasing diagrams
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Encoding dependency pair techniques and control strategies for maximal completion
• Equational inference, canonical proofs, and proof orderings
• Extending Maximal Completion (Invited Talk)
• Formalizing Knuth-Bendix orders and Knuth-Bendix completion
• Group-like structures in general categories. I. Multiplications and comultiplications
• scientific article; zbMATH DE number 50648 (Why is no real title available?)
• scientific article; zbMATH DE number 752977 (Why is no real title available?)
• scientific article; zbMATH DE number 1889386 (Why is no real title available?)
• scientific article; zbMATH DE number 1414284 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• KBCV – Knuth-Bendix Completion Visualizer
• Left-linear completion with AC axioms
• Left-Linear Completion with AC Axioms
• Linear completion
• Maximal completion
• mu-term: Verify Termination Properties Automatically (System Description)
• Multi-completion with termination tools
• Nagoya termination tool
• Normalized completion revisited
• Normalized rewriting: An alternative to rewriting modulo a set of equations
• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• Proof orders for decreasing diagrams
• Proving termination with multiset orderings
• Rewriting Techniques and Applications
• Slothrop: Knuth-Bendix Completion with a Modern Termination Checker
• Strict coherence of conditional rewriting modulo axioms
• Term Rewriting and All That
• Termination of rewriting systems by polynomial interpretations and its implementation

Cited in

(1)

• Left-linear completion with AC axioms

This page was built for publication: Left-linear completion with AC axioms

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