Confluence Competition

CTRS Category

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

Format

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.

Examples

  1. (CONDITIONTYPE ORIENTED)
    (VAR x)
    (RULES
      not(x) -> false | x == true
      not(x) -> true  | x == false
    )
    
    The correct answer is YES and a possible output is
    YES
    
    The unraveled TRS
    
    (VAR x1)
    (RULES
      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.
    
  2. (CONDITIONTYPE ORIENTED)
    (VAR )
    (RULES
      a -> b
      a -> c
      b -> c | b == c
    )
    
    The correct answer is NO and a possible output is
    NO
    
    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.