Verifying a Decision Procedure for Pattern Completeness
From MaRDI portal
- A verified algorithm for deciding pattern completeness
- First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification
- Ground confluence prover based on rewriting induction
- Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness
This page was built for software: Verifying a Decision Procedure for Pattern Completeness