• CSI

  • Referenced in 22 articles [sw09767]
  • confluence tool. This paper describes a new confluence tool for term rewrite systems ... analysis are adapted to prove and disprove confluence. Preliminary experimental results show the potential...
  • Saigawa

  • Referenced in 9 articles [sw10102]
  • Saigawa is a fully automatic confluence tool for first-order term rewrite systems. The latest ... version is based on the four confluence criteria: confluence criterion of Hirokawa and Middeldorp ... confluence criterion of Klein and Hirokawa (LPAR 2011); Church-Rosser modulo by Jouannaud and Kirchner...
  • Conditional Confluence

  • Referenced in 8 articles [sw13315]
  • Conditional confluence (system description). This paper describes the Conditional Confluence tool, a fully automatic confluence ... term rewrite systems. The tool implements various confluence criteria that have been proposed ... critical pairs for infeasibility, which makes conditional confluence criteria more useful. Detailed experimental data...
  • CoLL

  • Referenced in 5 articles [sw13633]
  • CoLL: a confluence tool for left-linear term rewrite systems. We present a confluence tool ... linear term rewrite systems. The tool proves confluence by using Hindley’s commutation theorem together ... tool is comparable to recent powerful confluence tools...
  • CoCoWeb

  • Referenced in 4 articles [sw28111]
  • Cops and CoCoWeb: infrastructure for confluence tools. In this paper we describe the infrastructure supporting ... confluence tools and competitions: Cops, the confluence problems database, and CoCoWeb, a convenient web interface ... tools that participate in the annual confluence competition...
  • CO3

  • Referenced in 3 articles [sw28113]
  • COnverter for proving COnfluence of COnditional TRSs. CO3 is a tool for proving confluence ... Serbanuta & Rosu, RTA 2006], and then verify confluence of the transformed TRS. CO3 is using ... very efficient. To make the confluence checking more powerful, we should implement more powerful methods ... proving confluence of TRSs, e.g., the critical pair theorem with using powerful termination proving methods...
  • Ctrl

  • Referenced in 6 articles [sw13874]
  • automatically analyse various properties such as termination, confluence and quasi-reductivity. Ctrl also offers both...
  • ConCon

  • Referenced in 3 articles [sw21589]
  • Reliable Confluence Checker for Conditional Term Rewrite Systems. ConCon is a fully automatic confluence checker ... ConCon issues calls to the external unconditional confluence and termination checkers CSI and TTT2 ... system, then it employs the following three confluence criteria: (A) a quasi-decreasing strongly deterministic...
  • Cops

  • Referenced in 3 articles [sw28112]
  • Cops and CoCoWeb: infrastructure for confluence tools. In this paper we describe the infrastructure supporting ... confluence tools and competitions: Cops, the confluence problems database, and CoCoWeb, a convenient web interface ... tools that participate in the annual confluence competition...
  • TenRes

  • Referenced in 5 articles [sw19993]
  • also makes the algorithmic verification of the confluence criterion more efficient. We provide an implementation...
  • Lolliproc

  • Referenced in 5 articles [sw22624]
  • example and prove soundness, strong normalization, and confluence results, which, among other things, guarantees freedom...
  • SCOOP

  • Referenced in 4 articles [sw10581]
  • reduction techniques. It can apply confluence reduction, dead variable reduction, constant elimination, summation elimination...
  • CoqMTU

  • Referenced in 3 articles [sw19138]
  • basic meta-theoretical properties of such calculi, confluence, subject reduction and strong normalization when restricted...
  • FORT

  • Referenced in 1 article [sw28637]
  • ground terms for properties related to confluence...
  • SOL

  • Referenced in 1 article [sw35247]
  • Order Laboratory, which assists the proofs of confluence and strong normalisation of computation rules derived...
  • MStaT

  • Referenced in 1 article [sw37786]
  • morphometrics module; (ii) migration module; and (iii) confluence module. MStaT delivers a short and medium...
  • ACL2

  • Referenced in 283 articles [sw00060]
  • ACL2 is both a programming language in which...
  • Coq

  • Referenced in 1856 articles [sw00161]
  • Coq is a formal proof management system. It...
  • Isabelle

  • Referenced in 674 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...