Improving rewriting induction approach for proving ground confluence

DOI10.4230/LIPICS.FSCD.2017.7zbMATH Open1434.68215OpenAlexW2758285181MaRDI QIDQ5111302FDOQ5111302

Authors Takahito Aoto, Yoshihito Toyama, Y. Kimura

Publication date 26 May 2020

Full work available at URL http://doi.org/10.4230/LIPIcs.FSCD.2017.7

zbMATH Keywords

term-rewriting systemsground confluencerewriting inductionnon-orientable equations

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Ground confluence prover based on rewriting induction
• Term rewriting induction
• Proving Confluence of Term Rewriting Systems Automatically
• Proving ground confluence and inductive validity in constructor based equational specifications
• Publication:3490953

Cites work

• scientific article; zbMATH DE number 3990847 (Why is no real title available?)
• scientific article; zbMATH DE number 4043234 (Why is no real title available?)
• scientific article; zbMATH DE number 1889386 (Why is no real title available?)
• scientific article; zbMATH DE number 6792369 (Why is no real title available?)
• Automated Mathematical Induction
• Confluence by decreasing diagrams
• Deductive and inductive synthesis of equational programs
• Disproving confluence of term rewriting systems by interpretation and ordering
• Ground confluence prover based on rewriting induction
• On sufficient-completeness and related properties of term rewriting systems
• Proving Confluence of Term Rewriting Systems Automatically
• Proving ground confluence and inductive validity in constructor based equational specifications
• Simultaneous checking of completeness and ground confluence for algebraic specifications
• Term rewriting induction
• Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness

Cited in

(2)

• Datatype defining rewrite systems for naturals and integers
• Ground confluence prover based on rewriting induction

This page was built for publication: Improving rewriting induction approach for proving ground confluence

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