Difference of constrained patterns in logically constrained term rewrite systems

DOI10.1007/978-3-032-04167-8_14MaRDI QIDQ6852308zbMATH OpenFDO

Authors Naoki Nishida, Misaki Kojima, Yuto Nakamura

Publication date 26 February 2026

Copyright license Creative Commons Attribution 4.0 International

zbMATH Keywords

complementunificationquasi-reducibilitylogically constrained rewriting

Mathematics Subject Classification ID

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

Cites work

• scientific article; zbMATH DE number 1729952 (Why is no real title available?)
• scientific article; zbMATH DE number 4011966 (Why is no real title available?)
• A coinductive approach to proving reachability properties in logically constrained term rewriting systems
• A nesting-preserving transformation of SIMP programs into logically constrained term rewrite systems
• A verified algorithm for deciding pattern completeness
• Completion for logically constrained rewriting
• Confluence of logically constrained rewrite systems revisited
• Constrained term rewriting tooL
• Equational theories and validity for logically constrained term rewriting
• Improving rewriting induction approach for proving ground confluence
• Loop detection by logically constrained term rewriting
• Matching \(\mu \)-logic
• Matching logic
• Matching µ-logic: Foundation of K framework
• Negation elimination in empty or permutative theories
• On sufficient-completeness and related properties of term rewriting systems
• Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting
• Sufficient completeness verification for conditional and constrained TRS
• Term Rewriting with Logical Constraints
• Term rewriting induction
• The negation elimination from syntactic equational formula is decidable
• Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness
• Transforming concurrent programs with semaphores into logically constrained term rewrite systems
• Unification Modulo Builtins
• Unification with abstraction and theory instantiation in saturation-based reasoning
• Verifying procedural programs via constrained rewriting induction
• Warnings for pattern matching

This page was built for publication: Difference of constrained patterns in logically constrained term rewrite systems

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