Ground confluence prover based on rewriting induction

DOI10.4230/LIPICS.FSCD.2016.33MaRDI QIDQ5369498zbMATH OpenOpenAlexFDO

Authors Takahito Aoto, Yoshihito Toyama

Publication date 17 October 2017

Full work available at URL https://doi.org/10.4230/lipics.fscd.2016.33

zbMATH Keywords

ground confluencenon-orientable equationsrewriting inductionterm rewriting systems

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Improving rewriting induction approach for proving ground confluence
• Proving Confluence of Term Rewriting Systems Automatically
• Decidability of the confluence of finite ground term rewrite systems and of other related term rewrite systems
• scientific article; zbMATH DE number 4043234
• On ground-confluence of term rewriting systems

Cited in

(10)

• On transforming cut- and quantifier-free cyclic proofs into rewriting-induction proofs
• Proving Confluence of Term Rewriting Systems Automatically
• scientific article; zbMATH DE number 4043234 (Why is no real title available?)
• Proving ground confluence and inductive validity in constructor based equational specifications
• Improving rewriting induction approach for proving ground confluence
• First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification
• On Ground Convergence and Completeness of Conditional Equational Program Hierarchies
• A verified algorithm for deciding pattern completeness
• A verified algorithm for deciding pattern completeness with optimal asymptotic complexity
• Verifying a Decision Procedure for Pattern Completeness

Describes a project that uses

Uses Software

• CSI
• Saigawa

This page was built for publication: Ground confluence prover based on rewriting induction

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