Left-Linear Completion with AC Axioms

DOI10.1007/978-3-031-38499-8_23MaRDI QIDQ6492759

Unnamed Author, Nao Hirokawa, Aart Middeldorp

Publication date: 26 April 2024

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Multi-completion with termination tools
• Only prime superpositions need be considered in the Knuth-Bendix completion procedure
• Normalized rewriting: An alternative to rewriting modulo a set of equations
• KBCV – Knuth-Bendix Completion Visualizer
• Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion
• Slothrop: Knuth-Bendix Completion with a Modern Termination Checker
• Completion of a Set of Rules Modulo a Set of Equations
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Term Rewriting and All That
• Extending Maximal Completion (Invited Talk)
• Nagoya Termination Tool
• AC Completion with Termination Tools

This page was built for publication: Left-Linear Completion with AC Axioms