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
(VAR idlist) and the function symbols
(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.
(CONDITIONTYPE ORIENTED) (VAR x) (RULES not(x) -> false | x == true not(x) -> true | x == false )The correct answer is
YESand 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.
(CONDITIONTYPE ORIENTED) (VAR ) (RULES a -> b a -> c b -> c | b == c )The correct answer is
NOand 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
Problems are selected among those in COPS with the '3_ctrs' and 'oriented' tags.