Confluence Criteria for Logically Constrained Rewrite Systems

DOI10.1007/978-3-031-38499-8_27MaRDI QIDQ6492763zbMATH OpenFDO

Authors Jonas Schöpf, Aart Middeldorp

Publication date 26 April 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-38499-8_27

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) 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
• Certification of classical confluence results for left-linear term rewrite systems
• Completion for logically constrained rewriting
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Constrained term rewriting tooL
• scientific article; zbMATH DE number 4106267 (Why is no real title available?)
• Runtime complexity analysis of logically constrained rewriting
• Term Rewriting and All That
• Term Rewriting with Logical Constraints
• Verifying procedural programs via constrained rewriting induction

Cited in

(2)

• Equational theories and validity for logically constrained term rewriting
• Confluence of logically constrained rewrite systems revisited

This page was built for publication: Confluence Criteria for Logically Constrained Rewrite Systems

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