Format

To represent infeasibility problems, we use :problem infeasibility in the format specifications of TRSs and CTRSs:

  INF ::= iTRS | iCTRS
 iTRS ::= ( format TRS :problem infeasibility ) fun* rule* query
iCTRS ::= ( format CTRS cond-type :problem infeasibility ) fun* rule* query
query ::= ( infeasible? cond+ )
 cond ::= ( = term term )

The grammar rule for rule in iTRS (iCTRS) is the same as the one in the TRS (CTRS) format.

Examples

; @cops 1651
; @author Akihisa Yamada
(format TRS :problem infeasibility)
(fun f 1)
(fun g 1)
(fun h 1)
(rule (f (g (h x))) (g (f (h (g x)))))
(rule (f x) x)
(rule (g x) x)
(rule (h x) x)
(infeasible? (= (f (g (h x))) (g (f (g (h x))))))

For TRSs the equality sign in the infeasibility constraint is interpreted as reachability.

; @author Naoki Nishida
; @cops 858
; origin COPS 337
(format CTRS oriented :problem infeasibility)
(fun 0 0)
(fun cons 2)
(fun false 0)
(fun lt 2)
(fun s 1)
(fun true 0)
(rule (lt x 0) false)
(rule (lt 0 (s y)) true)
(rule (lt (s x) (s y)) (lt x y))
(rule (cons x (cons y ys)) (cons y (cons x ys)) (= (lt x y) true))
(infeasible? (= (lt x x1) true) (= (lt x1 x2) true))

The interpretation of the equality sign in the infeasibility constraint is the same as the one in the conditions of the conditional rewrite rules, so reachability in this case.