This category is concerned with confluence of string rewrite systems.
The input is a string rewrite system, specified in the basic TRS format.
The question to be answered is whether the string rewrite system is confluent. 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.
(VAR x) (RULES f(f(x)) -> g(x) )The correct answer is
NOand possible outputs include
NO The peak f(g(x)) *<- f(f(f(x))) ->* g(f(x)) is not joinable.and
(VAR x) (RULES f(f(x)) -> x f(x) -> f(f(x)) )The correct answer is
YESand a possible output is
YES The addition of the redundant rules f(x) -> f(f(f(x))) and f(x) -> x makes the critical pairs of the SRS development closed. Hence the SRS is confluent.
Problems are selected among those in COPS with the 'srs' tag.