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

• YES, indicating that the input system is confluent,
• NO, indicating that the input system is non-confluent,
• any other answer (e.g., MAYBE) indicates that the tool could not determine the status of the input problem.

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.