Categories – TRS
This is the oldest CoCo category. It is concerned with confluence of firstorder rewrite systems.
Format
The input is a firstorder rewrite system without conditions, specified in the ARI TRS format. The question to be answered is whether the rewrite system is confluent.
Examples

(format TRS) (fun a 0) (fun b 0) (fun f 1) (rule (f a) b) (rule (f (f x)) a)
The correct answer isNO
. 
(format TRS) (fun Ap 2) (fun I 0) (fun K 0) (fun S 0) (rule (Ap (Ap (Ap S x) y) z) (Ap (Ap x z) (Ap y z))) (rule (Ap (Ap K x) y) x) (rule (Ap I x) x)
The correct answer isYES
.
Problem Selection
Problems are selected from those in the ARI database with the 'trs' tag.