CoCo 2019 will feature a new competition category on infeasibility problems.
Infeasibility problems are incorporated into COPS as follows:
(PROBLEM INFEASIBILITY) (COPS number) (VAR idlist) (CONDITION condlist) (COMMENT string)where
condlist ::= cond | cond , condlist cond ::= term == termhas the same syntax as the conditional part of a conditional rewrite rule and
numberrefers to an existing problem in CTRS or TRS format. If it is a CTRS then the semantics of
==is the same as declared in the
(CONDITIONTYPE ctype)declaration of the CTRS; if it is a TRS then the semantics of
->*). Variables declared in
idlistare used as variables in
condlist. Common function symbols occurring in COPS ♯
condlisthave the same arity. Moreover, function symbols in COPS ♯
numberdo not occur as variables in
idlistand function symbols in
condlistdo not occur as variables in COPS ♯
(VAR idlist)declaration can be omitted if the terms in
For the competition, the
(COPS number) declaration
will be inlined, before the problem is passed to participating tools.
The inlining program is available.
The question to be answered is whether
(CONDITION condlist) is
YES if no satisfying substitution exists,
NO if a satisfying substitution exists.
(PROBLEM INFEASIBILITY) (COPS 547) (VAR x) (CONDITION x == a, x == b) (COMMENT doi:10.4230/LIPIcs.FSCD.2016.29  Example 3 submitted by: Raul Gutierrez and Salvador Lucas )which expands to
(PROBLEM INFEASIBILITY) (COMMENT COPS 547) (CONDITIONTYPE ORIENTED) (VAR x) (RULES f(x) -> a | x == a f(x) -> b | x == b ) (VAR x) (CONDITION x == a, x == b)The correct answer is
(PROBLEM INFEASIBILITY) (COPS 47) (CONDITION G(A) == A) (COMMENT this comment will be removed)which expands to
(PROBLEM INFEASIBILITY) (COMMENT COPS 47) (VAR x) (RULES F(x,x) -> A G(x) -> F(x,G(x)) C -> G(C) ) (CONDITION G(A) == A)The correct answer is
(PROBLEM INFEASIBILITY) (CONDITIONTYPE ORIENTED) (VAR x y) (RULES f(x) -> g(x) ) (CONDITION f(x) == g(y)) (COMMENT ill-formed)This inlined problem is ill-formed. Since there is a no
(VAR idlist)declaration before the condition,
yare constants in the condition but also variables in the TRS, which is forbidden.
Problems are selected among those in COPS with the 'infeasibility' tag.