CSI -- a confluence tool. This paper describes a new confluence tool for term rewrite systems. Due to its modular design, the few techniques implemented so far can be combined flexibly. Methods developed for termination analysis are adapted to prove and disprove confluence. Preliminary experimental results show the potential of our tool.

References in zbMATH (referenced in 13 articles )

Showing results 1 to 13 of 13.
Sorted by year (citations)

  1. Felgenhauer, Bertram; Thiemann, René: Reachability, confluence, and termination analysis with state-compatible automata (2017)
  2. Nagele, Julian; Felgenhauer, Bertram; Zankl, Harald: Certifying confluence proofs via relative termination and rule labeling (2017)
  3. Sternagel, Christian; Sternagel, Thomas: Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems (2017)
  4. Aoto, Takahito; Kikuchi, Kentaro: Nominal confluence tool (2016)
  5. Nagele, Julian; Middeldorp, Aart: Certification of classical confluence results for left-linear term rewrite systems (2016)
  6. Felgenhauer, Bertram; Middeldorp, Aart; Zankl, Harald; Van Oostrom, Vincent: Layer systems for proving confluence (2015)
  7. Shintani, Kiraku; Hirokawa, Nao: CoLL: a confluence tool for left-linear term rewrite systems (2015)
  8. Zankl, Harald; Felgenhauer, Bertram; Middeldorp, Aart: Labelings for decreasing diagrams (2015)
  9. Sternagel, Thomas; Middeldorp, Aart: Conditional confluence (system description) (2014)
  10. Aoto, Takahito: Disproving confluence of term rewriting systems by interpretation and ordering (2013)
  11. Endrullis, Jörg; Klop, Jan Willem: De Bruijn’s weak diamond property revisited (2013)
  12. Klein, Dominik; Hirokawa, Nao: Confluence of non-left-linear TRSs via relative termination (2012)
  13. Zankl, Harald; Felgenhauer, Bertram; Middeldorp, Aart: CSI -- a confluence tool (2011)