The UNC category is concerned with the "unique normal forms with respect to conversion" property (UNC) of first-order rewrite systems
The input is a first-order rewrite system without conditions, specified in
the basic TRS format or the
extended TRS format (since
UNC is preserved under signature extensions, tools are free to ignore the
(SIG funlist) declaration).
The question to be answered is whether the rewrite system has the property that distinct normal forms are not convertible. The first line of the output must be
YES, indicating that the input system is UNC,
NO, indicating that the input system is not UNC,
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(x,x) -> A G(x) -> F(x,G(x)) C -> G(C) )The correct answer is
YESand a possible output is
YES The result of Stefan Kahrs and Connor Smith (FSCD 2016) stating that non-omega-overlapping rewrite systems are UNC applies.
(VAR x) (RULES F(x,x) -> A F(x,G(x)) -> B C -> G(C) )The correct answer is
NOand a possible output is
NO The term F(C,C) has different normal forms A and B.