Confluence Competition

CTRS Category

The CTRS category is concerned with confluence of conditional term rewrite systems.


The input is an oriented conditional term rewrite system of type 3, specified in the CTRS format.

The question to be answered is whether the rewrite system is confluent on the terms that can be built from the variables declared in the (VAR idlist) and the function symbols appearing in (RULES rulelist). 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.


    (VAR x)
      not(x) -> false | x == true
      not(x) -> true  | x == false
    The correct answer is YES and a possible output is
    The unraveled TRS
    (VAR x1)
      not(x1)      -> u1(x1,x1)
      u1(true,x1)  -> false
      u1(false,x1) -> true
    is orthogonal and hence confluent. By soundness of unraveling for
    confluence, the CTRS is confluent.
    (VAR )
      a -> b
      a -> c
      b -> c | b == c
    The correct answer is NO and a possible output is
    The rule
      b -> c | b == c
    is infeasible. The remaining rules constitute a non-confluent TRS because
    of the non-joinable peak
      b <- a -> c

Problem Selection

Problems are selected among those in COPS with the '3_ctrs' and 'oriented' tags.