Categories – INF

The INF category deals with infeasibility problems.

Format

The input is an infeasibility problem specified in the ARI INF format. The question to be answered is whether the condition contained in the problem is infeasible: YES if no satisfying substitution exists, NO if a satisfying substitution exists. The equality sign in the condition is interpreted as reachability if the rewrite system contained in the problem is a TRS or an oriented CTRS. For semi-equational (join) CTRSs the equality sign is interpreted as conversion (joinability).

Examples

1. ; origin COPS 547
   (format CTRS oriented :problem infeasibility)
   (fun a 0)
   (fun b 0)
   (fun f 1)
   (rule (f x) a (= x a))
   (rule (f x) b (= x b))
   (infeasible? (= x a) (= x b))
   

   The correct answer is YES.

2. ; origin COPS 47
   (format TRS :problem infeasibility)
   (fun A 0)
   (fun C 0)
   (fun F 2)
   (fun G 1)
   (rule (F x x) A)
   (rule (G x) (F x (G x)))
   (rule C (G C))
   (infeasible? (= (G A) A))
   

   The correct answer is YES.

Problem Selection

Problems are selected from those in the ARI database with the 'infeasibility' tag.