CoLL: a confluence tool for left-linear term rewrite systems

DOI10.1007/978-3-319-21401-6_8MaRDI QIDQ3454087zbMATH OpenOpenAlexFDO

Authors Kiraku Shintani, Nao Hirokawa

Publication date 2 December 2015

Published in Automated Deduction - CADE-25 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-21401-6_8

Mathematics Subject Classification ID

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

Recommendations

• CSI -- a confluence tool
• Conditional confluence (system description)
• Certification of classical confluence results for left-linear term rewrite systems
• Proving Confluence of Term Rewriting Systems Automatically
• Term Rewriting and Applications

Cites work

• scientific article; zbMATH DE number 4106267 (Why is no real title available?)
• scientific article; zbMATH DE number 1189062 (Why is no real title available?)
• scientific article; zbMATH DE number 1346492 (Why is no real title available?)
• scientific article; zbMATH DE number 3413831 (Why is no real title available?)
• A Church-Rosser checker tool for conditional order-sorted equational Maude specifications
• A fully syntactic AC-RPO.
• A reduction-preserving completion for proving confluence of non-terminating term rewriting systems
• A residual-based a posteriori error estimator for the Stokes-Darcy coupled problem
• Analysis of Least-Squares Finite Element Methods for the Navier--Stokes Equations
• Automated confluence proof by decreasing diagrams based on rule-labelling
• CSI -- a confluence tool
• Confluence by Decreasing Diagrams
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Decreasing diagrams and relative termination
• Developing developments
• Minimal solutions of linear diophantine systems : bounds and algorithms
• Modular properties of composable term rewriting systems
• On the Church-Rosser property for the direct sum of term rewriting systems
• Proving Confluence of Term Rewriting Systems Automatically

Cited in

(8)

• First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification
• CSI -- a confluence tool
• Certifying proofs in the first-order theory of rewriting
• CoLL
• Certification of classical confluence results for left-linear term rewrite systems
• Compositional confluence criteria
• Constrained term rewriting tooL
• Conditional confluence (system description)

Describes a project that uses

Uses Software

• CRC 3
• CSI

This page was built for publication: CoLL: a confluence tool for left-linear term rewrite systems

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