Confluence Competition

Categories – GCR

The GCR category is concerned with ground-confluence of many-sorted term rewrite systems (MSTRSs)


The input is a many-sorted first-order rewrite system without conditions, specified in the MSTRS format. The question to be answered is whether the rewrite system is confluent on all well-sorted ground terms.


  1. (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 is NO.
  2. (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 is YES.

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.