Confluence Competition

TRS Category

This is the oldest CoCo category. It is concerned with confluence of first-order rewrite systems.


The input is a first-order rewrite system without conditions, specified in the basic TRS format.

The question to be answered is whether the rewrite system is confluent on the terms that can be built from the function symbols appearing in (RULES rulelist) and variables. The first line of the output must be

In the first two cases, the output must be followed by justification that is understandable by a human expert.


  1. (VAR x)
      f(a) -> b
      f(f(x)) -> a
    The correct answer is NO and possible outputs include
    The peak a *<- f(f(a)) ->* f(b) is not joinable.
  2. (VAR x y z)
      Ap(Ap(Ap(S,x),y),z) -> Ap(Ap(x,z),Ap(y,z))
      Ap(Ap(K,x),y) -> x
      Ap(I,x) -> x
    The correct answer is YES and a possible output is
    The TRS is orthogonal.

Problem Selection

Problems are selected among those in COPS with the 'trs' tag.