A verified algorithm for deciding pattern completeness with optimal asymptotic complexity

DOI10.1016/J.JLAMP.2026.101129MaRDI QIDQ7320649zbMATH OpenFDO

Authors René Thiemann, Akihisa Yamada

Publication date 27 August 2026

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/J.JLAMP.2026.101129

Mathematics Subject Classification ID

Computer science (68-XX)

Cites work

• First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification
• Ground confluence prover based on rewriting induction
• scientific article; zbMATH DE number 4037164 (Why is no real title available?)
• scientific article; zbMATH DE number 4049024 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• On sufficient-completeness and related properties of term rewriting systems
• Partial and nested recursive function definitions in higher-order logic
• Rewriting Induction + Linear Arithmetic = Decision Procedure
• SAT competition 2020
• Simultaneous checking of completeness and ground confluence for algebraic specifications
• Sufficient completeness verification for conditional and constrained TRS
• Sufficient-completeness, ground-reducibility and their complexity
• Term rewriting induction
• Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness

This page was built for publication: A verified algorithm for deciding pattern completeness with optimal asymptotic complexity

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