Categories – GCR
The GCR category is concerned with groundconfluence of manysorted term rewrite systems (MSTRSs)
Format
The input is a manysorted firstorder rewrite system without conditions, specified in the MSTRS format. The question to be answered is whether the rewrite system is confluent on all wellsorted ground terms.
Examples

(format MSTRS) (sort 0) (sort 1) (fun a 0) (fun b 0) (fun c 0) (fun f (> 0 0 1)) (rule a b) (rule (f b b) (f a a)) (rule (f x a) (f a a))
The correct answer isNO
. 
(format MSTRS) (sort Nat) (sort Bool) (fun 0 Nat) (fun s (> Nat Nat)) (fun eq (> Nat Nat Bool)) (fun true Bool) (fun false Bool) (rule (eq x x) true) (rule (eq 0 (s x)) false) (rule (eq (s x) 0) false) (rule (eq (s x) (s y)) (eq x y)) (rule (eq x y) (eq y x))
The correct answer isYES
.
Problem Selection
Problems are selected from those in the ARI database with the 'trs' or the 'mstrs' tag. The former are transformed into MSTRSs with a single sort, prior to passing them to tools.