A verified algorithm for deciding pattern completeness

DOI10.4230/LIPICS.FSCD.2024.27MaRDI QIDQ6874982zbMATH OpenFDO

Authors René Thiemann, Akihisa Yamada

Publication date 14 January 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.FSCD.2024.27

zbMATH Keywords

Isabelle/HOLpattern matchingterm rewriting

Mathematics Subject Classification ID

Theory of computing (68Qxx)

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

Cited in

(2)

• Difference of constrained patterns in logically constrained term rewrite systems
• A nominal approach to equational problems in languages with binders

This page was built for publication: A verified algorithm for deciding pattern completeness

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