Left-Linear Completion with AC Axioms

DOI10.1007/978-3-031-38499-8_23MaRDI QIDQ6492759zbMATH OpenFDO

Authors Nao Hirokawa, Aart Middeldorp

Publication date 26 April 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-38499-8_23

Mathematics Subject Classification ID

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

Cites work

• Abstract completion, formalized
• AC completion with termination tools
• Completion of a Set of Rules Modulo a Set of Equations
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Extending Maximal Completion (Invited Talk)
• Formalizing Knuth-Bendix orders and Knuth-Bendix completion
• 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 3299786 (Why is no real title available?)
• scientific article; zbMATH DE number 7700620 (Why is no real title available?)
• KBCV – Knuth-Bendix Completion Visualizer
• Maximal completion
• 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
• Slothrop: Knuth-Bendix Completion with a Modern Termination Checker
• Term Rewriting and All That

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 Q6492759)