Confluence of logically constrained rewrite systems revisited

DOI10.1007/978-3-031-63501-4_16MaRDI QIDQ7034585zbMATH OpenFDO

Authors Jonas Schöpf, Fabian Mitterwallner, Aart Middeldorp

Publication date 31 January 2025

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-63501-4_16

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A coinductive approach to proving reachability properties in logically constrained term rewriting systems
• A variant of a recursively unsolvable problem
• Completion for logically constrained rewriting
• Compositional confluence criteria
• Confluence by critical pair analysis revisited
• Confluence Criteria for Logically Constrained Rewrite Systems
• Confluence without termination via parallel critical pairs
• CSI: new evidence -- a progress report
• Developing developments
• Disproving confluence of term rewriting systems by interpretation and ordering
• Formalizing almost development closed critical pairs (short paper)
• scientific article; zbMATH DE number 4106267 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• Labelings for decreasing diagrams
• Operationally-based program equivalence proofs using LCTRSs
• Proving Confluence of Term Rewriting Systems Automatically
• Term Rewriting with Logical Constraints
• Verifying procedural programs via constrained rewriting induction

Cited in

(2)

• Difference of constrained patterns in logically constrained term rewrite systems
• Confluence of almost parallel-closed generalized term rewriting systems

This page was built for publication: Confluence of logically constrained rewrite systems revisited

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