This is the oldest CoCo category. It is concerned with confluence of first-order rewrite systems.
The input is a first-order rewrite system without conditions, specified in the basic TRS format.
The question to be answered is whether the rewrite system is confluent on
the terms that can be built from the function symbols appearing in
(RULES rulelist) and variables. 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(a) -> b f(f(x)) -> a )The correct answer is
NOand possible outputs include
NO The peak a *<- f(f(a)) ->* f(b) is not joinable.and
(VAR x y z) (RULES Ap(Ap(Ap(S,x),y),z) -> Ap(Ap(x,z),Ap(y,z)) Ap(Ap(K,x),y) -> x Ap(I,x) -> x )The correct answer is
YESand a possible output is
YES The TRS is orthogonal.
Problems are selected among those in COPS with the 'trs' tag.