Proof transformation for non-compatible rewriting

DOI10.1007/3-540-61732-9_56zbMATH Open1541.68451MaRDI QIDQ6560375FDOQ6560375

Authors: Reinhard Bündgen 

Publication date: 21 June 2024

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

Mathematics Subject Classification ID

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

Cites Work

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

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)