Proof transformation for non-compatible rewriting

DOI10.1007/3-540-61732-9_56MaRDI QIDQ6560375zbMATH OpenFDO

Authors Reinhard Bündgen

Publication date 21 June 2024

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Grammars and rewriting systems (68Q42)

Recommendations

• A New and Formalized Proof of Abstract Completion
• Equational inference, canonical proofs, and proof orderings
• Abstract completion, formalized
• scientific article; zbMATH DE number 7204438
• Critical pair criteria for completion

Cites work

• scientific article; zbMATH DE number 43246 (Why is no real title available?)
• An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal
• Buchberger's algorithm: The term rewriter's point of view
• Critical pair criteria for completion
• Equational inference, canonical proofs, and proof orderings
• On theories with a combinatorial definition of 'equivalence'
• Proving termination with multiset orderings
• Systems of reductions
• The diamond lemma for ring theory

This page was built for publication: Proof transformation for non-compatible rewriting

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