CSI -- a confluence tool

DOI10.1007/978-3-642-22438-6_38MaRDI QIDQ5200045zbMATH OpenOpenAlexFDO

Authors Harald Zankl, Bertram Felgenhauer, Aart Middeldorp

Publication date 29 July 2011

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-22438-6_38

zbMATH Keywords

automationconfluenceterm rewriting

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• CSI: new evidence -- a progress report
• CoLL: a confluence tool for left-linear term rewrite systems
• Conditional confluence (system description)
• Proving Confluence of Term Rewriting Systems Automatically
• Deciding confluence of ground term rewrite systems in cubic time

Cites work

• Automated certified proofs with CiME3
• Automated confluence proof by decreasing diagrams based on rule-labelling
• Confluence by Decreasing Diagrams
• Confluence by decreasing diagrams
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Developing developments
• Frontiers of Combining Systems
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• Labelings for Decreasing Diagrams.
• Layer systems for proving confluence
• Match-bounds revisited
• Proving Confluence of Term Rewriting Systems Automatically
• Term Rewriting and All That

Cited in

(18)

• Conditions for confluence of innermost terminating term rewriting systems
• Labelings for decreasing diagrams
• CSI: new evidence -- a progress report
• Nominal confluence tool
• Certification of classical confluence results for left-linear term rewrite systems
• Layer systems for proving confluence
• Certifying confluence proofs via relative termination and rule labeling
• CoLL: a confluence tool for left-linear term rewrite systems
• Constrained term rewriting tooL
• Reachability, confluence, and termination analysis with state-compatible automata
• Conditional confluence (system description)
• Datatype defining rewrite systems for naturals and integers
• Compositional confluence criteria
• CSI: MSRI
• On Ground Convergence and Completeness of Conditional Equational Program Hierarchies
• Reconstruction of SMT proofs with Lambdapi
• Checking linear integer arithmetic proofs in Lambdapi
• De Bruijn's weak diamond property revisited

Describes a project that uses

Uses Software

• CiME
• CSI
• Tyrolean

This page was built for publication: CSI -- a confluence tool

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